I was reading today about a proposal regarding the Rust language’s use of async and await. which are related to colored subprograms. If you’re familiar with them, read on; if not, click the blurred text at bottom for a hopefully-correct explanation.

I naturally wondered how this issue affects Ada. I’m not as familiar with task types as I should be, even though I used them a few years ago, and Ada 2022 brings the new parallel keyword, which I have yet to use. After refreshing my memory:

Is my impression correct that Ada’s approach to concurrency and parallelism circumvents “colored” subprograms altogether? After all, task entries are called just like regular subprograms, and subprograms with parallel blocks are called just like other subprograms.

My apologies if I’m being unclear; please don’t hesitate to correct or scold me if I’m babbling nonsense. I know what I’m trying to say, but I’m not used to talking about these particular issues.

6 posts - 4 participants

Read full topic

I just ran alr edit to try something with SPARK and… gps had no SPARK menu! What happened to it?

I wondered if I don’t have the gnatprove crate installed. Neither alr get nor alr toolchain -i seemed to help, and alr show gnatprove gave a very unhelpful error message.

It somehow occurred to me that alr with might work, and sure enough, within moments gnatprove was being added to a project, and SPARK showed up in the gps menu!

But… it does not show up in other projects! Apparently I have to alr with spark in every project I want to use it in.

1. Is that what’s supposed to happen?
2. Is this documented somewhere? I didn’t see it if so.
3. Will it install a new gnatprove bin every time I install it, or is it just installed once, and set up in the projects where we use it?

5 posts - 3 participants

Read full topic

I’m trying to learn SPARK by implementing a Euclidean Ring package. (Don’t let the mathematics scare you; it’s not really relevant.) The package is generic, with several parameters that needs specification. Among these are a Size function, a Zero function, and a rem function.

