compfiles/lakefile.toml at main · XC0R/compfiles · GitHub

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
39
40
41
name = "compfiles"
defaultTargets = ["ProblemExtraction", "Compfiles", "buildWebpage", "extractProblems", "checkSolution"]

[leanOptions]
pp.unicode.fun = true
autoImplicit = false
relaxedAutoImplicit = false
weak.linter.style.multiGoal = true
weak.linter.style.cdot = true
weak.linter.tacticAnalysis.tryAtEachStepFromEnv = true

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4"
rev = "master"

[[require]]
name = "tryAtEachStep"
git = "https://github.com/dwrensha/tryAtEachStep"
rev = "main"

[[lean_lib]]
name = "ProblemExtraction"

[[lean_lib]]
name = "Compfiles"

[[lean_exe]]
name = "buildWebpage"
root = "scripts.buildWebpage"
supportInterpreter = true

[[lean_exe]]
name = "extractProblems"
root = "scripts.extractProblems"
supportInterpreter = true

[[lean_exe]]
name = "checkSolution"
root = "scripts.checkSolution"
supportInterpreter = true