From 3b45554f7315811b24fae924b4b5b5e70a1eeb10 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 2 Sep 2026 10:05:33 -0400 Subject: [PATCH] bench: Drop the formal-conjectures compile benchmark formal-conjectures is a corpus of conjectures, not of proofs, so compiling it measures the compiler against statements nobody has proved. That is not what the compile benchmarks are for. CompileFC existed only to build it: a package whose sole dependency was formal-conjectures, held at Lean v4.27.0 because the upstream corpus targets that release. That stale pin was the one thing the nightly lean-update sweep kept finding to move (#608). Its FC matrix entry in the benchmark workflow has been commented out since it fell behind, so nothing in CI loses a job here. With the pin gone, `. Benchmarks/**` sweeps a tree whose packages all track the current toolchain, so lean-update needs no steering around it. --- .github/workflows/bench-main.yml | 12 +- .github/workflows/update.yml | 3 +- Benchmarks/CompileFC/.envrc | 1 - Benchmarks/CompileFC/CompileFC.lean | 585 ------------------------ Benchmarks/CompileFC/README.md | 19 - Benchmarks/CompileFC/flake.lock | 117 ----- Benchmarks/CompileFC/flake.nix | 53 --- Benchmarks/CompileFC/lake-manifest.json | 105 ----- Benchmarks/CompileFC/lakefile.toml | 11 - Benchmarks/CompileFC/lean-toolchain | 1 - 10 files changed, 3 insertions(+), 904 deletions(-) delete mode 100644 Benchmarks/CompileFC/.envrc delete mode 100644 Benchmarks/CompileFC/CompileFC.lean delete mode 100644 Benchmarks/CompileFC/README.md delete mode 100644 Benchmarks/CompileFC/flake.lock delete mode 100644 Benchmarks/CompileFC/flake.nix delete mode 100644 Benchmarks/CompileFC/lake-manifest.json delete mode 100644 Benchmarks/CompileFC/lakefile.toml delete mode 100644 Benchmarks/CompileFC/lean-toolchain diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml index 4312e8ec4..d97e9a2e6 100644 --- a/.github/workflows/bench-main.yml +++ b/.github/workflows/bench-main.yml @@ -128,8 +128,7 @@ jobs: # lake target (Compile), the cache-key suffix, and the # bencher row name. Every registry env compiles here; which envs # the benchmark job then proves/checks depends on which envs have - # constants in Ix/BenchConstants.lean. Add FC once it's on - # current Lean. + # constants in Ix/BenchConstants.lean. include: - { env: InitStd } - { env: Lean } @@ -139,7 +138,6 @@ jobs: - { env: ISLB } - { env: Mathlib, mathlib: true } - { env: FLT, cache_pkg: flt, mathlib: true } - # - { env: FC, cache_pkg: formal_conjectures, mathlib: true } steps: - uses: actions/checkout@v7 # `lake build` below clones this package's Lake dependencies. @@ -154,10 +152,6 @@ jobs: label: Compile measurement CPU provenance-file: ~/.local/bin/benchmark-build-cpu.txt - run: echo "$HOME/.local/bin" >> $GITHUB_PATH - # FC's library env lives in a sibling `${COMPILE_DIR}FC` package dir, so - # point COMPILE_DIR there for the FC matrix job. - # - if: matrix.env == 'FC' - # run: echo "COMPILE_DIR=${{ env.COMPILE_DIR }}FC" | tee -a $GITHUB_ENV # Install the Lean toolchain. The mathlib olean cache is fetched only # for envs that import Mathlib (Mathlib, FLT) — the shared # Benchmarks/Compile package depends on mathlib, so without this @@ -168,14 +162,12 @@ jobs: auto-config: false use-github-cache: false use-mathlib-cache: ${{ matrix.mathlib && 'true' || 'false' }} - # FLT and FC take a few minutes to rebuild, so cache their build artifacts. + # FLT takes a few minutes to rebuild, so cache its build artifacts. - if: matrix.cache_pkg uses: actions/cache@v6 with: path: ${{ env.COMPILE_DIR }}/.lake/packages/${{ matrix.cache_pkg }}/.lake/build key: ${{ matrix.cache_pkg }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }} - # No `--wfail` here: formal-conjectures (FC) emits a copyright-notice - # warning that must not fail the build. - run: lake build Compile${{ matrix.env }} working-directory: ${{ env.COMPILE_DIR }} # The measured compile: serializes the env to `.ixe` at the diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml index a5089f05f..f2d50dc64 100644 --- a/.github/workflows/update.yml +++ b/.github/workflows/update.yml @@ -35,8 +35,7 @@ jobs: # The root package plus every package under Benchmarks/ — `/**` # walks the whole tree (catching Catalog's nested fixture # workspaces) and skips dotted directories, so `.lake` - # dependency checkouts are never swept up. This includes - # Benchmarks/CompileFC, previously pinned to an old toolchain. + # dependency checkouts are never swept up. lake_package_directory: ". Benchmarks/**" bump_mode: pinned-tags pr: true diff --git a/Benchmarks/CompileFC/.envrc b/Benchmarks/CompileFC/.envrc deleted file mode 100644 index 3550a30f2..000000000 --- a/Benchmarks/CompileFC/.envrc +++ /dev/null @@ -1 +0,0 @@ -use flake diff --git a/Benchmarks/CompileFC/CompileFC.lean b/Benchmarks/CompileFC/CompileFC.lean deleted file mode 100644 index bf053aea1..000000000 --- a/Benchmarks/CompileFC/CompileFC.lean +++ /dev/null @@ -1,585 +0,0 @@ -import FormalConjectures.Arxiv.«0911.2077».Conjecture6_3 -import FormalConjectures.Arxiv.«0912.2382».CurlingNumberConjecture -import FormalConjectures.Arxiv.«1308.0994».BoxdotConjecture -import FormalConjectures.Arxiv.«1506.05785».MaximumAngle -import FormalConjectures.Arxiv.«1601.03081».UniqueCrystalComponents -import FormalConjectures.Arxiv.«1609.08688».sIncreasingrTuples -import FormalConjectures.Arxiv.«2107.00295».IndependentDomination -import FormalConjectures.Arxiv.«2107.12475».CollatzLike -import FormalConjectures.Arxiv.«2208.14736».ZariskiCancellation -import FormalConjectures.Arxiv.«2501.03234».ArithmeticSumS -import FormalConjectures.Arxiv.«2504.17644».Margulis -import FormalConjectures.Arxiv.«2602.05192».FirstProof4 -import FormalConjectures.Arxiv.«2602.05192».FirstProof6 -import FormalConjectures.Books.UniformDistributionOfSequences.Equidistribution -import FormalConjectures.ErdosProblems.«1003» -import FormalConjectures.ErdosProblems.«1004» -import FormalConjectures.ErdosProblems.«100» -import FormalConjectures.ErdosProblems.«1038» -import FormalConjectures.ErdosProblems.«1041» -import FormalConjectures.ErdosProblems.«1043» -import FormalConjectures.ErdosProblems.«1049» -import FormalConjectures.ErdosProblems.«1051» -import FormalConjectures.ErdosProblems.«1052» -import FormalConjectures.ErdosProblems.«1054» -import FormalConjectures.ErdosProblems.«1055» -import FormalConjectures.ErdosProblems.«1056» -import FormalConjectures.ErdosProblems.«1059» -import FormalConjectures.ErdosProblems.«1060» -import FormalConjectures.ErdosProblems.«1061» -import FormalConjectures.ErdosProblems.«1062» -import FormalConjectures.ErdosProblems.«1063» -import FormalConjectures.ErdosProblems.«1064» -import FormalConjectures.ErdosProblems.«1065» -import FormalConjectures.ErdosProblems.«1067» -import FormalConjectures.ErdosProblems.«1068» -import FormalConjectures.ErdosProblems.«1071» -import FormalConjectures.ErdosProblems.«1072» -import FormalConjectures.ErdosProblems.«1073» -import FormalConjectures.ErdosProblems.«1074» -import FormalConjectures.ErdosProblems.«1077» -import FormalConjectures.ErdosProblems.«107» -import FormalConjectures.ErdosProblems.«1080» -import FormalConjectures.ErdosProblems.«1084» -import FormalConjectures.ErdosProblems.«1085» -import FormalConjectures.ErdosProblems.«108» -import FormalConjectures.ErdosProblems.«1092» -import FormalConjectures.ErdosProblems.«1093» -import FormalConjectures.ErdosProblems.«1094» -import FormalConjectures.ErdosProblems.«1095» -import FormalConjectures.ErdosProblems.«1097» -import FormalConjectures.ErdosProblems.«109» -import FormalConjectures.ErdosProblems.«10» -import FormalConjectures.ErdosProblems.«1101» -import FormalConjectures.ErdosProblems.«1102» -import FormalConjectures.ErdosProblems.«1104» -import FormalConjectures.ErdosProblems.«1105» -import FormalConjectures.ErdosProblems.«1106» -import FormalConjectures.ErdosProblems.«1107» -import FormalConjectures.ErdosProblems.«1108» -import FormalConjectures.ErdosProblems.«1135» -import FormalConjectures.ErdosProblems.«1137» -import FormalConjectures.ErdosProblems.«1139» -import FormalConjectures.ErdosProblems.«1141» -import FormalConjectures.ErdosProblems.«1145» -import FormalConjectures.ErdosProblems.«1148» -import FormalConjectures.ErdosProblems.«1150» -import FormalConjectures.ErdosProblems.«1176» -import FormalConjectures.ErdosProblems.«119» -import FormalConjectures.ErdosProblems.«11» -import FormalConjectures.ErdosProblems.«120» -import FormalConjectures.ErdosProblems.«123» -import FormalConjectures.ErdosProblems.«124» -import FormalConjectures.ErdosProblems.«125» -import FormalConjectures.ErdosProblems.«126» -import FormalConjectures.ErdosProblems.«128» -import FormalConjectures.ErdosProblems.«12» -import FormalConjectures.ErdosProblems.«137» -import FormalConjectures.ErdosProblems.«138» -import FormalConjectures.ErdosProblems.«139» -import FormalConjectures.ErdosProblems.«13» -import FormalConjectures.ErdosProblems.«141» -import FormalConjectures.ErdosProblems.«142» -import FormalConjectures.ErdosProblems.«143» -import FormalConjectures.ErdosProblems.«145» -import FormalConjectures.ErdosProblems.«14» -import FormalConjectures.ErdosProblems.«152» -import FormalConjectures.ErdosProblems.«153» -import FormalConjectures.ErdosProblems.«155» -import FormalConjectures.ErdosProblems.«158» -import FormalConjectures.ErdosProblems.«160» -import FormalConjectures.ErdosProblems.«168» -import FormalConjectures.ErdosProblems.«170» -import FormalConjectures.ErdosProblems.«172» -import FormalConjectures.ErdosProblems.«17» -import FormalConjectures.ErdosProblems.«188» -import FormalConjectures.ErdosProblems.«189» -import FormalConjectures.ErdosProblems.«194» -import FormalConjectures.ErdosProblems.«195» -import FormalConjectures.ErdosProblems.«196» -import FormalConjectures.ErdosProblems.«197» -import FormalConjectures.ErdosProblems.«198» -import FormalConjectures.ErdosProblems.«1» -import FormalConjectures.ErdosProblems.«200» -import FormalConjectures.ErdosProblems.«203» -import FormalConjectures.ErdosProblems.«204» -import FormalConjectures.ErdosProblems.«208» -import FormalConjectures.ErdosProblems.«20» -import FormalConjectures.ErdosProblems.«212» -import FormalConjectures.ErdosProblems.«213» -import FormalConjectures.ErdosProblems.«218» -import FormalConjectures.ErdosProblems.«219» -import FormalConjectures.ErdosProblems.«228» -import FormalConjectures.ErdosProblems.«229» -import FormalConjectures.ErdosProblems.«233» -import FormalConjectures.ErdosProblems.«234» -import FormalConjectures.ErdosProblems.«236» -import FormalConjectures.ErdosProblems.«238» -import FormalConjectures.ErdosProblems.«239» -import FormalConjectures.ErdosProblems.«23» -import FormalConjectures.ErdosProblems.«242» -import FormalConjectures.ErdosProblems.«243» -import FormalConjectures.ErdosProblems.«244» -import FormalConjectures.ErdosProblems.«245» -import FormalConjectures.ErdosProblems.«247» -import FormalConjectures.ErdosProblems.«248» -import FormalConjectures.ErdosProblems.«249» -import FormalConjectures.ErdosProblems.«250» -import FormalConjectures.ErdosProblems.«251» -import FormalConjectures.ErdosProblems.«252» -import FormalConjectures.ErdosProblems.«253» -import FormalConjectures.ErdosProblems.«257» -import FormalConjectures.ErdosProblems.«258» -import FormalConjectures.ErdosProblems.«259» -import FormalConjectures.ErdosProblems.«25» -import FormalConjectures.ErdosProblems.«263» -import FormalConjectures.ErdosProblems.«264» -import FormalConjectures.ErdosProblems.«266» -import FormalConjectures.ErdosProblems.«267» -import FormalConjectures.ErdosProblems.«268» -import FormalConjectures.ErdosProblems.«269» -import FormalConjectures.ErdosProblems.«26» -import FormalConjectures.ErdosProblems.«273» -import FormalConjectures.ErdosProblems.«274» -import FormalConjectures.ErdosProblems.«275» -import FormalConjectures.ErdosProblems.«276» -import FormalConjectures.ErdosProblems.«277» -import FormalConjectures.ErdosProblems.«283» -import FormalConjectures.ErdosProblems.«285» -import FormalConjectures.ErdosProblems.«288» -import FormalConjectures.ErdosProblems.«289» -import FormalConjectures.ErdosProblems.«28» -import FormalConjectures.ErdosProblems.«295» -import FormalConjectures.ErdosProblems.«298» -import FormalConjectures.ErdosProblems.«299» -import FormalConjectures.ErdosProblems.«303» -import FormalConjectures.ErdosProblems.«304» -import FormalConjectures.ErdosProblems.«306» -import FormalConjectures.ErdosProblems.«307» -import FormalConjectures.ErdosProblems.«30» -import FormalConjectures.ErdosProblems.«312» -import FormalConjectures.ErdosProblems.«313» -import FormalConjectures.ErdosProblems.«316» -import FormalConjectures.ErdosProblems.«317» -import FormalConjectures.ErdosProblems.«318» -import FormalConjectures.ErdosProblems.«319» -import FormalConjectures.ErdosProblems.«321» -import FormalConjectures.ErdosProblems.«324» -import FormalConjectures.ErdosProblems.«325» -import FormalConjectures.ErdosProblems.«326» -import FormalConjectures.ErdosProblems.«329» -import FormalConjectures.ErdosProblems.«32» -import FormalConjectures.ErdosProblems.«330» -import FormalConjectures.ErdosProblems.«331» -import FormalConjectures.ErdosProblems.«332» -import FormalConjectures.ErdosProblems.«33» -import FormalConjectures.ErdosProblems.«340» -import FormalConjectures.ErdosProblems.«341» -import FormalConjectures.ErdosProblems.«346» -import FormalConjectures.ErdosProblems.«347» -import FormalConjectures.ErdosProblems.«348» -import FormalConjectures.ErdosProblems.«349» -import FormalConjectures.ErdosProblems.«350» -import FormalConjectures.ErdosProblems.«351» -import FormalConjectures.ErdosProblems.«352» -import FormalConjectures.ErdosProblems.«354» -import FormalConjectures.ErdosProblems.«355» -import FormalConjectures.ErdosProblems.«357» -import FormalConjectures.ErdosProblems.«358» -import FormalConjectures.ErdosProblems.«359» -import FormalConjectures.ErdosProblems.«361» -import FormalConjectures.ErdosProblems.«364» -import FormalConjectures.ErdosProblems.«366» -import FormalConjectures.ErdosProblems.«36» -import FormalConjectures.ErdosProblems.«370» -import FormalConjectures.ErdosProblems.«371» -import FormalConjectures.ErdosProblems.«373» -import FormalConjectures.ErdosProblems.«375» -import FormalConjectures.ErdosProblems.«376» -import FormalConjectures.ErdosProblems.«377» -import FormalConjectures.ErdosProblems.«379» -import FormalConjectures.ErdosProblems.«383» -import FormalConjectures.ErdosProblems.«385» -import FormalConjectures.ErdosProblems.«386» -import FormalConjectures.ErdosProblems.«387» -import FormalConjectures.ErdosProblems.«389» -import FormalConjectures.ErdosProblems.«38» -import FormalConjectures.ErdosProblems.«390» -import FormalConjectures.ErdosProblems.«392» -import FormalConjectures.ErdosProblems.«394» -import FormalConjectures.ErdosProblems.«396» -import FormalConjectures.ErdosProblems.«397» -import FormalConjectures.ErdosProblems.«398» -import FormalConjectures.ErdosProblems.«399» -import FormalConjectures.ErdosProblems.«39» -import FormalConjectures.ErdosProblems.«3» -import FormalConjectures.ErdosProblems.«402» -import FormalConjectures.ErdosProblems.«406» -import FormalConjectures.ErdosProblems.«409» -import FormalConjectures.ErdosProblems.«40» -import FormalConjectures.ErdosProblems.«410» -import FormalConjectures.ErdosProblems.«412» -import FormalConjectures.ErdosProblems.«413» -import FormalConjectures.ErdosProblems.«414» -import FormalConjectures.ErdosProblems.«416» -import FormalConjectures.ErdosProblems.«417» -import FormalConjectures.ErdosProblems.«418» -import FormalConjectures.ErdosProblems.«41» -import FormalConjectures.ErdosProblems.«421» -import FormalConjectures.ErdosProblems.«422» -import FormalConjectures.ErdosProblems.«424» -import FormalConjectures.ErdosProblems.«427» -import FormalConjectures.ErdosProblems.«428» -import FormalConjectures.ErdosProblems.«42» -import FormalConjectures.ErdosProblems.«434» -import FormalConjectures.ErdosProblems.«442» -import FormalConjectures.ErdosProblems.«44» -import FormalConjectures.ErdosProblems.«454» -import FormalConjectures.ErdosProblems.«455» -import FormalConjectures.ErdosProblems.«457» -import FormalConjectures.ErdosProblems.«458» -import FormalConjectures.ErdosProblems.«463» -import FormalConjectures.ErdosProblems.«469» -import FormalConjectures.ErdosProblems.«470» -import FormalConjectures.ErdosProblems.«477» -import FormalConjectures.ErdosProblems.«479» -import FormalConjectures.ErdosProblems.«480» -import FormalConjectures.ErdosProblems.«486» -import FormalConjectures.ErdosProblems.«488» -import FormalConjectures.ErdosProblems.«489» -import FormalConjectures.ErdosProblems.«48» -import FormalConjectures.ErdosProblems.«494» -import FormalConjectures.ErdosProblems.«495» -import FormalConjectures.ErdosProblems.«499» -import FormalConjectures.ErdosProblems.«4» -import FormalConjectures.ErdosProblems.«503» -import FormalConjectures.ErdosProblems.«507» -import FormalConjectures.ErdosProblems.«508» -import FormalConjectures.ErdosProblems.«509» -import FormalConjectures.ErdosProblems.«510» -import FormalConjectures.ErdosProblems.«513» -import FormalConjectures.ErdosProblems.«516» -import FormalConjectures.ErdosProblems.«517» -import FormalConjectures.ErdosProblems.«51» -import FormalConjectures.ErdosProblems.«520» -import FormalConjectures.ErdosProblems.«522» -import FormalConjectures.ErdosProblems.«536» -import FormalConjectures.ErdosProblems.«541» -import FormalConjectures.ErdosProblems.«562» -import FormalConjectures.ErdosProblems.«564» -import FormalConjectures.ErdosProblems.«566» -import FormalConjectures.ErdosProblems.«567» -import FormalConjectures.ErdosProblems.«56» -import FormalConjectures.ErdosProblems.«587» -import FormalConjectures.ErdosProblems.«590» -import FormalConjectures.ErdosProblems.«591» -import FormalConjectures.ErdosProblems.«592» -import FormalConjectures.ErdosProblems.«598» -import FormalConjectures.ErdosProblems.«617» -import FormalConjectures.ErdosProblems.«61» -import FormalConjectures.ErdosProblems.«623» -import FormalConjectures.ErdosProblems.«624» -import FormalConjectures.ErdosProblems.«645» -import FormalConjectures.ErdosProblems.«647» -import FormalConjectures.ErdosProblems.«64» -import FormalConjectures.ErdosProblems.«659» -import FormalConjectures.ErdosProblems.«66» -import FormalConjectures.ErdosProblems.«672» -import FormalConjectures.ErdosProblems.«677» -import FormalConjectures.ErdosProblems.«678» -import FormalConjectures.ErdosProblems.«67» -import FormalConjectures.ErdosProblems.«680» -import FormalConjectures.ErdosProblems.«681» -import FormalConjectures.ErdosProblems.«686» -import FormalConjectures.ErdosProblems.«689» -import FormalConjectures.ErdosProblems.«68» -import FormalConjectures.ErdosProblems.«694» -import FormalConjectures.ErdosProblems.«695» -import FormalConjectures.ErdosProblems.«697» -import FormalConjectures.ErdosProblems.«699» -import FormalConjectures.ErdosProblems.«69» -import FormalConjectures.ErdosProblems.«6» -import FormalConjectures.ErdosProblems.«705» -import FormalConjectures.ErdosProblems.«707» -import FormalConjectures.ErdosProblems.«723» -import FormalConjectures.ErdosProblems.«727» -import FormalConjectures.ErdosProblems.«728» -import FormalConjectures.ErdosProblems.«730» -import FormalConjectures.ErdosProblems.«741» -import FormalConjectures.ErdosProblems.«749» -import FormalConjectures.ErdosProblems.«74» -import FormalConjectures.ErdosProblems.«757» -import FormalConjectures.ErdosProblems.«770» -import FormalConjectures.ErdosProblems.«779» -import FormalConjectures.ErdosProblems.«786» -import FormalConjectures.ErdosProblems.«817» -import FormalConjectures.ErdosProblems.«822» -import FormalConjectures.ErdosProblems.«825» -import FormalConjectures.ErdosProblems.«826» -import FormalConjectures.ErdosProblems.«828» -import FormalConjectures.ErdosProblems.«82» -import FormalConjectures.ErdosProblems.«830» -import FormalConjectures.ErdosProblems.«835» -import FormalConjectures.ErdosProblems.«845» -import FormalConjectures.ErdosProblems.«846» -import FormalConjectures.ErdosProblems.«847» -import FormalConjectures.ErdosProblems.«848» -import FormalConjectures.ErdosProblems.«849» -import FormalConjectures.ErdosProblems.«850» -import FormalConjectures.ErdosProblems.«851» -import FormalConjectures.ErdosProblems.«853» -import FormalConjectures.ErdosProblems.«855» -import FormalConjectures.ErdosProblems.«859» -import FormalConjectures.ErdosProblems.«85» -import FormalConjectures.ErdosProblems.«865» -import FormalConjectures.ErdosProblems.«868» -import FormalConjectures.ErdosProblems.«873» -import FormalConjectures.ErdosProblems.«881» -import FormalConjectures.ErdosProblems.«885» -import FormalConjectures.ErdosProblems.«886» -import FormalConjectures.ErdosProblems.«887» -import FormalConjectures.ErdosProblems.«888» -import FormalConjectures.ErdosProblems.«889» -import FormalConjectures.ErdosProblems.«890» -import FormalConjectures.ErdosProblems.«891» -import FormalConjectures.ErdosProblems.«893» -import FormalConjectures.ErdosProblems.«897» -import FormalConjectures.ErdosProblems.«899» -import FormalConjectures.ErdosProblems.«89» -import FormalConjectures.ErdosProblems.«906» -import FormalConjectures.ErdosProblems.«90» -import FormalConjectures.ErdosProblems.«912» -import FormalConjectures.ErdosProblems.«913» -import FormalConjectures.ErdosProblems.«918» -import FormalConjectures.ErdosProblems.«920» -import FormalConjectures.ErdosProblems.«92» -import FormalConjectures.ErdosProblems.«930» -import FormalConjectures.ErdosProblems.«931» -import FormalConjectures.ErdosProblems.«932» -import FormalConjectures.ErdosProblems.«936» -import FormalConjectures.ErdosProblems.«938» -import FormalConjectures.ErdosProblems.«939» -import FormalConjectures.ErdosProblems.«940» -import FormalConjectures.ErdosProblems.«942» -import FormalConjectures.ErdosProblems.«943» -import FormalConjectures.ErdosProblems.«944» -import FormalConjectures.ErdosProblems.«945» -import FormalConjectures.ErdosProblems.«946» -import FormalConjectures.ErdosProblems.«949» -import FormalConjectures.ErdosProblems.«951» -import FormalConjectures.ErdosProblems.«952» -import FormalConjectures.ErdosProblems.«961» -import FormalConjectures.ErdosProblems.«965» -import FormalConjectures.ErdosProblems.«968» -import FormalConjectures.ErdosProblems.«971» -import FormalConjectures.ErdosProblems.«972» -import FormalConjectures.ErdosProblems.«975» -import FormalConjectures.ErdosProblems.«978» -import FormalConjectures.ErdosProblems.«979» -import FormalConjectures.ErdosProblems.«97» -import FormalConjectures.ErdosProblems.«982» -import FormalConjectures.ErdosProblems.«985» -import FormalConjectures.ErdosProblems.«996» -import FormalConjectures.ErdosProblems.«997» -import FormalConjectures.ErdosProblems.«99» -import FormalConjectures.ErdosProblems.«9» -import FormalConjectures.GreensOpenProblems.«12» -import FormalConjectures.GreensOpenProblems.«15» -import FormalConjectures.GreensOpenProblems.«16» -import FormalConjectures.GreensOpenProblems.«18» -import FormalConjectures.GreensOpenProblems.«19» -import FormalConjectures.GreensOpenProblems.«1» -import FormalConjectures.GreensOpenProblems.«23» -import FormalConjectures.GreensOpenProblems.«24» -import FormalConjectures.GreensOpenProblems.«26» -import FormalConjectures.GreensOpenProblems.«2» -import FormalConjectures.GreensOpenProblems.«35» -import FormalConjectures.GreensOpenProblems.«37» -import FormalConjectures.GreensOpenProblems.«3» -import FormalConjectures.GreensOpenProblems.«45» -import FormalConjectures.GreensOpenProblems.«4» -import FormalConjectures.GreensOpenProblems.«57» -import FormalConjectures.GreensOpenProblems.«58» -import FormalConjectures.GreensOpenProblems.«60» -import FormalConjectures.GreensOpenProblems.«61» -import FormalConjectures.GreensOpenProblems.«62» -import FormalConjectures.GreensOpenProblems.«63» -import FormalConjectures.GreensOpenProblems.«72» -import FormalConjectures.GreensOpenProblems.«77» -import FormalConjectures.GreensOpenProblems.«7» -import FormalConjectures.GreensOpenProblems.«81» -import FormalConjectures.GreensOpenProblems.«85» -import FormalConjectures.GreensOpenProblems.«94» -import FormalConjectures.GreensOpenProblems.«9» -import FormalConjectures.HilbertProblems.«17» -import FormalConjectures.Kourovka.«19_25» -import FormalConjectures.Kourovka.«20_76» -import FormalConjectures.Mathoverflow.«1973» -import FormalConjectures.Mathoverflow.«21003» -import FormalConjectures.Mathoverflow.«235893» -import FormalConjectures.Mathoverflow.«31809» -import FormalConjectures.Mathoverflow.«339137» -import FormalConjectures.Mathoverflow.«34145» -import FormalConjectures.Mathoverflow.«347178» -import FormalConjectures.Mathoverflow.«486451» -import FormalConjectures.Mathoverflow.«75792» -import FormalConjectures.Millenium.GeneralizedRiemannHypothesis -import FormalConjectures.Millenium.PvsNP -import FormalConjectures.OEIS.«228828» -import FormalConjectures.OEIS.«231201» -import FormalConjectures.OEIS.«232174» -import FormalConjectures.OEIS.«239957» -import FormalConjectures.OEIS.«280831» -import FormalConjectures.OEIS.«281976» -import FormalConjectures.OEIS.«287616» -import FormalConjectures.OEIS.«303656» -import FormalConjectures.OEIS.«306477» -import FormalConjectures.OEIS.«308734» -import FormalConjectures.OEIS.«34693» -import FormalConjectures.OEIS.«358684» -import FormalConjectures.OEIS.«41» -import FormalConjectures.OEIS.«56777» -import FormalConjectures.OEIS.«63880» -import FormalConjectures.OEIS.«6697» -import FormalConjectures.OEIS.«67720» -import FormalConjectures.OEIS.«80170» -import FormalConjectures.OEIS.«81091» -import FormalConjectures.OEIS.«87719» -import FormalConjectures.Other.BeaverMathOlympiad -import FormalConjectures.Other.EquationalTheories_677_255 -import FormalConjectures.Other.SchurTruncatedExponential -import FormalConjectures.Other.VCDimConvex -import FormalConjectures.Paper.CardinalityLindelof -import FormalConjectures.Paper.CasasAlvero -import FormalConjectures.Paper.CatchUpConjecture -import FormalConjectures.Paper.Chvatal -import FormalConjectures.Paper.DegreeSequencesTriangleFree -import FormalConjectures.Paper.Gourevitch -import FormalConjectures.Paper.HartshorneConjecture -import FormalConjectures.Paper.Homogenous -import FormalConjectures.Paper.Kurepa -import FormalConjectures.Paper.LatinTableau -import FormalConjectures.Paper.PrimeTuples -import FormalConjectures.Paper.Rupert -import FormalConjectures.Paper.StrongSensitivityConjecture -import FormalConjectures.Paper.WeaklyFirstCountable -import FormalConjectures.Util.Answer -import FormalConjectures.Util.Answer.Syntax -import FormalConjectures.Util.Attributes.AMS -import FormalConjectures.Util.Attributes.Basic -import FormalConjectures.Util.ForMathlib -import FormalConjectures.Util.Linters.AMSLinter -import FormalConjectures.Util.Linters.AnswerLinter -import FormalConjectures.Util.Linters.AnswerLinterTest -import FormalConjectures.Util.Linters.CategoryLinter -import FormalConjectures.Util.Linters.CopyrightLinter -import FormalConjectures.Util.Linters.NamespaceLinter -import FormalConjectures.Util.ProblemImports -import FormalConjectures.Wikipedia.ABC -import FormalConjectures.Wikipedia.AgohGiuga -import FormalConjectures.Wikipedia.Andrica -import FormalConjectures.Wikipedia.ArtinPrimitiveRootsConjecture -import FormalConjectures.Wikipedia.BalancedPrimes -import FormalConjectures.Wikipedia.BatemanHornConjecture -import FormalConjectures.Wikipedia.BealConjecture -import FormalConjectures.Wikipedia.BetrothedNumbers -import FormalConjectures.Wikipedia.BoundedBurnsideProblem -import FormalConjectures.Wikipedia.BrocardConjecture -import FormalConjectures.Wikipedia.BrocardProblem -import FormalConjectures.Wikipedia.Bunyakovsky -import FormalConjectures.Wikipedia.BusyBeaver -import FormalConjectures.Wikipedia.CarmichaelTotient -import FormalConjectures.Wikipedia.Catalan -import FormalConjectures.Wikipedia.ClassNumberProblem -import FormalConjectures.Wikipedia.CollatzConjecture -import FormalConjectures.Wikipedia.CongruentNumber -import FormalConjectures.Wikipedia.Conway99Graph -import FormalConjectures.Wikipedia.DeterminantalConjecture -import FormalConjectures.Wikipedia.Dickson -import FormalConjectures.Wikipedia.EllipticCurveRank -import FormalConjectures.Wikipedia.Euclid -import FormalConjectures.Wikipedia.EulerBrick -import FormalConjectures.Wikipedia.EulerSumOfPowers -import FormalConjectures.Wikipedia.Exponentials -import FormalConjectures.Wikipedia.FeitThompsonPrimeConjecture -import FormalConjectures.Wikipedia.Fermat -import FormalConjectures.Wikipedia.FermatCatalanConjecture -import FormalConjectures.Wikipedia.FibonacciPrimes -import FormalConjectures.Wikipedia.Firoozbakht -import FormalConjectures.Wikipedia.GaussCircleProblem -import FormalConjectures.Wikipedia.Gilbreath -import FormalConjectures.Wikipedia.GoldbachConjecture -import FormalConjectures.Wikipedia.Grimm -import FormalConjectures.Wikipedia.GromovPolynomialGrowth -import FormalConjectures.Wikipedia.Hadamard -import FormalConjectures.Wikipedia.HadwigerNelson -import FormalConjectures.Wikipedia.Hall -import FormalConjectures.Wikipedia.HappyEndingProblem -import FormalConjectures.Wikipedia.HardyLittlewood -import FormalConjectures.Wikipedia.HerzogSchonheimConjecture -import FormalConjectures.Wikipedia.InscribedSquare -import FormalConjectures.Wikipedia.InvariantSubspaceProblem -import FormalConjectures.Wikipedia.InverseGalois -import FormalConjectures.Wikipedia.Irrational -import FormalConjectures.Wikipedia.JacobianConjecture -import FormalConjectures.Wikipedia.JugglerConjecture -import FormalConjectures.Wikipedia.Kakeya -import FormalConjectures.Wikipedia.Kaplansky -import FormalConjectures.Wikipedia.Koethe -import FormalConjectures.Wikipedia.KummerVandiver -import FormalConjectures.Wikipedia.LegendreConjecture -import FormalConjectures.Wikipedia.LehmerMahlerMeasureProblem -import FormalConjectures.Wikipedia.LehmerTotient -import FormalConjectures.Wikipedia.LeinsterGroup -import FormalConjectures.Wikipedia.Lemoine -import FormalConjectures.Wikipedia.LittlewoodConjecture -import FormalConjectures.Wikipedia.LonelyRunnerConjecture -import FormalConjectures.Wikipedia.MagicSquareOfSquares -import FormalConjectures.Wikipedia.Mahler32 -import FormalConjectures.Wikipedia.Mandelbrot -import FormalConjectures.Wikipedia.MeanValueProblem -import FormalConjectures.Wikipedia.Mersenne -import FormalConjectures.Wikipedia.MinimalOverlapProblem -import FormalConjectures.Wikipedia.ModularityConjecture -import FormalConjectures.Wikipedia.MoserWorm -import FormalConjectures.Wikipedia.NoetherProblem -import FormalConjectures.Wikipedia.Oppermann -import FormalConjectures.Wikipedia.PebblingNumberConjecture -import FormalConjectures.Wikipedia.Pell -import FormalConjectures.Wikipedia.PerfectNumbers -import FormalConjectures.Wikipedia.PierceBirkhoff -import FormalConjectures.Wikipedia.PollocksConjecture -import FormalConjectures.Wikipedia.PrimesAndPerfectSquares -import FormalConjectures.Wikipedia.RamanujanTau -import FormalConjectures.Wikipedia.RationalDistanceProblem -import FormalConjectures.Wikipedia.RegularPrimes -import FormalConjectures.Wikipedia.RiemannZetaValues -import FormalConjectures.Wikipedia.Schanuel -import FormalConjectures.Wikipedia.Schinzel -import FormalConjectures.Wikipedia.Selfridge -import FormalConjectures.Wikipedia.Sendov -import FormalConjectures.Wikipedia.Singmaster -import FormalConjectures.Wikipedia.SnakeInTheBox -import FormalConjectures.Wikipedia.SparseRuler -import FormalConjectures.Wikipedia.SquarePacking -import FormalConjectures.Wikipedia.SumOfThreeCubes -import FormalConjectures.Wikipedia.Toronto -import FormalConjectures.Wikipedia.Transcendental -import FormalConjectures.Wikipedia.TwinPrimes -import FormalConjectures.Wikipedia.UnionClosed -import FormalConjectures.Wikipedia.VaughtConjecture -import FormalConjectures.Wikipedia.WallSunSun -import FormalConjectures.Wikipedia.WolstenholmePrime -import FormalConjectures.Wikipedia.WoodalPrimes -import FormalConjectures.Wikipedia.conjecture_1_3_to_2_3 -import FormalConjectures.WrittenOnTheWallII.GraphConjecture1 -import FormalConjectures.WrittenOnTheWallII.GraphConjecture19 -import FormalConjectures.WrittenOnTheWallII.GraphConjecture2 -import FormalConjectures.WrittenOnTheWallII.GraphConjecture3 -import FormalConjectures.WrittenOnTheWallII.GraphConjecture34 -import FormalConjectures.WrittenOnTheWallII.GraphConjecture4 -import FormalConjectures.WrittenOnTheWallII.GraphConjecture40 -import FormalConjectures.WrittenOnTheWallII.GraphConjecture5 -import FormalConjectures.WrittenOnTheWallII.GraphConjecture58 -import FormalConjectures.WrittenOnTheWallII.GraphConjecture6 -import FormalConjectures.WrittenOnTheWallII.Test diff --git a/Benchmarks/CompileFC/README.md b/Benchmarks/CompileFC/README.md deleted file mode 100644 index c10070222..000000000 --- a/Benchmarks/CompileFC/README.md +++ /dev/null @@ -1,19 +0,0 @@ -# CompileFC - -Runs the Ix compiler over the Lean environment of all defs from https://github.com/google-deepmind/formal-conjectures. - -The defs in CompileFC.lean were generated automatically with the following: -``` -lake update -cd .lake/packages/formal_conjectures -lake exe mk_all --lib FormalConjectures -mv FormalConjectures.lean ../../../CompileFC.lean -``` - -This project shadows the `formal-conjectures` project's Lean version, which is not always up to date. - -## Usage - -First ensure the Lean version used to build Ix matches the `Benchmarks/CompileFC/lean-toolchain` version (check against `ix --version`). Then run - -`ix compile /path/to/CompileFC.lean` diff --git a/Benchmarks/CompileFC/flake.lock b/Benchmarks/CompileFC/flake.lock deleted file mode 100644 index e2d0ab18f..000000000 --- a/Benchmarks/CompileFC/flake.lock +++ /dev/null @@ -1,117 +0,0 @@ -{ - "nodes": { - "flake-parts": { - "inputs": { - "nixpkgs-lib": "nixpkgs-lib" - }, - "locked": { - "lastModified": 1769996383, - "narHash": "sha256-AnYjnFWgS49RlqX7LrC4uA+sCCDBj0Ry/WOJ5XWAsa0=", - "owner": "hercules-ci", - "repo": "flake-parts", - "rev": "57928607ea566b5db3ad13af0e57e921e6b12381", - "type": "github" - }, - "original": { - "owner": "hercules-ci", - "repo": "flake-parts", - "type": "github" - } - }, - "flake-parts_2": { - "inputs": { - "nixpkgs-lib": "nixpkgs-lib_2" - }, - "locked": { - "lastModified": 1765835352, - "narHash": "sha256-XswHlK/Qtjasvhd1nOa1e8MgZ8GS//jBoTqWtrS1Giw=", - "owner": "hercules-ci", - "repo": "flake-parts", - "rev": "a34fae9c08a15ad73f295041fec82323541400a9", - "type": "github" - }, - "original": { - "owner": "hercules-ci", - "repo": "flake-parts", - "type": "github" - } - }, - "lean4-nix": { - "inputs": { - "flake-parts": "flake-parts_2", - "nixpkgs": "nixpkgs" - }, - "locked": { - "lastModified": 1770601541, - "narHash": "sha256-wCun5wynV3vLoVrr9gU46qI0UG4YeID6IKhPIhtsp8U=", - "owner": "lenianiva", - "repo": "lean4-nix", - "rev": "561f1a779737e109d4e03a6f967108497bbbd73f", - "type": "github" - }, - "original": { - "owner": "lenianiva", - "repo": "lean4-nix", - "type": "github" - } - }, - "nixpkgs": { - "locked": { - "lastModified": 1765779637, - "narHash": "sha256-KJ2wa/BLSrTqDjbfyNx70ov/HdgNBCBBSQP3BIzKnv4=", - "owner": "nixos", - "repo": "nixpkgs", - "rev": "1306659b587dc277866c7b69eb97e5f07864d8c4", - "type": "github" - }, - "original": { - "owner": "nixos", - "ref": "nixos-unstable", - "repo": "nixpkgs", - "type": "github" - } - }, - "nixpkgs-lib": { - "locked": { - "lastModified": 1769909678, - "narHash": "sha256-cBEymOf4/o3FD5AZnzC3J9hLbiZ+QDT/KDuyHXVJOpM=", - "owner": "nix-community", - "repo": "nixpkgs.lib", - "rev": "72716169fe93074c333e8d0173151350670b824c", - "type": "github" - }, - "original": { - "owner": "nix-community", - "repo": "nixpkgs.lib", - "type": "github" - } - }, - "nixpkgs-lib_2": { - "locked": { - "lastModified": 1765674936, - "narHash": "sha256-k00uTP4JNfmejrCLJOwdObYC9jHRrr/5M/a/8L2EIdo=", - "owner": "nix-community", - "repo": "nixpkgs.lib", - "rev": "2075416fcb47225d9b68ac469a5c4801a9c4dd85", - "type": "github" - }, - "original": { - "owner": "nix-community", - "repo": "nixpkgs.lib", - "type": "github" - } - }, - "root": { - "inputs": { - "flake-parts": "flake-parts", - "lean4-nix": "lean4-nix", - "nixpkgs": [ - "lean4-nix", - "nixpkgs" - ] - } - } - }, - "root": "root", - "version": 7 -} diff --git a/Benchmarks/CompileFC/flake.nix b/Benchmarks/CompileFC/flake.nix deleted file mode 100644 index 57b04053c..000000000 --- a/Benchmarks/CompileFC/flake.nix +++ /dev/null @@ -1,53 +0,0 @@ -{ - description = "Ix Nix flake (Lean4 + C + Rust)"; - - inputs = { - # System packages, follows lean4-nix so we stay in sync - nixpkgs.follows = "lean4-nix/nixpkgs"; - - # Lean 4 & Lake - lean4-nix.url = "github:lenianiva/lean4-nix"; - - # Helper: flake-parts for easier outputs - flake-parts.url = "github:hercules-ci/flake-parts"; - }; - - outputs = inputs @ { - nixpkgs, - flake-parts, - lean4-nix, - ... - }: - flake-parts.lib.mkFlake {inherit inputs;} { - # Systems we want to build for - systems = [ - "aarch64-darwin" - "aarch64-linux" - "x86_64-darwin" - "x86_64-linux" - ]; - - perSystem = { - system, - pkgs, - ... - }: { - # Lean overlay - _module.args.pkgs = import nixpkgs { - inherit system; - overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)]; - }; - # Provide a unified dev shell with Lean + Rust - devShells.default = pkgs.mkShell { - packages = with pkgs; [ - pkg-config - openssl - clang - lean.lean-all # Includes Lean compiler, lake, stdlib, etc. - ]; - }; - - formatter = pkgs.alejandra; - }; - }; -} diff --git a/Benchmarks/CompileFC/lake-manifest.json b/Benchmarks/CompileFC/lake-manifest.json deleted file mode 100644 index c386f41a0..000000000 --- a/Benchmarks/CompileFC/lake-manifest.json +++ /dev/null @@ -1,105 +0,0 @@ -{"version": "1.1.0", - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/google-deepmind/formal-conjectures", - "type": "git", - "subDir": null, - "scope": "", - "rev": "bfe92e43cf56f4fb5fe1a9fac0fc093acf4f88ea", - "name": "formal_conjectures", - "manifestFile": "lake-manifest.json", - "inputRev": "bfe92e43cf56f4fb5fe1a9fac0fc093acf4f88ea", - "inherited": false, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", - "name": "LeanSearchClient", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "c04225ee7c0585effbd933662b3151f01b600e40", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.85", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "55c37290ff6186e2e965d68cf853a57c0702db82", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", - "inherited": true, - "configFile": "lakefile.toml"}], - "name": "CompileFC", - "lakeDir": ".lake"} diff --git a/Benchmarks/CompileFC/lakefile.toml b/Benchmarks/CompileFC/lakefile.toml deleted file mode 100644 index 2536d3750..000000000 --- a/Benchmarks/CompileFC/lakefile.toml +++ /dev/null @@ -1,11 +0,0 @@ -name = "CompileFC" -version = "0.1.0" -defaultTargets = ["CompileFC"] - -[[lean_lib]] -name = "CompileFC" - -[[require]] -name = "formal_conjectures" -git = "https://github.com/google-deepmind/formal-conjectures" -rev = "bfe92e43cf56f4fb5fe1a9fac0fc093acf4f88ea" diff --git a/Benchmarks/CompileFC/lean-toolchain b/Benchmarks/CompileFC/lean-toolchain deleted file mode 100644 index 5249182c0..000000000 --- a/Benchmarks/CompileFC/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:v4.27.0