Skip to content

Commit 97617dd

Browse files
hyperpolymathhyperpolymath
committed
chore: resolve merge conflicts by favoring PR branch for data files (to be regenerated)
2 parents 16dec0c + 9c95bd0 commit 97617dd

301 files changed

Lines changed: 2509871 additions & 204759 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/hypatia-scan.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,7 @@ jobs:
7676
echo "- Medium: $MEDIUM" >> $GITHUB_STEP_SUMMARY
7777
7878
- name: Upload findings artifact
79-
uses: actions/upload-artifact@65c79d7f54e76e4e3c7a8f34db0f4ac8b515c478 # v4
79+
uses: actions/upload-artifact@b4b15b8c7c6ac21ea08fcf65892d2ee8f75cf882 # v4
8080
with:
8181
name: hypatia-findings
8282
path: hypatia-findings.json

‎.github/workflows/live-provers.yml‎

Lines changed: 260 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,260 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# ECHIDNA — Live-Prover CI
3+
#
4+
# Exercises real prover binaries against canonical micro-goals. Complements
5+
# rust-ci.yml (which runs mock tests on every PR) with live-subprocess coverage.
6+
#
7+
# Tiering (matches ~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md + manifests/live-provers.scm):
8+
# T1 — trivial — every PR + push to main
9+
# T2 — build — nightly
10+
# T3 — container — weekly
11+
# T4 — niche — quarterly, allow-fail
12+
#
13+
# Reproducibility paths (both tried; at least one must succeed):
14+
# 1. Guix manifest (PRIMARY, per project CLAUDE.md): manifests/live-provers.scm
15+
# 2. Nix flake (fallback): nix develop .#live-provers
16+
# 3. apt-get (expedient bootstrap for T1 only): jobs below
17+
18+
name: Live Provers
19+
20+
on:
21+
push:
22+
branches: [main]
23+
pull_request:
24+
branches: [main]
25+
schedule:
26+
- cron: '0 3 * * *' # Tier-2 nightly at 03:00 UTC
27+
- cron: '0 5 * * 0' # Tier-3 weekly Sunday 05:00 UTC
28+
- cron: '0 6 1 */3 *' # Tier-4 quarterly 1st of Jan/Apr/Jul/Oct 06:00 UTC
29+
workflow_dispatch:
30+
inputs:
31+
tier:
32+
description: 'Which tier to run (1|2|3|4|all)'
33+
required: false
34+
default: '1'
35+
36+
permissions:
37+
contents: read
38+
39+
env:
40+
CARGO_TERM_COLOR: always
41+
RUST_BACKTRACE: 1
42+
ECHIDNA_LIVE_PROVERS: '1'
43+
44+
jobs:
45+
46+
# ============================================================================
47+
# Tier 1 — every PR. Apt-installable provers. Must stay green.
48+
# ============================================================================
49+
tier1:
50+
name: T1 / ${{ matrix.backend }}
51+
if: github.event_name != 'schedule' || github.event.schedule == '0 3 * * *'
52+
runs-on: ubuntu-latest
53+
strategy:
54+
fail-fast: false
55+
matrix:
56+
backend:
57+
- z3
58+
- cvc5
59+
- vampire
60+
- eprover
61+
- spass
62+
- alt-ergo
63+
- glpk
64+
- minizinc
65+
- chuffed
66+
steps:
67+
- name: Checkout
68+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
69+
70+
- name: Install Rust
71+
uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
72+
73+
- name: Cache Cargo
74+
uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
75+
76+
- name: Provision prover (${{ matrix.backend }})
77+
run: |
78+
set -euo pipefail
79+
sudo apt-get update
80+
case "${{ matrix.backend }}" in
81+
z3) sudo apt-get install -y z3 ;;
82+
cvc5) curl -sSL -o /tmp/cvc5 https://github.com/cvc5/cvc5/releases/latest/download/cvc5-Linux-static
83+
chmod +x /tmp/cvc5
84+
sudo install -m 0755 /tmp/cvc5 /usr/local/bin/cvc5 ;;
85+
vampire) curl -sSL -o /tmp/vampire.zip https://github.com/vprover/vampire/releases/latest/download/vampire-Linux-x86_64.zip
86+
unzip -j -o /tmp/vampire.zip -d /tmp
87+
sudo install -m 0755 /tmp/vampire /usr/local/bin/vampire ;;
88+
eprover) sudo apt-get install -y eprover ;;
89+
spass) sudo apt-get install -y spass ;;
90+
alt-ergo) sudo apt-get install -y alt-ergo ;;
91+
glpk) sudo apt-get install -y glpk-utils ;;
92+
minizinc) sudo apt-get install -y minizinc ;;
93+
chuffed) sudo apt-get install -y minizinc # chuffed bundled with minizinc-ide on recent ubuntu
94+
;;
95+
esac
96+
"${{ matrix.backend }}" --version 2>/dev/null || "${{ matrix.backend }}" --help 2>/dev/null || true
97+
98+
- name: Run live test for ${{ matrix.backend }}
99+
run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}
100+
101+
# ============================================================================
102+
# Tier 1 reproducibility check — ensure Guix manifest actually resolves.
103+
# Allow-fail: this is additional proof, not a gate (Guix-on-Ubuntu is flaky
104+
# without dedicated setup).
105+
# ============================================================================
106+
tier1-guix-reproducibility:
107+
name: T1 Guix manifest check
108+
if: github.event_name != 'schedule'
109+
runs-on: ubuntu-latest
110+
continue-on-error: true
111+
steps:
112+
- name: Checkout
113+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
114+
- name: Install Guix
115+
run: |
116+
sudo apt-get update
117+
sudo apt-get install -y guix
118+
- name: Resolve manifest (doesn't run tests — just proves the .scm parses)
119+
run: |
120+
guix describe || true
121+
guix package -m manifests/live-provers.scm --dry-run || \
122+
echo "NOTE: Guix manifest resolution failed — non-blocking reproducibility signal."
123+
124+
# ============================================================================
125+
# Tier 2 — nightly. Larger build-from-source provers.
126+
# ============================================================================
127+
tier2:
128+
name: T2 / ${{ matrix.backend }}
129+
if: github.event_name == 'schedule' && github.event.schedule == '0 3 * * *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '2' || inputs.tier == 'all'))
130+
runs-on: ubuntu-latest
131+
strategy:
132+
fail-fast: false
133+
matrix:
134+
backend:
135+
- coq
136+
- agda
137+
- idris2
138+
- lean4
139+
- isabelle
140+
- why3
141+
- dafny
142+
- fstar
143+
- hol-light
144+
- tlaps
145+
steps:
146+
- name: Checkout
147+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
148+
- name: Install Rust
149+
uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
150+
- name: Cache Cargo
151+
uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
152+
- name: Provision ${{ matrix.backend }} (best-effort via apt / upstream release)
153+
continue-on-error: true
154+
run: |
155+
set -euo pipefail
156+
sudo apt-get update
157+
case "${{ matrix.backend }}" in
158+
coq)
159+
sudo apt-get install -y coq
160+
;;
161+
agda)
162+
sudo apt-get install -y agda
163+
;;
164+
idris2)
165+
# Idris2 has no apt package; build from the self-hosting tarball.
166+
# Chez Scheme is the recommended backend.
167+
sudo apt-get install -y chezscheme make
168+
curl -fsSL -o /tmp/idris2.tar.gz https://github.com/idris-lang/Idris2/releases/latest/download/idris2-src-latest.tgz || \
169+
curl -fsSL -o /tmp/idris2.tar.gz https://www.idris-lang.org/download/idris2-0.7.0.tgz
170+
mkdir -p /tmp/idris2-src
171+
tar xzf /tmp/idris2.tar.gz -C /tmp/idris2-src --strip-components=1
172+
(cd /tmp/idris2-src && make bootstrap SCHEME=scheme && sudo make install PREFIX=/usr/local)
173+
;;
174+
lean4)
175+
curl -sSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain leanprover/lean4:stable
176+
echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
177+
;;
178+
isabelle)
179+
# Isabelle2024 tarball (~500MB); keep on nightly only.
180+
curl -fsSL -o /tmp/isabelle.tar.gz https://isabelle.in.tum.de/dist/Isabelle2024_linux.tar.gz
181+
sudo mkdir -p /opt
182+
sudo tar xzf /tmp/isabelle.tar.gz -C /opt
183+
sudo ln -sf /opt/Isabelle2024/bin/isabelle /usr/local/bin/isabelle
184+
;;
185+
why3)
186+
sudo apt-get install -y why3
187+
;;
188+
dafny)
189+
# Dafny 4.x is distributed as a standalone .NET global tool.
190+
# ubuntu-latest ships dotnet-sdk 8 in setup images; install via apt if absent.
191+
command -v dotnet >/dev/null 2>&1 || sudo apt-get install -y dotnet-sdk-8.0
192+
dotnet tool install --global Dafny
193+
echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
194+
;;
195+
fstar)
196+
# F* ships prebuilt Linux binaries; binary is `fstar.exe` even on Linux.
197+
curl -fsSL -o /tmp/fstar.tar.gz https://github.com/FStarLang/FStar/releases/latest/download/fstar-linux_x86_64.tar.gz
198+
sudo mkdir -p /opt/fstar
199+
sudo tar xzf /tmp/fstar.tar.gz -C /opt/fstar --strip-components=1
200+
sudo ln -sf /opt/fstar/bin/fstar.exe /usr/local/bin/fstar.exe
201+
;;
202+
hol-light)
203+
# No prebuilt binary; opam build is ~20min and pulls camlp5.
204+
# Deferred to Wave-3 (container-based provisioning) per the
205+
# production-wiring plan.
206+
echo "hol-light deferred to Wave-3 container provisioning"
207+
exit 0
208+
;;
209+
tlaps)
210+
# TLA+ Proof System ships a self-extracting installer; provides tlapm.
211+
curl -fsSL -o /tmp/tlaps.sh https://github.com/tlaplus/tlapm/releases/latest/download/tlaps-installer-linux-x86_64.sh
212+
chmod +x /tmp/tlaps.sh
213+
sudo /tmp/tlaps.sh --prefix=/opt/tlaps
214+
sudo ln -sf /opt/tlaps/bin/tlapm /usr/local/bin/tlapm
215+
;;
216+
esac
217+
# Best-effort version probe for the matrix log.
218+
case "${{ matrix.backend }}" in
219+
fstar) fstar.exe --version || true ;;
220+
tlaps) tlapm --version || true ;;
221+
hol-light) true ;;
222+
*) "${{ matrix.backend }}" --version 2>/dev/null || true ;;
223+
esac
224+
- name: Run live test for ${{ matrix.backend }} (allow-fail while Wave-2 wires up)
225+
continue-on-error: true
226+
run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}
227+
228+
# ============================================================================
229+
# Tier 3 — weekly. Container-provisioned provers. Wave-3 placeholder.
230+
# ============================================================================
231+
tier3:
232+
name: T3 container provers
233+
if: github.event_name == 'schedule' && github.event.schedule == '0 5 * * 0' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '3' || inputs.tier == 'all'))
234+
runs-on: ubuntu-latest
235+
continue-on-error: true
236+
steps:
237+
- name: Checkout
238+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
239+
- name: Announce Wave-3 TODO
240+
run: |
241+
echo "Tier-3 backends (Tamarin, ProVerif, Imandra, SCIP, OR-Tools, HOL4, ACL2, Twelf, Metamath)"
242+
echo "are provisioned via per-backend Containerfiles in Wave-3 of L3."
243+
echo "See ~/Desktop/ECHIDNA-L3-LIVE-PROVER-CI-PROMPT.md for scope."
244+
245+
# ============================================================================
246+
# Tier 4 — quarterly, best-effort / allow-fail.
247+
# ============================================================================
248+
tier4:
249+
name: T4 niche provers
250+
if: github.event_name == 'schedule' && github.event.schedule == '0 6 1 */3 *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '4' || inputs.tier == 'all'))
251+
runs-on: ubuntu-latest
252+
continue-on-error: true
253+
steps:
254+
- name: Checkout
255+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
256+
- name: Announce Wave-4 TODO
257+
run: |
258+
echo "Tier-4 backends (Mizar, Nuprl, PVS, Minlog, Dedukti, Arend, KeY, Prism, UPPAAL,"
259+
echo "ViPER, NuSMV, Spin, TLC, CBMC, Seahorn, dReal, Boogie, Kissat, Alloy) are"
260+
echo "retained as mock-only unless a maintainer volunteers a Containerfile."

