You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Extended 2026-11-04: this PR now also bumps cadical from 2.1.3 to 3.0.1 (the latest release) and adds an end-to-end bv_decide test to lean. It was previously a build.sh-only reproducibility fix for 2.1.3.
Policy: latest cadical, not the release Lean bundles
We run the latest upstream versions and fix what breaks. We don't pin to whatever an upstream happens to bundle. Lean 4.35 still builds rel-2.1.2 (lean4 CMakeLists.txt:71, GIT_TAG rel-2.1.2, unchanged since lean4#7347), and we deliberately don't follow that.
This is safe for soundness. bv_decide does not trust the solver: Lean bit-blasts the goal to CNF, runs cadical, and replays cadical's LRAT certificate in Lean's own verified checker. A different solver version can only make a proof fail. It cannot make Lean accept a false goal. The negative controls below show this directly: a fake cadical that claims s UNSATISFIABLE without a valid certificate is rejected with SAT solver produced invalid LRAT.
Both stale comments are fixed to say this: packages/cadical/build.ncl ("The release Lean 4.33 bundles") and packages/lean/build.ncl ("Same release Lean pins"). Both were already wrong after #999 moved us to 2.1.3.
Version check
gh release list -R arminbiere/cadical: rel-3.0.1 (2026-07-20) is Latest. The older releases are 3.0.0 (2025-12-23), 2.2.1 and 2.2.0.
The source is the GitHub tag archive (the AGENTS.md convention for GitHub sources). sha256 is 0a8ea563b5a25f5aa064634814edab45cc0e45111ea0f5d412a565f806fd7e11, and the sandbox fetch verified it.
How bv_decide calls cadical, and what changed in 3.x
It parses stdout for a leading s UNSATISFIABLE / s SATISFIABLE plus the model v lines. The solver path is <dir of lean>/cadical if that file exists, otherwise cadical on PATH (TacticContext.lean:59).
I checked 3.0.1 against each of these. Every flag still exists with the same meaning: lrat, binary (default 1), quiet, shrink (0..3), and the unsat/sat/default configs in config.cpp. The positional <input> <proof> usage and the s … result lines are unchanged. In lrattracer.cpp, the LRAT writer only switched its clause ids from uint64_t to int64_t, and the binary encoding (2*|id| + sign) is the same.
The one change that matters for proofs is BVA (factor), which adds extension variables to proofs. 3.0.0 turned it on by default; 3.0.1 turns it off again (NEWS: "Changed default value for preprocesslight and factor to zero"). That makes 3.0.1 the safer target of the two. The other 3.0.x changes are library-API breaks for incremental users (reserve→resize, declared variables) and don't touch the CLI that Lean uses.
Reproducibility in 3.0.1
scripts/make-build-header.sh now honours SOURCE_DATE_EPOCH for the date, but it still appends uname -srmn (hostname and kernel release) to build.hpp's DATE, which lands in .rodata. Changes to build.sh:
Dropped the date shim. Upstream now reads SOURCE_DATE_EPOCH itself, and the build asserts that it is set. make runs with TZ=UTC.
Kept the uname shim (kernel name and machine only) on PATH for make.
Kept the fail-closed check. The expected DATE string is computed from SOURCE_DATE_EPOCH and the pinned uname, and the build fails if build.hpp differs. The pinned string is unchanged from 2.1.3: Thu Jan 1 12:00:00 AM UTC 1970 Linux aarch64.
New in 3.x: one C file (src/kitten.c) is compiled with CC/CFLAGS, so CFLAGS now gets the same -ffile-prefix-map/-gno-record-gcc-switches flags as CXXFLAGS.
The other build.hpp inputs were re-checked for host data. VERSION comes from the tarball. The git id is empty, because git show finds no .git. COMPILER is g++ --version, and FLAGS is our CXXFLAGS. Nothing in the sources uses __DATE__/__TIME__ except the NBUILD fallback, which we don't use.
Verification (2026-11-04, remote min sessions, aarch64)
Each run used a fresh activate and --rebuild --verbose. The committed tree was built without probes. Where a hash is shown, it came from a temporary probe line that printed the hash into the build log, and that line has since been removed.
Thu Jan 1 12:00:00 AM UTC 1970 Linux (none) 6.12.114 aarch64
fails: ERROR: build/build.hpp DATE is not the pinned value
A and B are identical. N shows that upstream's own SOURCE_DATE_EPOCH handling fixes the date but leaves the host in the string, and that the check catches it. On the committed tree, min check --packages cadical passed every check, including enumerate bins, missing runtime_deps and standalone tests, with no Skip.
bv_decide compatibility, before any lean rebuild. This used a throwaway local probe package (never pushed) that depended on main's cached lean 4.35.0 and a 3.0.1 build of this recipe. The probe copied lean into a scratch bin/, so the solver next to it could be swapped:
solver next to lean
bv.lean (3 theorems)
cex.lean (false goal)
cadical 2.1.3 (current main)
proved, exit 0
counterexample x = 255#8
cadical 3.0.1
proved, exit 0
counterexample x = 255#8
none
could not execute external process 'cadical' ×3
n/a
fake: prints s UNSATISFIABLE, no proof
SAT solver produced invalid LRAT ×3
n/a
fake: prints garbage
unexpected output for each theorem, also run one at a time
n/a
The last row shows that none of the three goals is closed by bv_decide's preprocessing: each one reaches the SAT solver. The fake-UNSAT row shows the soundness argument above.
lean, with the new test
run
what
result
L
min package build --rebuild lean on the committed tree (lean re-keys onto cadical 3.0.1)
build finished, real source build, 1160 s
L
min check --packages lean
every check passes, including standalone tests (compiles_hello + the new bv_decide), no Skip
C1
negative control: test command 1 runs a copy of this lean whose sibling cadical prints garbage
standalone tests…Fail, bv_decide: … had exit code 1
C2
negative control: command 1 restored, command 2 runs that copy with no cadical anywhere (PATH=/tmp/x/bin)
standalone tests…Fail on command 2, which also shows command 1 passed for real
The controls changed only the test commands, which are not part of the package hash. Each one ran in a fresh session on lean's cached build, and neither was committed.
The new test (packages/lean, tests.bv_decide)
It runs as a lean test because lean runtime-depends on cadical, so lean's closure is what users get.
lean bv.lean must prove x * 3 = x + x + x (32-bit), (x &&& y) + (x ||| y) = x + y (32-bit), and x * y = y * x (8-bit, solverMode := .proof) by bv_decide.
lean cex.lean on the false goal x < x + 1 (8-bit) must report The prover found a counterexample. This exercises the SAT/model path. A missing solver produces a different error, so this command fails without one.
The cadical package keeps its --version and DIMACS smoke test.
Sequencing
cadical is a runtime dep of lean, so this re-keys lean and everything built on it: aeneas-latest today, and mathlib-oleans (about a 35 min build) once #1244 lands. Land this before #1244 so mathlib compiles once, on the final lean.
Other packages that vendor CaDiCaL (not changed here)
cbmc vendors rel-3.0.0 (its own tarball, built into the binary). Under the same policy it could move to 3.0.1. That release only touches the CLI signal handler, the terminator, and the factor/preprocesslight defaults, which CBMC's incremental use would actually feel, since factor off means it no longer has to declare variables. It should be a separate bump verified with CBMC's own regression. I recommend following, in its own PR.
cvc5 / cvc5-ff (pkgs#1294) pin cvc5's own rel-2.1.3-elevate branch commit (a384d22): 2.1.3 plus external-propagator fixes that cvc5's SAT layer depends on. 3.0.x breaks the library API (reserve→resize, declared variables), so these should not follow until cvc5 upstream moves. They are linked by cvc5's own FindCaDiCaL, not through this package. Also, their comment ("The fleet's cadical package is 2.1.2") is stale; that is a separate one-line fix.
No actionable comments were generated in the recent review.
Walkthrough
The CaDiCaL package moves to version 3.0.1 and checks generated build-date data during its build. Lean adds a standalone test for bit-vector proofs using CaDiCaL. Lean and Aeneas comments describe solver compatibility checks.
Changes: CaDiCaL package and Lean integration
Layer / File(s)
Summary
CaDiCaL version and reproducible build packages/cadical/build.ncl, packages/cadical/build.sh
The package uses CaDiCaL 3.0.1 and its updated source checksum. The build script applies CXXFLAGS to C compilation, uses a uname shim with TZ=UTC, requires SOURCE_DATE_EPOCH, and checks the generated DATE definition.
Lean CaDiCaL dependency and test packages/lean/build.ncl, packages/aeneas-latest/build.ncl
The Lean dependency comment describes the newer CaDiCaL release and LRAT certificate checking. A standalone test runs bit-vector proof goals and checks that a false goal produces a counterexample. The Aeneas comment describes solver call sites exercised by its library build.
gominimal/pkgs#1149: This PR adds a standalone Lean test that exercises the CaDiCaL runtime dependency and checks proof and counterexample behavior.
Possibly related PRs
gominimal/pkgs#1271: The Aeneas comment describes solver call sites at the commit pinned by that PR, although this PR does not change the pin.
Suggested reviewers:norrietaylor, mitodrummer
Merge Risk: Minimal · up to 33bc2
No actionable merge-blocking risk is established by the supplied evidence.
Pre-merge checks: 5
Check name
Status
Explanation
Description Check
Check skipped - CodeRabbit’s high-level summary is enabled.
Title check
The title names two changes that appear in the changeset: the CaDiCaL bump from 2.1.3 to 3.0.1 with a reproducible, host-pinned build, and the new bv_decide end-to-end test in Lean. The title covers b…
Docstring Coverage
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentat…
Linked Issues check
Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check
Check skipped because no linked issues were found for this pull request.
Full details: Title check
Explanation
The title names two changes that appear in the changeset: the CaDiCaL bump from 2.1.3 to 3.0.1 with a reproducible, host-pinned build, and the new bv_decide end-to-end test in Lean. The title covers both main changes, although it packs them into one line with parenthetical detail. It is specific and does not use vague wording. The title is related to the change, so the check passes.
Full details: Docstring Coverage
Explanation
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentation-only edits and deletions within surviving functions are included; unchanged diff context and fully deleted functions are excluded. Analyzed 0 functions across 1 files. (3 skipped: 3 unsupported.)
Finishing Touches
Generate unit tests (beta)
Commit to this branch
Create a new PR
Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts
Reviewing files that changed from the base of the PR and between 29b110e and 33bc21f.
Files selected for processing: 3
packages/aeneas-latest/build.ncl
packages/cadical/build.ncl
packages/lean/build.ncl
Files skipped from review as they are similar to previous changes: 1
packages/cadical/build.ncl
Included review availability: This review used your included allowance. 0 included reviews remain after this review. Your included PR review attempts over the past 7 days set your current allowance at 1 review per hour.
Verification update from the x86_64 lab box (48-core, native minimald):
4-build gauntlet, all byte-identical. Four forced real builds (min package build --rebuild, evicted between), each compared against build 1 — no differences. A double-build can clear an intermittent bug about half the time, so this is the stronger check.
One honest caveat on scope. A same-host gauntlet proves the DATE pin: both builds saw different wall-clock and now agree. It cannot prove the OS pin, because every build on one machine sees the same uname -srmn. That half is reasoned rather than measured — uname embeds the build host's kernel version and hostname, so it would differ across machines and defeat a cross-host comparison. Cross-host verification is not something this lab can run yet.
Follow-up: the uname half is now measured, not just reasoned. Two builds of unpatched cadical at the pin on the x86_64 lab box embed:
A="Thu Sep 24 10:37:47 PM UTC 2026 Linux cachyos-x8664 7.2.6-1-cachyos x86_64"
B="Thu Sep 24 10:38:52 PM UTC 2026 Linux cachyos-x8664 7.2.6-1-cachyos x86_64"
That is the build host's hostname and kernel release in .rodata, alongside the wall clock. Same-host builds only disagree on the time; any two hosts would also disagree on the rest. The earlier aarch64 run showed Linux (none) 6.12.105 aarch64 from inside the Mac's VM — a third distinct value for the same source. So the OS= pin is doing real work, not just defending a hypothetical.
… stray minimal.toml
2.1.3's scripts/make-build-header.sh is unchanged from 2.1.2: it still puts
`date` and `uname -srmn` (wall clock, hostname, kernel release) into the DATE
macro in .rodata. Instead of sed-editing the upstream script, the make step
gets pinned `date` (SOURCE_DATE_EPOCH, UTC) and `uname` (kernel name +
machine) on PATH, and a fixed-string check fails the build if build.hpp's
DATE is not the pinned value. Also reverts minimal.toml, which an earlier
commit on this branch changed by mistake (repro-lab tasks).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
bryan-minimal
changed the title
cadical: pin build date and uname in build.hpp (reproducible)
cadical: pin build.hpp's date and host (reproducible, 2.1.3)
Oct 23, 2026
Reworked for cadical 2.1.3 (now on main via #999) in d45d1b9, on a merge of main. 2.1.3's make-build-header.sh is unchanged, so both pins are still needed. They now go in through PATH shims for date and uname, with a fail-closed header check, instead of a sed on the upstream script. Two fresh-session builds are byte-identical (dc05982c…), and the unfixed main recipe built twice differs (f0467e6d… vs f46e68f2…). The table is in the body. The stray minimal.toml change is reverted. Leaving this as a draft.
Bump cadical 2.1.3 -> 3.0.1. Policy: run the latest release, not the
rel-2.1.2 Lean's CMake bundles. bv_decide replays cadical's LRAT
certificate in Lean's checker, so a newer solver can only make a proof
fail, never make lean accept a false goal. Fix both stale comments.
3.0.1's make-build-header.sh honours SOURCE_DATE_EPOCH, so the date
shim goes; the uname shim (no hostname/kernel release), TZ=UTC and the
fail-closed DATE check stay. CFLAGS gets the repro flags for the new
C file (kitten.c).
lean gains a bv_decide standalone test: three SAT-reaching BitVec
theorems must be proved, and a false goal must yield a counterexample.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
bryan-minimal
changed the title
cadical: pin build.hpp's date and host (reproducible, 2.1.3)
cadical 3.0.1, reproducible (pinned build.hpp host); bv_decide end-to-end test
Nov 5, 2026
The reason will be displayed to describe this comment to others. Learn more.
Scope matches the title and the extended PR body. All three files trace to the bump, the reproducibility fix or the new test. Clobber none: git log on packages/cadical and packages/lean/build.ncl shows the 2.1.3 update and lean 4.35.0 are intact. The dropped date shim is an intended replacement. Correctness the uname shim, the heredoc quoting, the fail-closed DATE check and both test commands read correctly. The second test command ends on grep -q, so its exit code is the check. One finding: the PR does not show that aeneas-latest builds on 3.0.1. Coverage note the new test runs the default and .proof solver modes, but not .counterexample (--sat). Not checked the download of the 3.0.1 tarball was denied in this environment. So the sha256, scripts/make-build-header.sh, the configure handling of CFLAGS, and the PR's flag claims are taken from the PR body. FLAGS carries the raw $(pwd) from CXXFLAGS into build.hpp, and the fail-closed check covers only DATE. The PR's identical A and B hashes show that the path was stable in those runs. I could not confirm that the path is stable on all build hosts. No build was run.
The reason will be displayed to describe this comment to others. Learn more.
medium · This comment says that lean's bv_decide standalone test catches a proof that a solver change breaks. That test proves three small goals. The real consumer is aeneas-latest: its library build runs Bvify's #guard_msgs examples through cadical (packages/aeneas-latest/build.ncl:116). The PR says the bump re-keys aeneas-latest, but its verification tables list no aeneas-latest build on 3.0.1. If an example fails on 3.0.1, for example from a timeout or changed output, the aeneas-latest build fails after merge. ci_scope.py includes aeneas-latest in the scoped check, but its only test is imports_aeneas, and I could not confirm that the check rebuilds it. I did not read the Bvify examples. Build aeneas-latest on this head before merge and record the result. Also narrow the comment to what the test shows. This is one instance: lean and aeneas-latest are the only users of this package for bv_decide.
The reason will be displayed to describe this comment to others. Learn more.
Agreed, the comment claimed too much. Fixed in 33bc21f.
What aeneas-latest runs. I read the source tarball it pins (aeneas-ab34bd2, sha256 matches build.ncl) and walked the import closure of lake build Aeneas (266 modules). The build runs 60 solver call sites:
9 bv_decide: 8 examples in Tactic/Conv/Bvify/Bvify.lean and 1 in Bvify/Lemmas.lean.
51 bv_tac, which ends in bvDecide: 12 examples in Solver/BvTac/BvTac.lean, 9 in BvTac/Tests.lean and 30 named simp lemmas in BvTac/Lemmas.lean. The lemmas use widths up to 128 bits.
Most of these are plain examples and lemmas, not #guard_msgs. Only one of Bvify's three #guard_msgs blocks ends in bv_decide, and it checks extract_goal's output. Some goals may be closed by bv_decide's preprocessing before cadical runs, so 60 is an upper bound on solver runs. A failing call fails the library build.
aeneas-latest was already built on 3.0.1. The build-bot's minimal build check on the previous head 29b110e (check run 127023925222) lists aeneas-latest under "packages this run built", with amd64 and arm64 both passing. That is a full library build against cadical 3.0.1 on both arches. The new head gets the same.
Changes
cadical/build.ncl: the comment now separates the two checks. lean's bv_decide test is a smoke test: cadical is found, lean accepts its certificates and a false goal is refuted. aeneas-latest's build covers real goals and gives the count.
lean/build.ncl: the test gains csub, Aeneas's ML-KEM conditional-subtraction goal from Bvify.lean, restated on plain BitVec 32 so it needs no Aeneas import. With a fake cadical it fails, so it reaches the solver. With a weakened bound it gets a counterexample. It takes under a second. I measured that locally with lean 4.34.1 and its bundled cadical 2.1.2. 3.0.1 is untested until the build-bot runs the test on this head.
aeneas-latest/build.ncl: the comment on its cadical dep is corrected. It said Bvify's #guard_msgs; it now gives the call sites. Comment only.
The .counterexample mode from your summary is not addressed here.
…de goal
Review on #757: the cadical comment credited lean's bv_decide standalone
test with catching a solver change that breaks proofs, but that test proves
small goals. The real consumer is aeneas-latest, whose `lake build Aeneas`
runs 60 bv_decide/bv_tac call sites (9 bv_decide in Bvify, 51 bv_tac in
BvTac's examples, Tests and simp lemmas, 8- to 128-bit). The comments now
say which check covers what: lean's test is a smoke test, and
aeneas-latest's build covers real goals. The build-bot rebuilds
aeneas-latest when cadical changes.
lean's test gains `csub`, Aeneas's ML-KEM conditional-subtraction goal
(Bvify.lean) restated on plain BitVec 32. It reaches the solver (a fake
cadical makes it fail) and takes under a second (lean 4.34.1 + cadical
2.1.2 locally). A weakened bound is refuted with a counterexample.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The reason will be displayed to describe this comment to others. Learn more.
Scope matches the title. All four files trace to the cadical bump, the reproducibility recipe or the bv_decide test. The aeneas-latest change is a comment only.
Clobber none. git log on the changed paths shows the 2.1.3 shim work in d45d1b9c. This PR replaces its date shim on purpose, because 3.x reads SOURCE_DATE_EPOCH. The uname shim and the fail-closed check stay.
Correctness I read build.sh line by line. The heredoc quoting, the uname shim and the DATE check are correct as far as the repo shows. The test commands contain no %{, so Nickel does not interpolate them. The cex.lean command gates on grep, which is the intended result because lean exits nonzero there. No other package imports cadical except lean and aeneas-latest. cbmc, cvc5 and cvc5-ff fetch their own CaDiCaL. The earlier thread on aeneas-latest coverage has an answer, and I do not raise it again. The findings are one comment claim about FLAGS, one unmeasured timing claim, and two comment nits.
Not checked Network reads were denied in this run. I did not read the upstream 3.0.1 sources, so make-build-header.sh, configure and the CC default are taken from the PR body. I did not read CI status, so I cannot confirm that csub passes on 3.0.1 at this head. I did not recount the 60 Aeneas call sites, because the tarball was not available. I built nothing.
The reason will be displayed to describe this comment to others. Learn more.
low · This comment calls FLAGS deterministic, but FLAGS is CXXFLAGS, and line 4 puts the absolute build directory in CXXFLAGS through -ffile-prefix-map=$(pwd)=/builddir. The prefix map does not rewrite a string literal, so that path lands in .rodata next
10000
to DATE. The output changes if the sandbox working directory ever changes, and the fail-closed check covers only DATE. packages/kissat/build.sh:4-5 lists the build directory as host data for this same class of header. Runs A and B in the PR match, so the path is stable today. Correct the comment to say that FLAGS depends on a stable build path, or extend the check to the FLAGS line. I did not read the upstream script, so this rests on the PR statement that FLAGS is our CXXFLAGS. The $(pwd) flag is common in this repo, but an embedded flag string is specific to this header shape.
The reason will be displayed to describe this comment to others. Learn more.
low · "It takes under a second" states a measurement for this lean and cadical pair, but the author measured it on another pair. The reply on this PR says the time came from lean 4.34.1 with its bundled cadical 2.1.2, and that 3.0.1 was untested at that point. The claim matters because bv_decide has a solver timeout, so a reader can take this goal as safe from timeouts on 3.0.1. Measure it on lean 4.35.0 with cadical 3.0.1, or remove the sentence. This is one instance.
The reason will be displayed to describe this comment to others. Learn more.
nit · The counts here (60 call sites, 9 and 51, 30 simp lemmas) describe one aeneas_sha. They go stale on the next aeneas bump, and no bump updates this file. The same count is in packages/aeneas-latest/build.ncl:117. Line 9 has the same shape with rel-2.1.2. The comment that this PR replaces went stale in this way ("The release Lean 4.33 bundles"). Say "dozens of solver call sites" here, and keep any exact count in one place beside aeneas_sha.
The reason will be displayed to describe this comment to others. Learn more.
nit · The rewritten comment keeps "lean releases bundle it, ours doesn't" as the reason for this dep. That reason is out of date, because packages/lean/build.ncl:46 lists cadical in runtime_deps, and AGENTS.md says the runtime deps of a build_deps entry reach the build. So this build gets cadical through lean. Remove the dep, or say that it is an explicit marker for the build's use of the solver.
…neas-latest-on-mathlib
Resolve packages/aeneas-latest/build.ncl: keep this PR's build_deps (make, jq;
no cache tool, so no toolchain/leangz) and take #757's cadical comment.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Policy: latest cadical, not the release Lean bundles
We run the latest upstream versions and fix what breaks. We don't pin to whatever an upstream happens to bundle. Lean 4.35 still builds
rel-2.1.2(lean4CMakeLists.txt:71,GIT_TAG rel-2.1.2, unchanged since lean4#7347), and we deliberately don't follow that.This is safe for soundness.
bv_decidedoes not trust the solver: Lean bit-blasts the goal to CNF, runs cadical, and replays cadical's LRAT certificate in Lean's own verified checker. A different solver version can only make a proof fail. It cannot make Lean accept a false goal. The negative controls below show this directly: a fakecadicalthat claimss UNSATISFIABLEwithout a valid certificate is rejected withSAT solver produced invalid LRAT.Both stale comments are fixed to say this:
packages/cadical/build.ncl("The release Lean 4.33 bundles") andpackages/lean/build.ncl("Same release Lean pins"). Both were already wrong after #999 moved us to 2.1.3.Version check
gh release list -R arminbiere/cadical: rel-3.0.1 (2026-07-20) is Latest. The older releases are 3.0.0 (2025-12-23), 2.2.1 and 2.2.0.0a8ea563b5a25f5aa064634814edab45cc0e45111ea0f5d412a565f806fd7e11, and the sandbox fetch verified it.How
bv_decidecalls cadical, and what changed in 3.xlean4 v4.35.0
src/Lean/Meta/Tactic/BVDecide/External.leansatQuery:It parses stdout for a leading
s UNSATISFIABLE/s SATISFIABLEplus the modelvlines. The solver path is<dir of lean>/cadicalif that file exists, otherwisecadicalonPATH(TacticContext.lean:59).I checked 3.0.1 against each of these. Every flag still exists with the same meaning:
lrat,binary(default 1),quiet,shrink(0..3), and theunsat/sat/defaultconfigs inconfig.cpp. The positional<input> <proof>usage and thes …result lines are unchanged. Inlrattracer.cpp, the LRAT writer only switched its clause ids fromuint64_ttoint64_t, and the binary encoding (2*|id| + sign) is the same.The one change that matters for proofs is BVA (
factor), which adds extension variables to proofs. 3.0.0 turned it on by default; 3.0.1 turns it off again (NEWS: "Changed default value forpreprocesslightandfactorto zero"). That makes 3.0.1 the safer target of the two. The other 3.0.x changes are library-API breaks for incremental users (reserve→resize, declared variables) and don't touch the CLI that Lean uses.Reproducibility in 3.0.1
scripts/make-build-header.shnow honoursSOURCE_DATE_EPOCHfor the date, but it still appendsuname -srmn(hostname and kernel release) tobuild.hpp'sDATE, which lands in.rodata. Changes tobuild.sh:dateshim. Upstream now readsSOURCE_DATE_EPOCHitself, and the build asserts that it is set.makeruns withTZ=UTC.unameshim (kernel name and machine only) onPATHformake.DATEstring is computed fromSOURCE_DATE_EPOCHand the pinneduname, and the build fails ifbuild.hppdiffers. The pinned string is unchanged from 2.1.3:Thu Jan 1 12:00:00 AM UTC 1970 Linux aarch64.src/kitten.c) is compiled withCC/CFLAGS, soCFLAGSnow gets the same-ffile-prefix-map/-gno-record-gcc-switchesflags asCXXFLAGS.The other
build.hppinputs were re-checked for host data.VERSIONcomes from the tarball. The git id is empty, becausegit showfinds no.git.COMPILERisg++ --version, andFLAGSis ourCXXFLAGS. Nothing in the sources uses__DATE__/__TIME__except theNBUILDfallback, which we don't use.Verification (2026-11-04, remote
minsessions, aarch64)Each run used a fresh
activateand--rebuild --verbose. The committed tree was built without probes. Where a hash is shown, it came from a temporary probe line that printed the hash into the build log, and that line has since been removed.cadical 3.0.1
usr/bin/cadicalsha256build.hppDATE8fb0590f12f5f0380199bddaa3088003e4a6b76ac335bda7a1d435b704b81951Thu Jan 1 12:00:00 AM UTC 1970 Linux aarch648fb0590f12f5f0380199bddaa3088003e4a6b76ac335bda7a1d435b704b81951unameshim removed frommake(negative control)Thu Jan 1 12:00:00 AM UTC 1970 Linux (none) 6.12.114 aarch64ERROR: build/build.hpp DATE is not the pinned valueA and B are identical. N shows that upstream's own
SOURCE_DATE_EPOCHhandling fixes the date but leaves the host in the string, and that the check catches it. On the committed tree,min check --packages cadicalpassed every check, including enumerate bins, missing runtime_deps and standalone tests, with no Skip.bv_decidecompatibility, before any lean rebuild. This used a throwaway local probe package (never pushed) that depended on main's cached lean 4.35.0 and a 3.0.1 build of this recipe. The probe copiedleaninto a scratchbin/, so the solver next to it could be swapped:bv.lean(3 theorems)cex.lean(false goal)x = 255#8x = 255#8could not execute external process 'cadical'×3s UNSATISFIABLE, no proofSAT solver produced invalid LRAT×3unexpected outputfor each theorem, also run one at a timeThe last row shows that none of the three goals is closed by
bv_decide's preprocessing: each one reaches the SAT solver. The fake-UNSAT row shows the soundness argument above.lean, with the new test
min package build --rebuild leanon the committed tree (lean re-keys onto cadical 3.0.1)min check --packages leanstandalone tests(compiles_hello+ the newbv_decide), no Skipcadicalprints garbagebv_decide: … had exit code 1cadicalanywhere (PATH=/tmp/x/bin)The controls changed only the test commands, which are not part of the package hash. Each one ran in a fresh session on lean's cached build, and neither was committed.
The new test (
packages/lean,tests.bv_decide)It runs as a lean test because lean runtime-depends on cadical, so lean's closure is what users get.
lean bv.leanmust provex * 3 = x + x + x(32-bit),(x &&& y) + (x ||| y) = x + y(32-bit), andx * y = y * x(8-bit,solverMode := .proof) bybv_decide.lean cex.leanon the false goalx < x + 1(8-bit) must reportThe prover found a counterexample. This exercises the SAT/model path. A missing solver produces a different error, so this command fails without one.The cadical package keeps its
--versionand DIMACS smoke test.Sequencing
cadicalis a runtime dep oflean, so this re-keysleanand everything built on it:aeneas-latesttoday, andmathlib-oleans(about a 35 min build) once #1244 lands. Land this before #1244 so mathlib compiles once, on the final lean.Other packages that vendor CaDiCaL (not changed here)
cbmcvendorsrel-3.0.0(its own tarball, built into the binary). Under the same policy it could move to 3.0.1. That release only touches the CLI signal handler, the terminator, and thefactor/preprocesslightdefaults, which CBMC's incremental use would actually feel, sincefactoroff means it no longer has to declare variables. It should be a separate bump verified with CBMC's own regression. I recommend following, in its own PR.cvc5/cvc5-ff(pkgs#1294) pin cvc5's ownrel-2.1.3-elevatebranch commit (a384d22): 2.1.3 plus external-propagator fixes that cvc5's SAT layer depends on. 3.0.x breaks the library API (reserve→resize, declared variables), so these should not follow until cvc5 upstream moves. They are linked by cvc5's ownFindCaDiCaL, not through this package. Also, their comment ("The fleet'scadicalpackage is 2.1.2") is stale; that is a separate one-line fix.Relates to gominimal/inbox#253.
🤖 Generated with Claude Code
Summary by CodeRabbit