Skip to content

Commit 66d2adb

Browse files
JonathangadeaharderJonathan Gadea Harder
Jonathangadeaharder
and
Jonathan Gadea Harder
authored
feat: add quality gates CI/CD for Lean 4 project (#23)
- pr-gate.yml: format, lint, build, verification audit, semgrep, CodeQL - merge-gate.yml: same minus non-merge-specific, on push to master - codeql.yml: weekly + per-PR security analysis - .semgrep.yml: Lean-aware SAST rules (sorry, axiom, admit, native_decide) - .jscpd.json: copy-paste detection config for Lean sources - sonar-project.properties: SonarCloud integration All pr-gate jobs guarded against fork PRs. Co-authored-by: Jonathan Gadea Harder <jonathangadeaharder@Jonathans-MacBook-Pro.local>
1 parent edff444 commit 66d2adb

6 files changed

Lines changed: 537 additions & 0 deletions

File tree

‎.github/workflows/codeql.yml‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
name: CodeQL Security Analysis
2+
3+
on:
4+
push:
5+
branches: [master]
6+
pull_request:
7+
branches: [master]
8+
schedule:
9+
- cron: '0 6 * * 1' # Weekly: Monday 06:00 UTC
10+
11+
jobs:
12+
analyze:
13+
runs-on: ubuntu-latest
14+
permissions:
15+
security-events: write
16+
actions: read
17+
contents: read
18+
timeout-minutes: 30
19+
20+
strategy:
21+
fail-fast: false
22+
matrix:
23+
language: [cpp]
24+
25+
steps:
26+
- uses: actions/checkout@v4
27+
28+
- uses: github/codeql-action/init@v3
29+
with:
30+
languages: ${{ matrix.language }}
31+
queries: security-and-quality
32+
33+
- uses: github/codeql-action/analyze@v3

‎.github/workflows/merge-gate.yml‎

Lines changed: 199 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,199 @@
1+
name: Merge Gate
2+
3+
on:
4+
push:
5+
branches: [master]
6+
7+
concurrency:
8+
group: ${{ github.workflow }}-${{ github.ref }}
9+
cancel-in-progress: true
10+
11+
jobs:
12+
format:
13+
runs-on: ["self-hosted", "macos", "arm64", "VidiomTM"]
14+
name: Format Check
15+
timeout-minutes: 15
16+
steps:
17+
- uses: actions/checkout@v4
18+
- name: Install Elan
19+
run: |
20+
which elan 2>/dev/null || { curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none; }
21+
echo "$HOME/.elan/bin" >> $GITHUB_PATH
22+
- name: Symlink .lake cache
23+
run: |
24+
CACHE_DIR="$HOME/.cache/lean-runtime-analysis/lake"
25+
mkdir -p "$CACHE_DIR"
26+
if [ -d .lake ] && [ ! -L .lake ]; then
27+
rsync -a .lake/ "$CACHE_DIR/" 2>/dev/null || true
28+
rm -rf .lake
29+
fi
30+
ln -sfn "$CACHE_DIR" .lake
31+
- name: Check formatting
32+
run: lake fmt --check
33+
34+
lint:
35+
runs-on: ["self-hosted", "macos", "arm64", "VidiomTM"]
36+
name: Lint
37+
timeout-minutes: 25
38+
steps:
39+
- uses: actions/checkout@v4
40+
- name: Install Elan
41+
run: |
42+
which elan 2>/dev/null || { curl -sSfL https://raw.githubusercontent.com/leanprover/lean/master/elan-init.sh | sh -s -- -y --default-toolchain none; }
43+
echo "$HOME/.elan/bin" >> $GITHUB_PATH
44+
- name: Symlink .lake cache
45+
run: |
46+
CACHE_DIR="$HOME/.cache/lean-runtime-analysis/lake"
47+
mkdir -p "$CACHE_DIR"
48+
if [ -d .lake ] && [ ! -L .lake ]; then
49+
rsync -a .lake/ "$CACHE_DIR/" 2>/dev/null || true
50+
rm -rf .lake
51+
fi
52+
ln -sfn "$CACHE_DIR" .lake
53+
- name: Run lint
54+
run: lake lint
55+
- name: Check for sorry (outside LBTCoupling.lean)
56+
run: |
57+
FOUND=$(grep -rn 'sorry' --include='*.lean' . \
58+
| grep -v '\.lake/packages/' \
59+
| grep -v '^Binary' \
60+
| grep -v 'LBTCoupling.lean' \
61+
|| true)
62+
if [ -n "$FOUND" ]; then
63+
echo "::error::Found sorry in Lean sources (outside LBTCoupling.lean)"
64+
echo "$FOUND"
65+
exit 1
66+
fi
67+
- name: Check for axiom declarations
68+
run: |
69+
FOUND=$(grep -rnE '^\s*(private\s+|protected\s+|noncomputable\s+)*axiom\b' --include='*.lean' . \
70+
| grep -v '\.lake/packages/' \
71+
|| true)
72+
if [ -n "$FOUND" ]; then
73+
echo "::error::Found axiom declarations"
74+
echo "$FOUND"
75+
exit 1
76+
fi
77+
- name: Check for admit
78+
run: |
79+
FOUND=$(grep -rn 'admit' --include='*.lean' . \
80+
| grep -v '\.lake/packages/' \
81+
| grep -v 'sorry_admit' \
82+
| grep -v 'LintOptions.lean' \
83+
|| true)
84+
if [ -n "$FOUND" ]; then
85+
echo "::error::Found admit"
86+
echo "$FOUND"
87+
exit 1
88+
fi
89+
- name: Check for native_decide
90+
run: |
91+
FOUND=$(grep -rn 'native_decide' --include='*.lean' . \
92+
| grep -v '\.lake/packages/' \
93+
|| true)
94+
if [ -n "$FOUND" ]; then
95+
echo "::error::Found native_decide (bypasses kernel)"
96+
echo "$FOUND"
97+
exit 1
98+
fi
99+
100+
build:
101+
runs-on: ["self-hosted", "macos", "arm64", "VidiomTM"]
102+
name: Build & Typecheck
103+
timeout-minutes: 30
104+
steps:
105+
- uses: actions/checkout@v4
106+
- name: Install Elan
107+
run: |
108+
which elan 2>/dev/null || { curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none; }
109+
echo "$HOME/.elan/bin" >> $GITHUB_PATH
110+
- name: Symlink .lake cache
111+
run: |
112+
CACHE_DIR="$HOME/.cache/lean-runtime-analysis/lake"
113+
mkdir -p "$CACHE_DIR"
114+
if [ -d .lake ] && [ ! -L .lake ]; then
115+
rsync -a .lake/ "$CACHE_DIR/" 2>/dev/null || true
116+
rm -rf .lake
117+
fi
118+
ln -sfn "$CACHE_DIR" .lake
119+
- name: Build
120+
run: lake build
121+
122+
verification:
123+
runs-on: ["self-hosted", "macos", "arm64", "VidiomTM"]
124+
name: Mechanization Audit
125+
timeout-minutes: 15
126+
needs: [build]
127+
steps:
128+
- uses: actions/checkout@v4
129+
- name: Install Elan
130+
run: |
131+
which elan 2>/dev/null || { curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none; }
132+
echo "$HOME/.elan/bin" >> $GITHUB_PATH
133+
- name: Symlink .lake cache
134+
run: |
135+
CACHE_DIR="$HOME/.cache/lean-runtime-analysis/lake"
136+
mkdir -p "$CACHE_DIR"
137+
if [ -d .lake ] && [ ! -L .lake ]; then
138+
rsync -a .lake/ "$CACHE_DIR/" 2>/dev/null || true
139+
rm -rf .lake
140+
fi
141+
ln -sfn "$CACHE_DIR" .lake
142+
- name: Mechanization completeness audit
143+
run: |
144+
ERRORS=0
145+
check_theorem() {
146+
local file="$1" name="$2" label="$3"
147+
if grep -qE "^[[:space:]]*(private[[:space:]]+|protected[[:space:]]+|noncomputable[[:space:]]+)*theorem[[:space:]]+${name}\\b" "$file"; then
148+
echo " ✓ $label: $name"
149+
else
150+
echo "::error::$label missing: theorem $name not found in $file"
151+
ERRORS=$((ERRORS + 1))
152+
fi
153+
}
154+
check_no_stub() {
155+
local file="$1" pattern="$2" label="$3"
156+
if grep -qF "$pattern" "$file"; then
157+
echo "::error::$label still contains stub: $pattern"
158+
ERRORS=$((ERRORS + 1))
159+
else
160+
echo " ✓ $label: no stub markers"
161+
fi
162+
}
163+
164+
echo "=== Fully mechanized (verified present) ==="
165+
check_theorem LeCamLowerBound.lean tight_sample_lower_bound "Thm 4 (Le Cam)"
166+
check_theorem LeCamLowerBound.lean hellingerSq_uniform_shift "Thm 4 (H² shift)"
167+
check_theorem LeCamLowerBound.lean exists_grid_size "Thm 4 (grid size)"
168+
check_theorem WitnessGameDrift.lean C_k_nonneg "Lem 4 (Y-drift)"
169+
check_theorem WitnessGameDrift.lean batch_mean_formula "Lem 5 (batch-mean)"
170+
check_theorem WitnessGameDrift.lean progression_gap_sum "Lem 5 (progression)"
171+
check_theorem WitnessGameDrift.lean regression_gap_sum "Lem 5 (regression)"
172+
check_theorem WitnessGameDrift.lean batch_mean_misranking "Prop 3 (misranking)"
173+
check_theorem RLocalGames.lean r_local_offset_bound "Lem 3 (r-local offset)"
174+
check_theorem RLocalGames.lean r_local_alignment "Thm 7 (r-local alignment)"
175+
check_theorem DriftTheorems/NegativeDrift.lean negative_drift_theorem "NDT (abstract)"
176+
177+
echo "=== Required (must be fully mechanized) ==="
178+
check_theorem RLocalGames.lean r_local_tightness_all_pairs_misranked "Prop 1 (cyclic adversarial)"
179+
check_no_stub RLocalGames.lean "Uses a trivial zero-game" "Prop 1 (stub check)"
180+
181+
if [ $ERRORS -gt 0 ]; then
182+
echo "::error::$ERRORS mechanization target(s) missing or incomplete"
183+
exit 1
184+
fi
185+
echo "All required mechanization targets present."
186+
187+
codeql:
188+
runs-on: ubuntu-latest
189+
name: CodeQL Analysis
190+
permissions:
191+
security-events: write
192+
timeout-minutes: 30
193+
steps:
194+
- uses: actions/checkout@v4
195+
- uses: github/codeql-action/init@v3
196+
with:
197+
languages: cpp
198+
queries: security-extended
199+
- uses: github/codeql-action/analyze@v3

0 commit comments

Comments
 (0)