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

1 post - 1 participant

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

@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

(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

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

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

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

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 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 do the following, per the Alire Quickstart instructions:

alr init --bin my_proj
cd my_proj
alr build
alr run

Next I try to edit it:

alr edit

The most recent gnatstudio is in my path, so the editor pops up in the crate. Trouble is, it doesn’t seem to understand the project file at all. (Screenshot below.) To wit:

• src has a source file in it, but the icon isn’t expandable.
• While there are “build” and “run” buttons, they doesn’t actually build and run the program; rather, they seem good only for generating Uncaught Exceptions; see output below.
• This is not a problem with pre-existing alire crates; it’s only a problem for anything I try to generate now.

Weirdly, this was working earlier today, which makes me think I broke something at some point. Does anyone have any suggestions for figuring out how to fix it?

Uncaught exception in workflows:
Traceback (most recent call last):
  File "/path/to/opt/gnatstudio/share/gnatstudio/support/ui/workflow_buttons.py", line 133, in build_main
    r0 = yield builder.wait_on_execute(main_name)
  File "/path/to/opt/gnatstudio/share/gnatstudio/support/ui/workflows/promises.py", line 1108, in wait_on_execute
    self.__target.execute(main_name=main_name,
  File "/path/to/opt/gnatstudio/share/gnatstudio/support/core/extensions/__init__.py", line 380, in execute
    self._internal_execute(
GPS.Unexpected_Exception: unexpected internal exception raised CONSTRAINT_ERROR : gnatcoll-projects.adb:5729 index check failed
[/path/to/opt/gnatstudio/bin/../lib/gnatstudio/libgnatcoll.so.23.0w]
0x7f1c6cc179c1 gnatcoll__projects__compute_scenario_variables__register_untyped_var.1798.constprop.0 at ???
0x7f1c6cc17d06 gnatcoll__projects__compute_scenario_variables__register_var.1778 at ???
0x7f1c6cc238c7 gnatcoll__projects__for_each_external_variable_declaration at ???
0x7f1c6cc26235 gnatcoll__projects__compute_scenario_variables at ???
0x7f1c6cc271aa gnatcoll__projects__scenario_variables__3.part.0 at ???
0x7f1c6cc27319 gnatcoll__projects__scenario_variables at ???
[/path/to/opt/gnatstudio/bin/gnatstudio_exe]
0x3cdd374

…and after that, a bunch more hexadecimal numbers and suchnot.

6 posts - 3 participants

Read full topic

I’m not sure why he didn’t call this one SNAFU, but it was easy and fun, which I think is typical on Day 25.

Anyone add up the numbers using SNAFU arithmetic, or did everyone convert to decimal, add, then convert back?

PS If I may be allowed a personal remark: This is my third time doing AoC, but the first one I’ve completed it in time: for the 2020 competition I finished up around New Year’s instead of Christmas Day; then I went back and completed the 2019 competition, and then I took a break until this year. Having thsi forum to discuss things with, even to vent frustration once or twice, was helpful. I really enjoyed learning from everyone. Maybe I’ll go back and complete some other years… after getting some first.

4 posts - 4 participants

Read full topic

Part 1 is another spoiler. I wasted too much time getting the blizzard logic wrong. I knew what to do; I just kept getting the math wrong! I did at least have the presence of mind spoiler.

Part 2 was also pretty straightforward, once Part 1 is done. Interesting that the result is not three times the value of Part 1, but not especially surprising, given how the blizzards move around.

Glancing over at the Reddit Solutions Megathread, some commenters have noticed that spoiler (It certainly would be in my case.)

9 posts - 4 participants

Read full topic

Another one that I thought was fun! The input proved helpful, and was not so different from the example today as it was yesterday. Then again, it would be hard to diverge as greatly from the example to the input as yesterday did…

My solution spoiler To determine the direction an elf considers, spoiler

Is there a way to determine how many variants an enumerated type has?

I have an idea for a visualization, and if I find time I’ll do it later.

Added later: Now that I review the discussion on Reddit, I notice that a lot of people missed something that I almost missed myself: spoiler Yeah, watch out for that.

11 posts - 4 participants

Read full topic

This was fun. Even the debugging was fun. Even though the example was once again naughty, at least for Part 2, this was fun. (If anyone’s input creates a cube in the same way as the example, I’d like to know!)

Only one hint / comment from me: in part 2, spoiler.

I thought about drawing the paths onto the map, but it’s pretty late where I am, so maybe tomorrow. In lieu of that, here’s an aid I made to help with Part 2.

3 days left!

10 posts - 3 participants

Read full topic

I really enjoyed today’s puzzle! Observations / hints / spoilers:

• The example does not cover all the cases you need to check in Part 2. Interestingly, the input is relatively small if you look at it right, so even though I got Part 2 wrong the first time, it didn’t take me long to work through the example and find my mistake.
• In part 1, spoiler
• In part 2, spoiler

4 days left!!!

7 posts - 4 participants

Read full topic

(edited after remembering another bad idea, whoops)

I had one very good idea, one good idea, and quite a few bad ideas, including one very bad idea that held me up a long time.

• The very good idea was spoiler As a result, the solution to both parts takes only less than two seconds (using full optimization and inlining).
• The good idea I don’t quite remember, sorry, but I had it in mind at one point.
• One bad idea was spoiler. Fortunately, I caught that one quickly.
• Another bad idea was spoiler Rather naughty of the example not to have a value that would illustrate that.
• The very bad idea came while testing my code on the example. spoiler I wasted over an hour on that stupid mistake…

8 posts - 4 participants

Read full topic

Nope. I’ve been at this for hours.

• I wasted hours just trying to get my code to run the example in a reasonable time, and when I gave up I discovered that the input takes not much longer to run than the example.

  So there’s a hint that doesn’t require a spoiler: don’t bother trying to get your program to work on the example in seconds; the input isn’t that much harder! Just try to get the program to work on the example, period!

• Unfortunately, that’s not enough. The example doesn’t really illuminate the problem. Your code can run correctly on the example and run incorrectly on the problem input. This happens from time to time, but on a problem like today it’s ruinous.

• To help me debug my program, I downloaded and ran several people’s solutions posted online (in other languages). I haven’t tried any of the solutions, but there’s a morbid satisfaction in the fact that different “solutions” produce different results on my input.

• Some authors admit that they guessed at optimizations and got lucky; the optimizations probably don’t work in general. I’ve tried a few, and nope, they don’t work on my input (unless I’m implementing them wrong).

• Some authors used parallelism. I may yet try that, since the problem is parallelizable, and otherwise I have to wait 5-10 minutes per attempt.

In short, I haven’t finished it yet. IMHO the puzzle is terribly flawed, for the reasons given above. And, yeah, sour grapes, too.

8 posts - 3 participants

Read full topic

I use Ada for my personal projects, largely out of admiration for the language, but I’m entirely self-taught in Ada, and the literature on its usage is… well, somewhat scant in comparison to, say, C++.

Not every language is perfect, but some things in the standard Ada library seem far too cumbersome. So much so, that I have to wonder if I’m doing things right. I’ve looked at the ARM, perhaps not well, and rosetta code is down at the moment, so I thought I’d inquire here.

Queues

Setting up a queue seems to involve way more effort than it should:

• You have to include two separate packages:
  • Containers.Synchronized_Queue_Interfaces
  • Containers.Unbounded_Synchronized_Queues or one of the other three variants
• You have to use all type Ada.Containers.Count_Type if you want to check whether it’s empty.

The payoff? For all the effort you put into creating it, the resulting queue offers less functionality than other languages’. All you can do is Enqueue, Dequeue, and check usage. You can’t iterate through the queue to see what’s there and possibly modify it, nor search through it, let alone split the queue. There isn’t even an .Is_Empty method to tell you when it’s exhausted.

Queues are pretty common, and I’ve never seen one so bare bones. Is there something more functional than this in the standard library? If not, do people recommend a different library (e.g,. the Simple Components library) or do you typically roll your own?

(I realize there may be good reasons for the library to do things this way; I’m just wondering what people do about it.)

Iteration through maps

Suppose I set up a map M and want to iterate through it.

• for E of M iterates through the map’s elements, not through its keys. I wish they had returned the keys instead, since often that’s what I want, and it’s easy to obtain the elements from the keys, and not so much the converse. But this does make sense.
• for C in M.Iterate iterates a cursor through the key/pair combinations. This makes sense, too. But…
• Using Cursor is, again, cumbersome. As far as I can tell, I can’t do this: C.Key or C.Element. Instead, I have to with all type Map_Type.Cursor to get Key(C) and Element(C), or else qualify the functions fully: Map_Type.Key(C) or Map_Type.Element(C).

(I think Ada 2022 introduces functionality to let me treat a cursor the way I want, but if so, I have to update my gnat: version 20210519-103.)

So what am I doing wrong?

Have I missed something, or is this indeed the standard way of doing these things in Ada? I would be grateful for any direction, because I don’t use Ada often enough to remember these two things, and the compiler’s help error messages are not the greatest.

Honestly!

I apologize if it comes across as a complaint. I realize there’s no perfect language, and just want to know if I’m missing something, because Ada does so many things right. I can make much, much longer lists of my complaints with C++, and a somewhat longer list of complaints with Rust, than I can with Ada.

9 posts - 4 participants

Read full topic

Part 1 is pretty straightforward, I think.

Part 2 requires some mathematics, or at least that’s what got me to solve it quite quickly I did one other thing, too.

1. spoiler
2. spoiler
3. spoiler

The solution I uploaded for part 2 will probably not work on the example program, because the example’s sequences aren’t quite as well-behaved as the actual puzzle, which made the problem a little harder. But the same technique really does work!

2 posts - 2 participants

Read full topic