If SPARK is to have any prayer at all of proving correctness, the rem function needs a constraint along these lines:

    generic

       -- a bunch of stuff omitted

       with function "rem" ( Dividend, Divisor : Ring_Element ) return Ring_Element
          is <>
              with
                 Pre => Divisor /= Zero,
                 Post => (
                             "rem"'Result /= Zero
                          or else Size ( "rem"'Result ) < Size ( Divisor )
                         )
       ;

…and the compiler chokes on the contracts:

euclidean.ads:39:13: incorrect placement of aspect "Pre"
euclidean.ads:40:13: incorrect placement of aspect "Post"

Originally I tried placing it before the is <> but that didn’t work, either.

So… where does one specify constraints for the parameters to a generic?

6 posts - 3 participants

Read full topic

gnatdoc doesn’t seem to document generic parameters to a package. Does that sound right?

In case my meaning isn’t clear, the following specification should do the trick. Ask away if not.

-- @summary this commentary appears (as long as there's no space between it and "generic" keyword)
generic
   type T is <>;
   -- commentary on T does not appear
   function "=" ( Left, Right: T ) return Boolean is <>;
   -- commentary on "=" does not appear
package P is
   -- commentary in here appears

7 posts - 3 participants

Read full topic

To help learn me some SPARK, I decided to try implementing the Euclidean Algorithm. With a generic type. Basically (simplified from what I actually have, which includes contracts):

generic

   type Ring_Element is private;

   Zero : Ring_Element;

   with function "=" (Left, Right : Ring_Element) return Boolean is <>;
   with function Size (Value : Ring_Element) return Natural;
   with function "-" ( Left, Right : Ring_Element ) return Ring_Element is <>;
   with function "rem"
     (Dividend, Divisor : Ring_Element) return Ring_Element is <>;
package Euclidean is ...

And the body Euclidean:

    function Gcd ( A, B : Ring_Element ) return Ring_Element is

       M: Ring_Element := A;
       N: Ring_Element := B;

    begin

       while N /= Zero loop

          declare
             R : constant Ring_Element := M rem N;
          begin
             M := N;
             N := R;
          end;

       end loop;

    end Gcd;

The algorithm has several nice properties. One is a loop invariant that r divides a - b.

I’ve struggled with getting SPARK to accept a contract to that effect. My latest iteration has this:

   if R /= Zero then ( A rem R ) - ( B rem R ) = Zero

…but when I instantiate Ring_Element => Integer it reports

   euclidean.adb:26:41: medium: loop invariant might fail in first iteration, cannot prove (A rem R ) - ( B rem R ) = Zero, in instantiation at main.adb:32 (e.g. when A = -2 and B = 1 and M = 1 and R = 3)[#0]

That… makes no sense. It’s not possible for the algorithm to start with those inputs and end up with R = 3.

1. Am I misreading the error report?
2. How does SPARK come up with this value of R?
3. Any advice on writing a contract for this condition? I’ve generally had trouble with guaranteeing arithmetic expressions like A + B and A - B; I understand why, but am not sure how to handle them. Using rem R was something I thought might help here, it did get me past the under/overflow, and it is also true.

10 posts - 3 participants

Read full topic

(If it matters, alr tells me that this is gnat_external=12.3.1; notice the pragma)

I was recently in a situation along these lines:

pragma Ada_2022;

   --  ...

   type Enum is (A, B, C);

   type Disc_Rec (Kind : Enum) is record
      case Kind is
         when A => Field : Natural;
         when others => null;
      end case;
   end record;

   --  ... in what follows, `Thing` is of type `constant Enum` and `Value` is of type 

         D : Disc_Rec := (
            case Thing is
               when A => Disc_Rec'(Kind => A, Field => Value),
               when B | C => Disc_Rec'(Kind => Thing)               --  LINE 37
         );

gnat tells me:

test_enum.adb:37:48: error: no single variant is associated with all values of the subtype of discriminant value "Kind"

Column 47 lands on Thing.

I understand the message, but I’d have thought it clear that since Thing has the type B or C in line 37, Thing has all values of the subtype that matter in this branch. Indeed, if Disc_Rec does not have the case statement that defines Field, and I remove the assignment to Field in line 36, the compiler sings happily. So the problem doesn’t seem to be Thing so much as that the optional Field… which isn’t needed in this branch.

Is there a way to make something like this work? My current workaround handles the branches explicitly (when A => ... , when B => ..., when C => ...), but In a practical case, Kind could have a lot of variants.

7 posts - 3 participants

Read full topic

@JeremyGrosser hasn’t posted on today’s puzzle yet; I hope he won’t mind if I do.

There’s always at least one puzzle with ginormous numbers, though I don’t recall their appearance in as early as Day 5!

The first speed bump I encountered is that gnat defaults (?) to 32-bit integers for Natural, so my machine choked, though nearly 12 hours later I can’t remember whether it choked on the input proper or during the tracing. Very well, then: spoiler

Is 32-bits a fixed standard for Ada’s Natural? Since 64-bit numbers are not uncommon in these puzzles (at least 2 or 3 puzzles will go there), should I by default define a numeric type and use that? (Isn’t that arguably the Ada way anyway? I’ve always wished the puzzle master would be more specific about the data we might encounter in these puzzles.)

The second speed bump is that solving Part 2 the natural, “brute-force” way takes the computer while, and I mean a while. It is doable! It took my machine “only” about 15 minutes. (I’ve paid for those gigahertz; might as well use them, right?)

So, while I was able to solve Part 2 via brute force – not usually possible when we start to see 6-digit numbers, let alone 9-digit ones! – I decided to spoiler.

My solution is here. I’d be interested to know if anyone took a different approach.

17 posts - 5 participants

Read full topic

I relied on enumerations. In both parts spoiler For part 2, I used spoiler
That, and a rewrite of the ordering in part 1, did the trick.

2 posts - 2 participants

Read full topic

Relatively straightforward. I suspected, correctly, that spoiler. Unfortunately, I incremented my step counter at the wrong time, so that I didn’t see spoiler.

4 posts - 2 participants

Read full topic

What a relief after yesterday’s puzzle!

• Kind of amusing how the puzzle master attempted to disguise spoiler. I recently completed the 2018 puzzles, and he made no attempt to disguise that.
• It amuses me that I guessed Part 2’s task while completing Part 1, so I went ahead and solved Part 1 with an approach that made it easy to complete Part 2 in about 5 minutes. The puzzle master’s love of throwing huge numbers into puzzles, which blocks a lot of obvious approaches, really helped foresee where this was going.
• That 5 minutes for Part 2 includes the minute I spent figuring out why my initial answer was wrong… spoiler

1 post - 1 participant

Read full topic

just kidding. but this one took me a long time. We seem to have entered the fiendishly difficult phase. Fortunately, difficult problems are usually followed by not-so-difficult ones. Usually.

• I first completed part 1 using a recursive algorithm that pruned failing branches. No problem, though it was a bit slow, so I knew what was coming next.
• Yup, Part 2 inflates the input to an insane size. The first record completed quickly, to my surprise but I quit the program after it dawdled on the second record for several minutes.
• I stared at it a while.
• Finally, I visited the Reddit solutions page. People were mentioning spoiler. What the heck is spoiler, thinks I, feeling a little humiliated at not knowing. Scrolling down a little, I see that someone else has the wherewithal to ask. It means spoiler. Oh yeah, says I, albeit a little more colorfully. (i.e., ) I remember something about that from my Algorithms class. But… how?
• Reading a bit more, I see what people say they are doing. Unfortunately, they are writing in languages like C++, D, Python, Rust. Excerpts range from illegible to incomprehensible out of their context. Probably doesn’t help that’s it’s 2am. Oooookayyyyy… time for a nap.

Thinking about it this evening, I realized that I could do the following.

1. For each line, iterate over the contiguous groups from left to right. So, start with the leftmost.
2. Assume the group records n damaged springs,
   • Determine spoiler.
   • For each i in 0 … spoiler A picture is probably worth 1000 words here: if n is 3, and spoiler, look at spoiler It is easy to tell whether this matches .#?#?.***
   • If it matches, take the next contiguous group and recurse (step 2) with an appropriate starting index for the next string. (Have I mentioned how I Ada’s custom indexing?.)
   • This is a key point. If you don’t want to wait forever, spoiler

A couple of additional complications I encountered:

• The result in part 2 is larger than Natural'Last on my input, so you’ll likely need something larger.
• If you use a hashed map for the spoiler, be prepared for some moding. I do wonder if I’d have done better with an ordered map.

There was more, but I can’t remember it now.

***I don’t recall reading this detail anywhere in the Reddit discussion of solutions, but then again, I don’t think so well at 2am. Either way, I’m pleased as punch that it seemed different.

3 posts - 2 participants

Read full topic

Correct loop termination bedeviled me. A spoiler which isn’t really a spoiler is that I’m pretty sure parts 1 and 2 can call the same subprograms, but testing for different things. I didn’t implement it that way, though.

3 posts - 2 participants

Read full topic

Fake spoiler: it didn’t require the use of the quadratic formula.

Not too difficult; I had more trouble with part 1 than with part 2. For part 2, spoiler

3 posts - 2 participants

Read full topic

First: this is pretty cool. I don’t remember the animations starting before the end of the competition.

Today’s puzzle would have wrecked me when I first started doing AoC puzzles, back in 2020. I must be learning something, as I managed it in relatively short time (less than two hours, all told), without having to run my code on the example.

I used the following tools, and I’m pretty sure that each, or some variant of each, is necessary.

• A beam can end up in an infinite loop. (I haven’t verified this, but I’m pretty sure it’s true.)
  • To prevent this, we need a way to verify the beam isn’t repeating previous steps; i.e., a beam tracker. But it’s not enough to spoiler, then it should keep moving.
  • When you get to Part 2, don’t forget to spoiler
• Splitting leads to new beams; my maximum number of beams was 65. Since we are spoiler

I’ll see if I can come up with a visualization of Part 2’s solution later. I did create a visualization for Day 14, but it wasn’t very helpful, and the forum rejected it as being too large an image, so I shrugged it off.

5 posts - 3 participants

Read full topic

I should have finished this much earlier, but my spoiler Nothing was helping me figure that out, not even comparing to known solutions! Then I noticed that there was a large gap between my previously-considered level of heat loss (1043 or so) and the reported result (1060) and the proverbial went off.

I might add more later, but for now, here’s a quick 'n dirty visualization of parts 1 and 2. Brighter shades indicate more heat loss. I’d be curious to know if other participants likewise see a “bulge” in their data, or if there’s a different pattern.

2 posts - 2 participants

Read full topic

Part 1 was pretty straightforward.

After several hours of looking at Part 2, it looks as if I had two really good ideas, but gave up on them too early. (Short on time lately.)

My favorite idea was to (spoiler). But when I applied it to the example, I realized, to my horror, that it depended on an unspoken assumption: spoiler. After starting at it a while and watching an hour or so go by, I despaired and gave up. I still like the idea (and apparently someone else did do it this way!), so I hope to return to it eventually.

Then I thought about trying a spoiler I still like that idea, but just as I was on the verge of implementing it I got cold feet. (From what I read, at least one person did something to this effect, too.)

As the hour drew very, very late, I visited the Reddit page and learned that most people seem to be solving it using spoiler… neither of which I’ve ever heard of. (I’d be embarrassed, since I have a PhD in mathematics, but someone else commented that he has a PhD in computational geometry, and he hadn’t heard of it either, so there.) But even that isn’t trivial; you can’t just copy & paste the formulas from Wikipedia. And since the same approach was useful on Day 10, these formulas may prove useful a third time.

I don’t suppose he’ll ever supply a puzzle that relies on my old research topics…

LOL, one person on the Reddit page says, “Finally, a relaxing day again…” That’s what I thought of the entire previous week between days 10 and 17…

4 posts - 2 participants

Read full topic

Today’s puzzle is cute:

To start, each part is rated in each of four categories:

* `x`: E*x*tremely cool looking
* `m`: *M*usical (it makes a noise when you hit it)
* `a`: *A*erodynamic
* `s`: *S*hiny

Kind of embarrassed how I didn’t notice what the categories “spelled out” at first.

I solved it in a manner similar to Day 5: spoiler

Using the original example:

• Start at in with intervals (1,4000),(1,4000),(1,4000),(1,4000).
• The rule s < 1351 applies, so spoiler

…and so forth. When a group visits A, add the group’s number of intervals to the running total; when a group visits R, spoiler.

6 posts - 3 participants

Read full topic

I usually look at the general leaderboard for each problem to get an impression of how difficult the “experts” find it. It surprises me that the general leaderboard for day 20 suggests that this has been the hardest problem so far: nearly 49 minutes for the first 100 participants to complete it! The only one that came close to this relative difficulty was day 10, with 36 minutes before the first 100 participants completed it.

Day 20 didn’t seem that complicated to me. So long as you read the problem carefully, and I do mean carefully, part 1 is possibly the most straightforward problem yet. The only thing that makes part 2 challenging is that the answer is a “ludicrous size” number, so you don’t want to wait around for it. But the technique to make it work has already been used with other problems: spoiler

1 post - 1 participant

Read full topic

I’ve only finished Part 1 so far, but here are some thoughts on Part 2. While it’s not implemented yet, it should be the right track: when testing it by hand on a much smaller example, I come too close to the brute-force answer to make me think the mistakes are anything other than due to hand computation / numbers-slightly-off / etc.

Sorry if this seems far too long, too detailed, or too annoying with blurred spoilers-which-perhaps-aren’t, but if anyone sees an invalid assumption, I would be grateful!

• Once the elf visits a plot, he cannot visit it again except on multiples of 2, on account of the limited number of directions available. That is, if he first visits the plot in row 5, column 12 on step 7, then he will only visit that plot on odd-numbered steps.
• In my input, and I suspect in all inputs, the number of steps is 65 + x * 131, where x is a Very Large Number , 131 is the dimension of the square, and 65 is the number of steps it takes to get from the starting point, which is in the middle, to the end of the square.
• Unlike the example – and this is a big deal! – spoiler
• As the elf explores, you get spoiler

• You can thus consider separately squares spoiler
• Rspoiler the number of squares visited in the cardinal directions, but they’re not all full: spoiler We’ll return to this speed bump in a moment.
• In each column not in a cardinal direction (e.g., the column with squares G, E, and C; or, the column with just G and E), spoiler
• So it’s relatively easy to count the number of full squares, spoiler That product gives the number of plots the elf can visit in all the full squares. spoiler
• Likewise, it should be relatively easy to brute-force count the number of plots the elf visits in squares that aren’t full, because you know the shortest number of steps it takes to arrive there, and you can explore from that entrace position. Again, the fact that movement is limited to the cardinal directions helps you here: in a box to the northwest of A, for instance, the earliest entrance is in a southeast corner, so explore from there for the number of steps remaining.
• Add the values in these last two steps and you should have the answer.

I suspect the reason my hand computation is wrong is that I’m slightly off on the next-to-last step. I’ll look at it more later…

5 posts - 2 participants

Read full topic