Skip to content

Commit fa0eaa0

Browse files
JonathangadeaharderJonathangadeaharder
authored
feat: add leanblueprint setup with GitHub Pages deployment
LeanBlueprint LaTeX dependency graph for the formalization. Deploys to GitHub Pages on push to master.
2 parents b089a3d + f1c5120 commit fa0eaa0

34 files changed

Lines changed: 2411 additions & 49 deletions

‎.github/workflows/blueprint.yml‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
name: Blueprint to GitHub Pages
2+
3+
on:
4+
push:
5+
branches: [master]
6+
workflow_dispatch:
7+
8+
permissions:
9+
contents: read
10+
pages: write
11+
id-token: write
12+
13+
concurrency:
14+
group: "pages"
15+
cancel-in-progress: false
16+
17+
jobs:
18+
build:
19+
runs-on: ubuntu-latest
20+
steps:
21+
- name: Checkout
22+
uses: actions/checkout@v4
23+
24+
- name: Install Elan
25+
run: |
26+
curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
27+
echo "$HOME/.elan/bin" >> $GITHUB_PATH
28+
29+
- name: Cache Mathlib
30+
uses: actions/cache@v4
31+
with:
32+
path: |
33+
.lake/packages/mathlib
34+
.lake/build
35+
key: lake-${{ runner.os }}-${{ hashFiles('lakefile.lean', 'lake-manifest.json', 'lean-toolchain') }}
36+
restore-keys: lake-${{ runner.os }}-
37+
38+
- name: Build project
39+
run: lake build
40+
41+
- name: Install Python dependencies
42+
run: |
43+
pip install leanblueprint
44+
45+
- name: Install LaTeX
46+
run: |
47+
sudo apt-get update
48+
sudo apt-get install -y texlive-full
49+
50+
- name: Build blueprint web
51+
run: leanblueprint web
52+
53+
- name: Upload artifact
54+
uses: actions/upload-pages-artifact@v3
55+
with:
56+
path: blueprint/web
57+
58+
deploy:
59+
environment:
60+
name: github-pages
61+
url: ${{ steps.deployment.outputs.page_url }}
62+
runs-on: ubuntu-latest
63+
needs: build
64+
steps:
65+
- name: Deploy to GitHub Pages
66+
id: deployment
67+
uses: actions/deploy-pages@v4

‎.github/workflows/ci.yml‎

Lines changed: 24 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,22 +2,25 @@ name: Lean CI
22

33
on:
44
push:
5-
branches: [master, peer-review-fixes]
5+
branches:
6+
- master
7+
- peer-review-fixes
8+
- 'epic/**'
69
pull_request:
710
branches: [master]
811

912
jobs:
1013
build-and-verify:
11-
runs-on: ubuntu-latest
14+
runs-on: macos-latest
1215
name: Build & Verify Formalization
16+
timeout-minutes: 25
1317
steps:
1418
- name: Checkout
1519
uses: actions/checkout@v4
1620

1721
- name: Install Elan
1822
run: |
19-
curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.6/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
20-
./elan-init -y --default-toolchain none
23+
curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
2124
echo "$HOME/.elan/bin" >> $GITHUB_PATH
2225
2326
- name: Cache Mathlib
@@ -83,6 +86,20 @@ jobs:
8386
echo "No admit found."
8487
echo "::endgroup::"
8588
89+
- name: Check for native_decide
90+
run: |
91+
echo "::group::Searching for native_decide"
92+
FOUND=$(grep -rn 'native_decide' --include='*.lean' . \
93+
| grep -v '\.lake/packages/' \
94+
|| true)
95+
if [ -n "$FOUND" ]; then
96+
echo "::error::Found native_decide in Lean sources (bypasses kernel — use decide instead)"
97+
echo "$FOUND"
98+
exit 1
99+
fi
100+
echo "No native_decide found."
101+
echo "::endgroup::"
102+
86103
- name: Mechanization completeness audit
87104
run: |
88105
echo "::group::Mechanization completeness audit"
@@ -131,7 +148,6 @@ jobs:
131148
echo "=== Skipped (known gaps — not enforced) ==="
132149
echo " ⊘ Thm 9: ND coupling → E[T_X] = 2^Ω(n)"
133150
echo " ⊘ Thm 8: LBT coupling → E[T_X] = O(n log n)"
134-
echo " ⊘ SignedEpistasisSkeleton: module placeholder"
135151
136152
echo ""
137153
if [ $ERRORS -gt 0 ]; then
@@ -150,9 +166,11 @@ jobs:
150166
SORRY_COUNT=$(grep -rn 'sorry' --include='*.lean' . | grep -v '\.lake/packages/' | grep -v '^Binary' | wc -l || true)
151167
AXIOM_COUNT=$(grep -rnE '^\s*(private\s+|protected\s+|noncomputable\s+)*axiom\b' --include='*.lean' . | grep -v '\.lake/packages/' | wc -l || true)
152168
ADMIT_COUNT=$(grep -rn 'admit' --include='*.lean' . | grep -v '\.lake/packages/' | grep -v 'sorry_admit' | wc -l || true)
169+
NATIVE_DECIDE_COUNT=$(grep -rn 'native_decide' --include='*.lean' . | grep -v '\.lake/packages/' | wc -l || true)
153170
echo "- **Lean source files:** ${LEAN_FILES}" >> $GITHUB_STEP_SUMMARY
154171
echo "- **Total lines:** ${TOTAL_LINES}" >> $GITHUB_STEP_SUMMARY
155-
echo "- **sorry count:** ${SORRY_COUNT}" >> $GITHUB_STEP_SUMMARY
172+
echo "- **sorry count:** ${SORRY_COUNT} (3 documented deferred proofs in LBTCoupling.lean)" >> $GITHUB_STEP_SUMMARY
156173
echo "- **axiom count:** ${AXIOM_COUNT}" >> $GITHUB_STEP_SUMMARY
157174
echo "- **admit count:** ${ADMIT_COUNT}" >> $GITHUB_STEP_SUMMARY
175+
echo "- **native_decide count:** ${NATIVE_DECIDE_COUNT}" >> $GITHUB_STEP_SUMMARY
158176
echo "- **required theorem:** Proposition 1 (r_local_tightness_all_pairs_misranked)" >> $GITHUB_STEP_SUMMARY

