Advent of Code 2024

Advent of Code
21

[zertovitch][1][Ada] (examples) Added Advent of Code 2024, Day 1 · zertovitch/hac@1e444b9 · GitHub

22

[JeremyGrosser][1][Ada] advent/2024/src/day1_2.adb at 8571ee23485b41d452494300974a367e6e980a05 · JeremyGrosser/advent · GitHub
[JeremyGrosser][2][Ada] advent/2024/src/day2_2.adb at 8571ee23485b41d452494300974a367e6e980a05 · JeremyGrosser/advent · GitHub

1 Like
23

[cunger][2][Ada] 100hoursofada/aoc2024/src/02 at main · cunger/100hoursofada · GitHub

No SPARK today, as vectors are not allowed in SPARK.

1 Like
24

@cunger you can use the spark_unbound crate which provides a proven alternative to Ada.Containers.Vector.

2 Likes
25

[jcmoyer][2][Ada] puzzles/AdventOfCode2024/src/day02.adb at 3a75c7b5afa84c667088cdfa360ad79baae227fa · jcmoyer/puzzles · GitHub

26

Part one:

[alexispaez][2][Ada]advent-of-code/2024/day_2_1/src/day_2_1.adb at 054384968a78a6827e46709eefb1018d4d4503f9 · alexispaez/advent-of-code · GitHub

And part two:

[alexispaez][2][Ada]advent-of-code/2024/day_2_2/src/day_2_2.adb at master · alexispaez/advent-of-code · GitHub

27

[zsoltiv][1][Ada]aoc2024/day1.adb at a994ca81c44bf16635fb6875c7ddca4870a01213 · zsoltiv/aoc2024 · GitHub
[zsoltiv][2][Ada]aoc2024/day2.adb at a994ca81c44bf16635fb6875c7ddca4870a01213 · zsoltiv/aoc2024 · GitHub

1 Like
28

Thanks for the pointer! I replaced my vectors with those unbound arrays and use them as follows, but based on this definition I get a lot of errors about what cannot be proven in the spark_unbound-arrays.ads. I’m a bit lost how I can make it easier on the prover - and in general, I think I need to start much simpler… :sweat_smile:

   type Levels is range 1 .. 10;

   package Arrays is new Spark_Unbound.Arrays (
      Index_Type   => Levels,
      Element_Type => Natural
   );
29

Part 1: [tgv][02][Ada]aoc2024/aoc202402a at master · theovosse/aoc2024 · GitHub

Part 2: [tgv][02][Ada]aoc2024/aoc202402b at master · theovosse/aoc2024 · GitHub

30

[zertovitch][2][Ada] (examples) Added Advent of Code 2024, Day 2 · zertovitch/hac@a26c0fe · GitHub

31

[Daniel-Larraz][2][SPARK]https://github.com/daniel-larraz/advent-of-code/tree/main/2024/Ada/day02

1 Like
32

Alternatively, you can use SPARK.Containers.Formal.Unbounded_Vectors. I used it to implement my solutions to the Day 1 and Day 2 puzzles in SPARK. The SPARK library is installed together with the gnatprove crate, but you need to add this GPR file to your project and include it in your main GPR file.

2 Likes
34

[JeremyGrosser][3][Ada] advent/2024/src/day3_2.adb at c50aa046df3ffebd26cf525fd53d6ebb8d89bc25 · JeremyGrosser/advent · GitHub

35

[zertovitch][3][Ada] (examples) Added Advent of Code 2024, Day 03 - and 100th regression t… · zertovitch/hac@932d987 · GitHub

36

[cunger][3][Ada] 100hoursofada/aoc2024/src/03/aoc2024_03.adb at fc23ee7c9aab6bdf490a8a961eb50796c6423023 · cunger/100hoursofada · GitHub

(SPARK still pending, I’m slowly figuring things out…)

37

[jcmoyer][3][Ada] puzzles/AdventOfCode2024/src/day03.adb at 28e953807e27b67d9a5dca2f1901d9d0ed09cdb8 · jcmoyer/puzzles · GitHub

38

Part 1:
[alexispaez][3][Ada]advent-of-code/2024/day_3_1/src/day_3_1.adb at 4e254b80eb1c4db029385ddb11a89f25f853ba0a · alexispaez/advent-of-code · GitHub

Part 2:
[alexispaez][3][Ada]advent-of-code/2024/day_3_2/src/day_3_2.adb at master · alexispaez/advent-of-code · GitHub

39

Part 1: [tgv][03][Ada]aoc2024/aoc202403a at master · theovosse/aoc2024 · GitHub

Part 2: [tgv][03][Ada]aoc2024/aoc202403b at master · theovosse/aoc2024 · GitHub

40

[Irvise][02][Ada]advent-of-code-2024/day_2/src/main.adb at e3e03cbf56a316322a351da71ebbbc74f755178b · Irvise/advent-of-code-2024 · GitHub

41

[Chris660][3][Ada] part 1: AOC-2024/Day_03/part1.adb at 68a45b134a73ea319a5ef73fe6a4dfb4b250ede9 · Chris660/AOC-2024 · GitHub
[Chris660][3][Ada] part 2: AOC-2024/Day_03/part2.adb at 68a45b134a73ea319a5ef73fe6a4dfb4b250ede9 · Chris660/AOC-2024 · GitHub

[Chris660][4][Ada] part 1: AOC-2024/Day_04/part1.adb at ef8dcddff05584621849739e4736bf5cc3d80668 · Chris660/AOC-2024 · GitHub