summaryrefslogtreecommitdiff
path: root/lakefile.lean
blob: e89dba4d58b317ade75a78f38f73c2eef37103e0 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
import Lake
open Lake DSL

package «aoc-2023» where

lean_lib «Day1» where
lean_lib «Day2» where
lean_lib «Day3» where
lean_lib «Day4» where
lean_lib «Day5» where
lean_lib «Day6» where
lean_lib «Day7» where
lean_lib «Day8» where
lean_lib «Day9» where
lean_lib «Day10» where
lean_lib «Day11» where
lean_lib «Day12» where
lean_lib «Day13» where
lean_lib «Day14» where
lean_lib «Day15» where
lean_lib «Day16» where
lean_lib «Day17» where

lean_lib «Common» where

@[default_target]
lean_exe «aoc-2023» where
  root := `Main
  -- Enables the use of the Lean interpreter by the executable (e.g.,
  -- `runFrontend`) at the expense of increased binary size on Linux.
  -- Remove this line if you do not need such functionality.
  supportInterpreter := true

require BinaryHeap from git
  "http://git.grois.info/BinaryHeap"@"ff5c64836ede27d87dbc56b3869021ad8b0d255b"

require «lean-astar» from git
  "http://git.grois.info/lean-astar"@"2539ac49ab6af74b31d91e03d7dbfceedc9c1f02"