‎.github/workflows/scorecard.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,6 @@ jobs:
2727
results_format: sarif
2828

2929
- name: Upload results
30-
uses: github/codeql-action/upload-sarif@6624720a57d4c312633c7b953db2f2da5bcb4c3a # v3
30+
uses: github/codeql-action/upload-sarif@662472033e021d55d94146f66f6058822b0b39fd # v3.28.1
3131
with:
3232
sarif_file: results.sarif

‎.github/workflows/security-scan.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,6 @@ permissions:
1414

1515
jobs:
1616
scan:
17-
uses: hyperpolymath/panic-attacker/.github/workflows/scan-and-report.yml@main
17+
uses: hyperpolymath/panic-attack/.github/workflows/scan-and-report.yml@main
1818
secrets:
1919
VERISIMDB_PAT: ${{ secrets.VERISIMDB_PAT }}

‎.gitignore‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -147,6 +147,10 @@ training_data/vocabulary_*.txt
147147
training_data/proof_states_UNIFIED.jsonl
148148
training_data/proof_states_smtlib.jsonl
149149
training_data/tactics_smtlib.jsonl
150+
# TPTP full-share output exceeds 100MB (reproducible via scripts/extract_tptp.jl)
151+
training_data/proof_states_tptp.a2ml
152+
# KeY output exceeds 100MB (reproducible via scripts/extract_key.jl)
153+
training_data/proof_states_key.jsonl
150154

151155
# Root-level merged artifacts
152156
premises_merged.jsonl
@@ -162,6 +166,14 @@ FINAL_CORPUS_COMPLETENESS_REPORT.md
162166
PROVER_EXPANSION_ROADMAP.md
163167
models/neural/
164168

169+
# Per-epoch training checkpoints (regenerated; only models/ root kept)
170+
models/e*/
171+
/models_e*/
172+
173+
# Zig FFI build output (regenerated by `zig build`)
174+
src/zig_ffi/zig-out/
175+
src/zig_ffi/.zig-cache/
176+
165177
# asdf version manager
166178
.tool-versions
167179

@@ -173,3 +185,11 @@ proofs/coq/**/*.glob
173185
proofs/coq/**/.*.aux
174186
proofs/agda/**/*.agdai
175187
proofs/metamath/.metamath*
188+
target/
189+
node_modules/
190+
_build/
191+
deps/
192+
.elixir_ls/
193+
.cache/
194+
build/
195+
dist/

0 commit comments

Comments
 (0)