‎LintOptions.lean‎

Lines changed: 43 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -1,28 +1,43 @@
1-
/-!
2-
# Global Lint Options for Formal Verification Hardening
3-
4-
These options enforce strict variable tracking and tactic hygiene across
5-
all modules in the CoEA Level-Based formalization. Every `.lean` file
6-
in the project must `import LintOptions` to inherit these constraints.
7-
8-
## Paper Reference
9-
Derived from: "Formally Verified Artificial Intelligence: Exhaustive Protocols
10-
for Detecting and Preventing Heuristic Cheating in Lean 4 Proof Generation"
11-
-/
12-
13-
-- ============================================================
14-
-- STRICT VARIABLE TRACKING
15-
-- ============================================================
16-
-- Forces the compiler to flag any declared variable that fails
17-
-- to structurally propagate through the proof body.
18-
19-
set_option linter.unusedVariables true
20-
set_option linter.unusedVariables.funArgs true
21-
set_option linter.unusedVariables.patternVars true
22-
23-
-- ============================================================
24-
-- NOTE: Tactic bloat detection is handled externally by
25-
-- semantic_linter.py (Rule 8) since linter.unusedTactic
26-
-- is not available in this Lean 4 version.
27-
-- ============================================================
28-
1+
/-!
2+
# Global Lint Options for Formal Verification Hardening
3+
4+
These options enforce strict variable tracking and tactic hygiene across
5+
all modules in the CoEA Level-Based formalization. Every `.lean` file
6+
in the project must `import LintOptions` to inherit these constraints.
7+
8+
## Enforced checks
9+
10+
1. **Unused variables** — any declared variable that does not appear in the
11+
proof body is flagged by the compiler.
12+
2. **Function argument tracking** — unused function arguments are flagged.
13+
3. **Pattern variable tracking** — unused pattern-match binders are flagged.
14+
15+
## CI enforcement (additional, external)
16+
17+
The `.github/workflows/ci.yml` pipeline enforces:
18+
- `sorry` — forbidden outside `LBTCoupling.lean` (three documented deferred proofs)
19+
- `axiom` declarations — forbidden in all project files
20+
- `admit` — forbidden in all project files
21+
- `native_decide` — forbidden in all project files (bypasses the Lean kernel)
22+
23+
## Paper Reference
24+
Derived from: "Formally Verified Artificial Intelligence: Exhaustive Protocols
25+
for Detecting and Preventing Heuristic Cheating in Lean 4 Proof Generation"
26+
-/
27+
28+
-- ============================================================
29+
-- STRICT VARIABLE TRACKING
30+
-- ============================================================
31+
-- Forces the compiler to flag any declared variable that fails
32+
-- to structurally propagate through the proof body.
33+
34+
set_option linter.unusedVariables true
35+
set_option linter.unusedVariables.funArgs true
36+
set_option linter.unusedVariables.patternVars true
37+
38+
-- ============================================================
39+
-- NOTE: native_decide is banned via CI (see ci.yml).
40+
-- It bypasses the Lean kernel by compiling to native code,
41+
-- so proofs using it are not kernel-checked.
42+
-- Use `decide` (kernel-checked) instead.
43+
-- ============================================================

‎blueprint/src/blueprint.sty‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
\DeclareOption*{}
2+
\ProcessOptions
3+
4+
\newcommand{\graphcolor}[3]{}

0 commit comments

Comments
 (0)