MathEvidence/lakefile.toml at main · fraware/MathEvidence · 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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
name = "MathEvidence"
version = "0.1.0"
defaultTargets = [
  "MathEvidenceCore",
  "MathEvidenceIR",
  "MathEvidenceEncoding",
  "MathEvidenceCheckers",
  "MathEvidenceHypothesis",
  "MathEvidenceConjecture",
  "MathEvidenceTraceToPlan",
  "MathEvidenceAssurance",
  "MathEvidenceTactic",
  "MathEvidenceRegistry",
  "MathEvidenceTesting",
]

# Pin Mathlib to the Lean 4.14.0 release commit (matches lean-toolchain).
# Prefer the mathlib4 git URL + commit SHA over Reservoir `scope` + tag:
# a corrupted local `.lake/packages/mathlib` pointing at this repo previously
# made Lake report "revision not found 'v4.14.0'" even though the upstream
# tag exists (leanprover-community/mathlib4@v4.14.0 -> 4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84).
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84"

# Each lean_lib is a MathEvidence.* package boundary. Roots pull in submodules
# via import; avoid globs here so Lake 5 reliably builds the barrel modules.

[[lean_lib]]
name = "MathEvidenceCore"
roots = ["MathEvidence.Core"]

[[lean_lib]]
name = "MathEvidenceIR"
roots = ["MathEvidence.IR"]

[[lean_lib]]
name = "MathEvidenceEncoding"
roots = ["MathEvidence.Encoding"]

[[lean_lib]]
name = "MathEvidenceCheckers"
roots = ["MathEvidence.Checkers"]

[[lean_lib]]
name = "MathEvidenceHypothesis"
roots = ["MathEvidence.Hypothesis"]

[[lean_lib]]
name = "MathEvidenceConjecture"
roots = ["MathEvidence.Conjecture"]

[[lean_lib]]
name = "MathEvidenceTraceToPlan"
roots = ["MathEvidence.TraceToPlan"]

[[lean_lib]]
name = "MathEvidenceAssurance"
roots = ["MathEvidence.Assurance"]

[[lean_lib]]
name = "MathEvidenceTactic"
roots = ["MathEvidence.Tactic"]

[[lean_lib]]
name = "MathEvidenceRegistry"
roots = ["MathEvidence.Registry"]

[[lean_lib]]
name = "MathEvidenceTesting"
roots = ["MathEvidence.Testing"]

[[lean_exe]]
name = "mathevidence-verify-bundle"
root = "MathEvidence.Exe.Replay"

# Temporary alias — Wave 0 keeps the old name until call sites migrate fully.
[[lean_exe]]
name = "mathevidence-replay"
root = "MathEvidence.Exe.Replay"

# Theorem-producing kernel replay (ME-RV-022). Protocol-reference fixture is
# compiled into the exe; general bundles use the Python generated-module driver.
[[lean_exe]]
name = "mathevidence-kernel-replay"
root = "MathEvidence.Exe.KernelReplay"

# Post-elaboration declaration inspector. Certification orchestration calls this
# after compiling a generated replay module; theorem/proof identity is derived
# from the ConstantInfo stored in a freshly imported Lean.Environment.
[[lean_exe]]
name = "mathevidence-declaration-identity"
root = "MathEvidence.Exe.DeclarationIdentity"
supportInterpreter = true

[[lean_exe]]
name = "mathevidence-axiom-report"
root = "MathEvidence.Exe.AxiomReport"
# Required for Lean.importModules / CollectAxioms at runtime (ME-RV-071/072).
supportInterpreter = true

[[lean_exe]]
name = "mathevidence-import-graph"
root = "MathEvidence.Exe.ImportGraph"
# Required for Lean.importModules at runtime (ME-RV-071).
supportInterpreter = true