chore: Update Lean to v4.33.1#593

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
argument-ci-bot wants to merge 4 commits into from
Closed

chore: Update Lean to v4.33.1 #593

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
0ba9a4d
ci: Exclude CompileFC from lean-update
samuelburnham Aug 27, 2026
024bc51
lakefile: drop Blake3 from the native-decide dynlib
samuelburnham Aug 28, 2026
cdcc54b
ci: Glob Benchmarks and exclude CompileFC by name
samuelburnham Aug 28, 2026
a82579a
chore: Update lean4-nix to e014934
samuelburnham Aug 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
37 changes: 24 additions & 13 deletions .github/workflows/update.yml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -24,20 +24,31 @@ jobs:
client-id: ${{ secrets.TOKEN_APP_ID }}
private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}

# `dev` carries the fork's bump_mode/release_channel support; `main` only
# mirrors upstream, which silently ignores these inputs. A PR is opened
# on an update/lean-{release} branch whether or not the build passes, so
# an incompatible release shows up as a failing PR to review. Dependencies
# pinned to a Lean version tag move with the toolchain; a dependency
# pinned to a commit hash is reported and left alone.
- uses: argumentcomputer/lean-update@dev
# `exclude-dir` carries the fork's bump_mode/release_channel support plus
# the `!` exclusion syntax below; `main` only mirrors upstream, which
# silently ignores these inputs. Move back to `dev` once the exclusion
# lands there. A PR is opened on an update/lean-{release} branch whether
# or not the build passes, so an incompatible release shows up as a
# failing PR to review. Dependencies pinned to a Lean version tag move
# with the toolchain; a dependency pinned to a commit hash is reported
# and left alone.
- uses: argumentcomputer/lean-update@exclude-dir
with:
# 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.
lake_package_directory: ". Benchmarks/**"
# The root package plus the benchmark packages. `/**` walks a whole
# subtree, reaching packages nested inside another package (Catalog's
# relocation fixtures, Compile's TruthMines) and skipping dotted
# directories so `.lake` dependency checkouts are never swept up.
#
# `!` subtracts a directory and everything beneath it, so the glob can
# cover Benchmarks while sparing CompileFC, which must stay pinned: it
# builds against formal-conjectures at a commit hash, which the action
# leaves alone, so moving its toolchain off v4.27.0 only breaks the
# build. An exclusion takes no glob of its own, and one matching
# nothing is reported in the log rather than passing silently.
lake_package_directory: >-
.
Benchmarks/**
!Benchmarks/CompileFC
bump_mode: pinned-tags
pr: true
token: ${{ steps.app-token.outputs.token }}
6 changes: 3 additions & 3 deletions flake.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

39 changes: 16 additions & 23 deletions lakefile.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -7,13 +7,15 @@ package ix where
require LSpec from git
"https://github.com/argumentcomputer/LSpec" @ "ab4d5eb461941837f48eb891be755c8c73e89fdd"

/- Blake3's `blake3_rs_shared` target builds `blake3-rs` as a `cdylib`
alongside the staticlib. `ix_native_decide_dynlib` fetches it to supply the
BLAKE3 backend to Lean's native evaluator, and that dynlib gates every
`IxTcVerify` module, so this pin must stay at or after the revision that
introduced the target. -/
/- Blake3 precompiles its libraries, so Lake loads their shared objects -- which
bundle the C and Rust FFI objects -- into any process elaborating a module that
imports them. That is what supplies the BLAKE3 backend to Lean's native evaluator
for the `native_decide` proofs in `IxTcVerify`, so this pin must stay at or after
the revision that turned precompilation on. Before it, Blake3 exposed a
`blake3_rs_shared` cdylib that `ix_native_decide_dynlib` had to fetch and link;
that target no longer exists. -/
require Blake3 from git
"https://github.com/argumentcomputer/Blake3.lean" @ "1b0fbd2bd78b2b873e14264037af8c8b1536b9e9"
"https://github.com/argumentcomputer/Blake3.lean" @ "5ff5e70b6c7fc371cc6b454b83844f1f5b44ac96"

require Cli from git
"https://github.com/leanprover/lean4-cli" @ "v4.33.0"
Expand DownExpand Up@@ -197,29 +199,20 @@ opaque `@[extern]` it reaches, both symbol layers must be loadable up front:
* the raw Rust symbol it forwards to, taken from that crate's `cdylib`, recorded
by absolute path so no `LD_LIBRARY_PATH` is needed.

Covered externs: `Blake3.Rust` hashing (with the `Blake3` base module, which
holds the `HasherOps.hash` orchestration `Address.blake3` calls) against
`blake3_rs`, and `Ix.Unsigned.toLEBytes` against `ix-ffi-dyn`. -/
Covers Ix's own externs only -- currently `Ix.Unsigned.toLEBytes` against
`ix-ffi-dyn`. Blake3's are not here: that package precompiles its libraries, so
Lake loads their shared objects into the elaborating process by itself. -/
target ix_native_decide_dynlib pkg : Dynlib := do
let some blake3Base ← findModule? `Blake3
| error "module `Blake3` not found; is the Blake3 dependency available?"
let some blake3Rust ← findModule? `Blake3.Rust
| error "module `Blake3.Rust` not found; is the Blake3 dependency available?"
let some ixUnsigned ← findModule? `Ix.Unsigned
| error "module `Ix.Unsigned` not found"
-- Raw symbols come from each crate's cdylib, recorded by path, and are built
-- by fetching the owning package's target (no direct cargo calls here):
-- Blake3 via its `blake3_rs_shared`, Ix via the minimal `ix_ffi_dyn`.
let blake3Cdylib := (← blake3Rust.pkg.fetchTargetJob `blake3_rs_shared).map fun _ =>
blake3Rust.pkg.dir / "rust" / "target" / "release" / nameToSharedLib "blake3_rs"
-- Raw symbols come from the crate's cdylib, recorded by path, and are built
-- by fetching the owning target (no direct cargo calls here).
let ixCdylib ← ix_ffi_dyn.fetch
-- Boxed entry points are Lean's own generated objects for the declaring modules.
let mut boxedObjs := #[]
for mod in #[blake3Base, blake3Rust, ixUnsigned] do
boxedObjs := boxedObjs ++ (← (mod.nativeFacets true).mapM (·.fetch mod))
-- Boxed entry points are Lean's own generated objects for the declaring module.
let boxedObjs ← (ixUnsigned.nativeFacets true).mapM (·.fetch ixUnsigned)
buildSharedLib "ix_native_decide"
(pkg.buildDir / nameToSharedLib "ix_native_decide")
(boxedObjs.push blake3Cdylib |>.push ixCdylib) #[]
(boxedObjs.push ixCdylib) #[]

/- Formal verification of `Ix.Tc` against the lean4lean `Theory` spec.
Non-default: `lake build ix` never
Expand Down
, 'i'); if (__m === '*' || __re.test(location.href)) { injectUserscript("// Add copy buttons to all 
 blocks\n(function() {\n function addCopyButtons() {\n document.querySelectorAll('pre code').forEach(function(codeBlock) {\n if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;\n codeBlock.parentElement.setAttribute('data-copy-added', 'true');\n \n var btn = document.createElement('button');\n btn.textContent = 'Copy';\n btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';\n btn.onmouseover = function() { this.style.opacity = '1'; };\n btn.onmouseout = function() { this.style.opacity = '0.7'; };\n btn.onclick = function() {\n navigator.clipboard.writeText(codeBlock.textContent).then(function() {\n btn.textContent = 'Copied!';\n setTimeout(function() { btn.textContent = 'Copy'; }, 1500);\n });\n };\n codeBlock.parentElement.style.position = 'relative';\n codeBlock.parentElement.appendChild(btn);\n });\n }\n \n addCopyButtons();\n \n // Re-run on dynamic content\n var observer = new MutationObserver(addCopyButtons);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Add Copy Buttons to Code Blocks");
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '

Skip to content
chore: Update Lean to v4.33.1#593

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Closed

argument-ci-bot
wants to merge
4
commits into

from

 Closed


chore: Update Lean to v4.33.1
#593
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


4 commits


Select commit
Hold shift + click to select a range
0ba9a4d

ci: Exclude CompileFC from lean-update


samuelburnham Aug 27, 2026
024bc51

lakefile: drop Blake3 from the native-decide dynlib


samuelburnham Aug 28, 2026
cdcc54b

ci: Glob Benchmarks and exclude CompileFC by name


samuelburnham Aug 28, 2026
a82579a

chore: Update lean4-nix to e014934


samuelburnham Aug 28, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


37 changes: 24 additions & 13 deletions
.github/workflows/update.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -24,20 +24,31 @@ jobs:
 client-id: ${{ secrets.TOKEN_APP_ID }}
 private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}

 # `dev` carries the fork's bump_mode/release_channel support; `main` only
 # mirrors upstream, which silently ignores these inputs. A PR is opened
 # on an update/lean-{release} branch whether or not the build passes, so
 # an incompatible release shows up as a failing PR to review. Dependencies
 # pinned to a Lean version tag move with the toolchain; a dependency
 # pinned to a commit hash is reported and left alone.
 - uses: argumentcomputer/lean-update@dev
 # `exclude-dir` carries the fork's bump_mode/release_channel support plus
 # the `!` exclusion syntax below; `main` only mirrors upstream, which
 # silently ignores these inputs. Move back to `dev` once the exclusion
 # lands there. A PR is opened on an update/lean-{release} branch whether
 # or not the build passes, so an incompatible release shows up as a
 # failing PR to review. Dependencies pinned to a Lean version tag move
 # with the toolchain; a dependency pinned to a commit hash is reported
 # and left alone.
 - uses: argumentcomputer/lean-update@exclude-dir
 with:
 # 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.
 lake_package_directory: ". Benchmarks/**"
 # The root package plus the benchmark packages. `/**` walks a whole
 # subtree, reaching packages nested inside another package (Catalog's
 # relocation fixtures, Compile's TruthMines) and skipping dotted
 # directories so `.lake` dependency checkouts are never swept up.
 #
 # `!` subtracts a directory and everything beneath it, so the glob can
 # cover Benchmarks while sparing CompileFC, which must stay pinned: it
 # builds against formal-conjectures at a commit hash, which the action
 # leaves alone, so moving its toolchain off v4.27.0 only breaks the
 # build. An exclusion takes no glob of its own, and one matching
 # nothing is reported in the log rather than passing silently.
 lake_package_directory: >-
 .
 Benchmarks/**
 !Benchmarks/CompileFC
 bump_mode: pinned-tags
 pr: true
 token: ${{ steps.app-token.outputs.token }}

6 changes: 3 additions & 3 deletions
flake.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


39 changes: 16 additions & 23 deletions
lakefile.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -7,13 +7,15 @@ package ix where
require LSpec from git
 "https://github.com/argumentcomputer/LSpec" @ "ab4d5eb461941837f48eb891be755c8c73e89fdd"

/- Blake3's `blake3_rs_shared` target builds `blake3-rs` as a `cdylib`
alongside the staticlib. `ix_native_decide_dynlib` fetches it to supply the
BLAKE3 backend to Lean's native evaluator, and that dynlib gates every
`IxTcVerify` module, so this pin must stay at or after the revision that
introduced the target. -/
/- Blake3 precompiles its libraries, so Lake loads their shared objects -- which
bundle the C and Rust FFI objects -- into any process elaborating a module that
imports them. That is what supplies the BLAKE3 backend to Lean's native evaluator
for the `native_decide` proofs in `IxTcVerify`, so this pin must stay at or after
the revision that turned precompilation on. Before it, Blake3 exposed a
`blake3_rs_shared` cdylib that `ix_native_decide_dynlib` had to fetch and link;
that target no longer exists. -/
require Blake3 from git
 "https://github.com/argumentcomputer/Blake3.lean" @ "1b0fbd2bd78b2b873e14264037af8c8b1536b9e9"
 "https://github.com/argumentcomputer/Blake3.lean" @ "5ff5e70b6c7fc371cc6b454b83844f1f5b44ac96"

require Cli from git
 "https://github.com/leanprover/lean4-cli" @ "v4.33.0"
Expand DownExpand Up@@ -197,29 +199,20 @@ opaque `@[extern]` it reaches, both symbol layers must be loadable up front:
* the raw Rust symbol it forwards to, taken from that crate's `cdylib`, recorded
 by absolute path so no `LD_LIBRARY_PATH` is needed.

Covered externs: `Blake3.Rust` hashing (with the `Blake3` base module, which
holds the `HasherOps.hash` orchestration `Address.blake3` calls) against
`blake3_rs`, and `Ix.Unsigned.toLEBytes` against `ix-ffi-dyn`. -/
Covers Ix's own externs only -- currently `Ix.Unsigned.toLEBytes` against
`ix-ffi-dyn`. Blake3's are not here: that package precompiles its libraries, so
Lake loads their shared objects into the elaborating process by itself. -/
target ix_native_decide_dynlib pkg : Dynlib := do
 let some blake3Base ← findModule? `Blake3
 | error "module `Blake3` not found; is the Blake3 dependency available?"
 let some blake3Rust ← findModule? `Blake3.Rust
 | error "module `Blake3.Rust` not found; is the Blake3 dependency available?"
 let some ixUnsigned ← findModule? `Ix.Unsigned
 | error "module `Ix.Unsigned` not found"
 -- Raw symbols come from each crate's cdylib, recorded by path, and are built
 -- by fetching the owning package's target (no direct cargo calls here):
 -- Blake3 via its `blake3_rs_shared`, Ix via the minimal `ix_ffi_dyn`.
 let blake3Cdylib := (← blake3Rust.pkg.fetchTargetJob `blake3_rs_shared).map fun _ =>
 blake3Rust.pkg.dir / "rust" / "target" / "release" / nameToSharedLib "blake3_rs"
 -- Raw symbols come from the crate's cdylib, recorded by path, and are built
 -- by fetching the owning target (no direct cargo calls here).
 let ixCdylib ← ix_ffi_dyn.fetch
 -- Boxed entry points are Lean's own generated objects for the declaring modules.
 let mut boxedObjs := #[]
 for mod in #[blake3Base, blake3Rust, ixUnsigned] do
 boxedObjs := boxedObjs ++ (← (mod.nativeFacets true).mapM (·.fetch mod))
 -- Boxed entry points are Lean's own generated objects for the declaring module.
 let boxedObjs ← (ixUnsigned.nativeFacets true).mapM (·.fetch ixUnsigned)
 buildSharedLib "ix_native_decide"
 (pkg.buildDir / nameToSharedLib "ix_native_decide")
 (boxedObjs.push blake3Cdylib |>.push ixCdylib) #[]
 (boxedObjs.push ixCdylib) #[]

/- Formal verification of `Ix.Tc` against the lean4lean `Theory` spec.
Non-default: `lake build ix` never
Expand Down

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Force GitHub README to respect dark mode\n(function() {\n var style = document.createElement('style');\n style.textContent = '\n .markdown-body {\n color-scheme: dark light;\n }\n .markdown-body pre { background: #161b22 !important; }\n .markdown-body code { background: rgba(110, 118, 129, 0.4) !important; }\n .markdown-body table th, .markdown-body table td { border-color: #30363d !important; }\n .markdown-body img { background: #0d1117; }\n .markdown-body blockquote { border-left-color: #8b949e; }\n .markdown-body hr { border-color: #30363d; }\n ';\n document.head.appendChild(style);\n})();", "GitHub Dark Mode README Fix");
}
} catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
chore: Update Lean to v4.33.1#593

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Closed

argument-ci-bot
wants to merge
4
commits into

from

 Closed


chore: Update Lean to v4.33.1
#593
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


4 commits


Select commit
Hold shift + click to select a range
0ba9a4d

ci: Exclude CompileFC from lean-update


samuelburnham Aug 27, 2026
024bc51

lakefile: drop Blake3 from the native-decide dynlib


samuelburnham Aug 28, 2026
cdcc54b

ci: Glob Benchmarks and exclude CompileFC by name


samuelburnham Aug 28, 2026
a82579a

chore: Update lean4-nix to e014934


samuelburnham Aug 28, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


37 changes: 24 additions & 13 deletions
.github/workflows/update.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -24,20 +24,31 @@ jobs:
 client-id: ${{ secrets.TOKEN_APP_ID }}
 private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}

 # `dev` carries the fork's bump_mode/release_channel support; `main` only
 # mirrors upstream, which silently ignores these inputs. A PR is opened
 # on an update/lean-{release} branch whether or not the build passes, so
 # an incompatible release shows up as a failing PR to review. Dependencies
 # pinned to a Lean version tag move with the toolchain; a dependency
 # pinned to a commit hash is reported and left alone.
 - uses: argumentcomputer/lean-update@dev
 # `exclude-dir` carries the fork's bump_mode/release_channel support plus
 # the `!` exclusion syntax below; `main` only mirrors upstream, which
 # silently ignores these inputs. Move back to `dev` once the exclusion
 # lands there. A PR is opened on an update/lean-{release} branch whether
 # or not the build passes, so an incompatible release shows up as a
 # failing PR to review. Dependencies pinned to a Lean version tag move
 # with the toolchain; a dependency pinned to a commit hash is reported
 # and left alone.
 - uses: argumentcomputer/lean-update@exclude-dir
 with:
 # 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.
 lake_package_directory: ". Benchmarks/**"
 # The root package plus the benchmark packages. `/**` walks a whole
 # subtree, reaching packages nested inside another package (Catalog's
 # relocation fixtures, Compile's TruthMines) and skipping dotted
 # directories so `.lake` dependency checkouts are never swept up.
 #
 # `!` subtracts a directory and everything beneath it, so the glob can
 # cover Benchmarks while sparing CompileFC, which must stay pinned: it
 # builds against formal-conjectures at a commit hash, which the action
 # leaves alone, so moving its toolchain off v4.27.0 only breaks the
 # build. An exclusion takes no glob of its own, and one matching
 # nothing is reported in the log rather than passing silently.
 lake_package_directory: >-
 .
 Benchmarks/**
 !Benchmarks/CompileFC
 bump_mode: pinned-tags
 pr: true
 token: ${{ steps.app-token.outputs.token }}

6 changes: 3 additions & 3 deletions
flake.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


39 changes: 16 additions & 23 deletions
lakefile.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -7,13 +7,15 @@ package ix where
require LSpec from git
 "https://github.com/argumentcomputer/LSpec" @ "ab4d5eb461941837f48eb891be755c8c73e89fdd"

/- Blake3's `blake3_rs_shared` target builds `blake3-rs` as a `cdylib`
alongside the staticlib. `ix_native_decide_dynlib` fetches it to supply the
BLAKE3 backend to Lean's native evaluator, and that dynlib gates every
`IxTcVerify` module, so this pin must stay at or after the revision that
introduced the target. -/
/- Blake3 precompiles its libraries, so Lake loads their shared objects -- which
bundle the C and Rust FFI objects -- into any process elaborating a module that
imports them. That is what supplies the BLAKE3 backend to Lean's native evaluator
for the `native_decide` proofs in `IxTcVerify`, so this pin must stay at or after
the revision that turned precompilation on. Before it, Blake3 exposed a
`blake3_rs_shared` cdylib that `ix_native_decide_dynlib` had to fetch and link;
that target no longer exists. -/
require Blake3 from git
 "https://github.com/argumentcomputer/Blake3.lean" @ "1b0fbd2bd78b2b873e14264037af8c8b1536b9e9"
 "https://github.com/argumentcomputer/Blake3.lean" @ "5ff5e70b6c7fc371cc6b454b83844f1f5b44ac96"

require Cli from git
 "https://github.com/leanprover/lean4-cli" @ "v4.33.0"
Expand DownExpand Up@@ -197,29 +199,20 @@ opaque `@[extern]` it reaches, both symbol layers must be loadable up front:
* the raw Rust symbol it forwards to, taken from that crate's `cdylib`, recorded
 by absolute path so no `LD_LIBRARY_PATH` is needed.

Covered externs: `Blake3.Rust` hashing (with the `Blake3` base module, which
holds the `HasherOps.hash` orchestration `Address.blake3` calls) against
`blake3_rs`, and `Ix.Unsigned.toLEBytes` against `ix-ffi-dyn`. -/
Covers Ix's own externs only -- currently `Ix.Unsigned.toLEBytes` against
`ix-ffi-dyn`. Blake3's are not here: that package precompiles its libraries, so
Lake loads their shared objects into the elaborating process by itself. -/
target ix_native_decide_dynlib pkg : Dynlib := do
 let some blake3Base ← findModule? `Blake3
 | error "module `Blake3` not found; is the Blake3 dependency available?"
 let some blake3Rust ← findModule? `Blake3.Rust
 | error "module `Blake3.Rust` not found; is the Blake3 dependency available?"
 let some ixUnsigned ← findModule? `Ix.Unsigned
 | error "module `Ix.Unsigned` not found"
 -- Raw symbols come from each crate's cdylib, recorded by path, and are built
 -- by fetching the owning package's target (no direct cargo calls here):
 -- Blake3 via its `blake3_rs_shared`, Ix via the minimal `ix_ffi_dyn`.
 let blake3Cdylib := (← blake3Rust.pkg.fetchTargetJob `blake3_rs_shared).map fun _ =>
 blake3Rust.pkg.dir / "rust" / "target" / "release" / nameToSharedLib "blake3_rs"
 -- Raw symbols come from the crate's cdylib, recorded by path, and are built
 -- by fetching the owning target (no direct cargo calls here).
 let ixCdylib ← ix_ffi_dyn.fetch
 -- Boxed entry points are Lean's own generated objects for the declaring modules.
 let mut boxedObjs := #[]
 for mod in #[blake3Base, blake3Rust, ixUnsigned] do
 boxedObjs := boxedObjs ++ (← (mod.nativeFacets true).mapM (·.fetch mod))
 -- Boxed entry points are Lean's own generated objects for the declaring module.
 let boxedObjs ← (ixUnsigned.nativeFacets true).mapM (·.fetch ixUnsigned)
 buildSharedLib "ix_native_decide"
 (pkg.buildDir / nameToSharedLib "ix_native_decide")
 (boxedObjs.push blake3Cdylib |>.push ixCdylib) #[]
 (boxedObjs.push ixCdylib) #[]

/- Formal verification of `Ix.Tc` against the lean4lean `Theory` spec.
Non-default: `lake build ix` never
Expand Down

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Highlight search terms from Google/DuckDuckGo/Bing referrer\n(function() {\n var ref = document.referrer;\n var terms = [];\n \n if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) {\n var url = new URL(ref);\n var q = url.searchParams.get('q') || url.searchParams.get('p');\n if (q) {\n terms = q.split(/\\s+/).filter(function(t) { return t.length > 2; });\n }\n }\n \n if (terms.length === 0) return;\n \n var style = document.createElement('style');\n style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';\n document.head.appendChild(style);\n \n function highlight(node) {\n if (node.nodeType === 3) { // text node\n var text = node.textContent;\n var found = false;\n terms.forEach(function(term) {\n var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\\]\\\\]/g, '\\\\') + ')', 'gi');\n if (regex.test(text)) {\n found = true;\n var frag = document.createDocumentFragment();\n var parts = text.split(regex);\n parts.forEach(function(part, i) {\n if (i % 2 === 0) {\n frag.appendChild(document.createTextNode(part));\n } else {\n var span = document.createElement('span');\n span.className = 'userscript-highlight';\n span.textContent = part;\n frag.appendChild(span);\n }\n });\n node.parentNode.replaceChild(frag, node);\n }\n });\n } else if (node.nodeType === 1 && node.childNodes) { // element\n var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];\n if (!skipTags.includes(node.tagName)) {\n Array.from(node.childNodes).forEach(highlight);\n }\n }\n }\n \n highlight(document.body);\n \n // Re-highlight on dynamic content\n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1 || node.nodeType === 3) highlight(node);\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Highlight Search Terms");
}
} catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
chore: Update Lean to v4.33.1#593

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Closed

argument-ci-bot
wants to merge
4
commits into

from

 Closed


chore: Update Lean to v4.33.1
#593
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


4 commits


Select commit
Hold shift + click to select a range
0ba9a4d

ci: Exclude CompileFC from lean-update


samuelburnham Aug 27, 2026
024bc51

lakefile: drop Blake3 from the native-decide dynlib


samuelburnham Aug 28, 2026
cdcc54b

ci: Glob Benchmarks and exclude CompileFC by name


samuelburnham Aug 28, 2026
a82579a

chore: Update lean4-nix to e014934


samuelburnham Aug 28, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


37 changes: 24 additions & 13 deletions
.github/workflows/update.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -24,20 +24,31 @@ jobs:
 client-id: ${{ secrets.TOKEN_APP_ID }}
 private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}

 # `dev` carries the fork's bump_mode/release_channel support; `main` only
 # mirrors upstream, which silently ignores these inputs. A PR is opened
 # on an update/lean-{release} branch whether or not the build passes, so
 # an incompatible release shows up as a failing PR to review. Dependencies
 # pinned to a Lean version tag move with the toolchain; a dependency
 # pinned to a commit hash is reported and left alone.
 - uses: argumentcomputer/lean-update@dev
 # `exclude-dir` carries the fork's bump_mode/release_channel support plus
 # the `!` exclusion syntax below; `main` only mirrors upstream, which
 # silently ignores these inputs. Move back to `dev` once the exclusion
 # lands there. A PR is opened on an update/lean-{release} branch whether
 # or not the build passes, so an incompatible release shows up as a
 # failing PR to review. Dependencies pinned to a Lean version tag move
 # with the toolchain; a dependency pinned to a commit hash is reported
 # and left alone.
 - uses: argumentcomputer/lean-update@exclude-dir
 with:
 # 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.
 lake_package_directory: ". Benchmarks/**"
 # The root package plus the benchmark packages. `/**` walks a whole
 # subtree, reaching packages nested inside another package (Catalog's
 # relocation fixtures, Compile's TruthMines) and skipping dotted
 # directories so `.lake` dependency checkouts are never swept up.
 #
 # `!` subtracts a directory and everything beneath it, so the glob can
 # cover Benchmarks while sparing CompileFC, which must stay pinned: it
 # builds against formal-conjectures at a commit hash, which the action
 # leaves alone, so moving its toolchain off v4.27.0 only breaks the
 # build. An exclusion takes no glob of its own, and one matching
 # nothing is reported in the log rather than passing silently.
 lake_package_directory: >-
 .
 Benchmarks/**
 !Benchmarks/CompileFC
 bump_mode: pinned-tags
 pr: true
 token: ${{ steps.app-token.outputs.token }}

6 changes: 3 additions & 3 deletions
flake.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


39 changes: 16 additions & 23 deletions
lakefile.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -7,13 +7,15 @@ package ix where
require LSpec from git
 "https://github.com/argumentcomputer/LSpec" @ "ab4d5eb461941837f48eb891be755c8c73e89fdd"

/- Blake3's `blake3_rs_shared` target builds `blake3-rs` as a `cdylib`
alongside the staticlib. `ix_native_decide_dynlib` fetches it to supply the
BLAKE3 backend to Lean's native evaluator, and that dynlib gates every
`IxTcVerify` module, so this pin must stay at or after the revision that
introduced the target. -/
/- Blake3 precompiles its libraries, so Lake loads their shared objects -- which
bundle the C and Rust FFI objects -- into any process elaborating a module that
imports them. That is what supplies the BLAKE3 backend to Lean's native evaluator
for the `native_decide` proofs in `IxTcVerify`, so this pin must stay at or after
the revision that turned precompilation on. Before it, Blake3 exposed a
`blake3_rs_shared` cdylib that `ix_native_decide_dynlib` had to fetch and link;
that target no longer exists. -/
require Blake3 from git
 "https://github.com/argumentcomputer/Blake3.lean" @ "1b0fbd2bd78b2b873e14264037af8c8b1536b9e9"
 "https://github.com/argumentcomputer/Blake3.lean" @ "5ff5e70b6c7fc371cc6b454b83844f1f5b44ac96"

require Cli from git
 "https://github.com/leanprover/lean4-cli" @ "v4.33.0"
Expand DownExpand Up@@ -197,29 +199,20 @@ opaque `@[extern]` it reaches, both symbol layers must be loadable up front:
* the raw Rust symbol it forwards to, taken from that crate's `cdylib`, recorded
 by absolute path so no `LD_LIBRARY_PATH` is needed.

Covered externs: `Blake3.Rust` hashing (with the `Blake3` base module, which
holds the `HasherOps.hash` orchestration `Address.blake3` calls) against
`blake3_rs`, and `Ix.Unsigned.toLEBytes` against `ix-ffi-dyn`. -/
Covers Ix's own externs only -- currently `Ix.Unsigned.toLEBytes` against
`ix-ffi-dyn`. Blake3's are not here: that package precompiles its libraries, so
Lake loads their shared objects into the elaborating process by itself. -/
target ix_native_decide_dynlib pkg : Dynlib := do
 let some blake3Base ← findModule? `Blake3
 | error "module `Blake3` not found; is the Blake3 dependency available?"
 let some blake3Rust ← findModule? `Blake3.Rust
 | error "module `Blake3.Rust` not found; is the Blake3 dependency available?"
 let some ixUnsigned ← findModule? `Ix.Unsigned
 | error "module `Ix.Unsigned` not found"
 -- Raw symbols come from each crate's cdylib, recorded by path, and are built
 -- by fetching the owning package's target (no direct cargo calls here):
 -- Blake3 via its `blake3_rs_shared`, Ix via the minimal `ix_ffi_dyn`.
 let blake3Cdylib := (← blake3Rust.pkg.fetchTargetJob `blake3_rs_shared).map fun _ =>
 blake3Rust.pkg.dir / "rust" / "target" / "release" / nameToSharedLib "blake3_rs"
 -- Raw symbols come from the crate's cdylib, recorded by path, and are built
 -- by fetching the owning target (no direct cargo calls here).
 let ixCdylib ← ix_ffi_dyn.fetch
 -- Boxed entry points are Lean's own generated objects for the declaring modules.
 let mut boxedObjs := #[]
 for mod in #[blake3Base, blake3Rust, ixUnsigned] do
 boxedObjs := boxedObjs ++ (← (mod.nativeFacets true).mapM (·.fetch mod))
 -- Boxed entry points are Lean's own generated objects for the declaring module.
 let boxedObjs ← (ixUnsigned.nativeFacets true).mapM (·.fetch ixUnsigned)
 buildSharedLib "ix_native_decide"
 (pkg.buildDir / nameToSharedLib "ix_native_decide")
 (boxedObjs.push blake3Cdylib |>.push ixCdylib) #[]
 (boxedObjs.push ixCdylib) #[]

/- Formal verification of `Ix.Tc` against the lean4lean `Theory` spec.
Non-default: `lake build ix` never
Expand Down

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Strip utm_, fbclid, gclid, etc. from all links on page\n(function() {\n var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content',\n 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid',\n 'ref', 'ref_src', 'source', 'medium', 'campaign'];\n \n function cleanUrl(url) {\n try {\n var u = new URL(url, window.location.origin);\n var changed = false;\n trackingParams.forEach(function(p) {\n if (u.searchParams.has(p)) {\n u.searchParams.delete(p);\n changed = true;\n }\n });\n return changed ? u.toString() : url;\n } catch (e) {\n return url;\n }\n }\n \n function cleanLinks() {\n document.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n \n cleanLinks();\n \n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1) {\n if (node.tagName === 'A') cleanLinks();\n node.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Remove Tracking Parameters from Links");
}
} catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); }
})();
(function(){
try {
var __m = "youtube.com";
var __re = new RegExp('^' + "youtube\\.com" + '

Skip to content
chore: Update Lean to v4.33.1#593

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Closed

argument-ci-bot
wants to merge
4
commits into

from

 Closed


chore: Update Lean to v4.33.1
#593
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


4 commits


Select commit
Hold shift + click to select a range
0ba9a4d

ci: Exclude CompileFC from lean-update


samuelburnham Aug 27, 2026
024bc51

lakefile: drop Blake3 from the native-decide dynlib


samuelburnham Aug 28, 2026
cdcc54b

ci: Glob Benchmarks and exclude CompileFC by name


samuelburnham Aug 28, 2026
a82579a

chore: Update lean4-nix to e014934


samuelburnham Aug 28, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


37 changes: 24 additions & 13 deletions
.github/workflows/update.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -24,20 +24,31 @@ jobs:
 client-id: ${{ secrets.TOKEN_APP_ID }}
 private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}

 # `dev` carries the fork's bump_mode/release_channel support; `main` only
 # mirrors upstream, which silently ignores these inputs. A PR is opened
 # on an update/lean-{release} branch whether or not the build passes, so
 # an incompatible release shows up as a failing PR to review. Dependencies
 # pinned to a Lean version tag move with the toolchain; a dependency
 # pinned to a commit hash is reported and left alone.
 - uses: argumentcomputer/lean-update@dev
 # `exclude-dir` carries the fork's bump_mode/release_channel support plus
 # the `!` exclusion syntax below; `main` only mirrors upstream, which
 # silently ignores these inputs. Move back to `dev` once the exclusion
 # lands there. A PR is opened on an update/lean-{release} branch whether
 # or not the build passes, so an incompatible release shows up as a
 # failing PR to review. Dependencies pinned to a Lean version tag move
 # with the toolchain; a dependency pinned to a commit hash is reported
 # and left alone.
 - uses: argumentcomputer/lean-update@exclude-dir
 with:
 # 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.
 lake_package_directory: ". Benchmarks/**"
 # The root package plus the benchmark packages. `/**` walks a whole
 # subtree, reaching packages nested inside another package (Catalog's
 # relocation fixtures, Compile's TruthMines) and skipping dotted
 # directories so `.lake` dependency checkouts are never swept up.
 #
 # `!` subtracts a directory and everything beneath it, so the glob can
 # cover Benchmarks while sparing CompileFC, which must stay pinned: it
 # builds against formal-conjectures at a commit hash, which the action
 # leaves alone, so moving its toolchain off v4.27.0 only breaks the
 # build. An exclusion takes no glob of its own, and one matching
 # nothing is reported in the log rather than passing silently.
 lake_package_directory: >-
 .
 Benchmarks/**
 !Benchmarks/CompileFC
 bump_mode: pinned-tags
 pr: true
 token: ${{ steps.app-token.outputs.token }}

6 changes: 3 additions & 3 deletions
flake.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


39 changes: 16 additions & 23 deletions
lakefile.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -7,13 +7,15 @@ package ix where
require LSpec from git
 "https://github.com/argumentcomputer/LSpec" @ "ab4d5eb461941837f48eb891be755c8c73e89fdd"

/- Blake3's `blake3_rs_shared` target builds `blake3-rs` as a `cdylib`
alongside the staticlib. `ix_native_decide_dynlib` fetches it to supply the
BLAKE3 backend to Lean's native evaluator, and that dynlib gates every
`IxTcVerify` module, so this pin must stay at or after the revision that
introduced the target. -/
/- Blake3 precompiles its libraries, so Lake loads their shared objects -- which
bundle the C and Rust FFI objects -- into any process elaborating a module that
imports them. That is what supplies the BLAKE3 backend to Lean's native evaluator
for the `native_decide` proofs in `IxTcVerify`, so this pin must stay at or after
the revision that turned precompilation on. Before it, Blake3 exposed a
`blake3_rs_shared` cdylib that `ix_native_decide_dynlib` had to fetch and link;
that target no longer exists. -/
require Blake3 from git
 "https://github.com/argumentcomputer/Blake3.lean" @ "1b0fbd2bd78b2b873e14264037af8c8b1536b9e9"
 "https://github.com/argumentcomputer/Blake3.lean" @ "5ff5e70b6c7fc371cc6b454b83844f1f5b44ac96"

require Cli from git
 "https://github.com/leanprover/lean4-cli" @ "v4.33.0"
Expand DownExpand Up@@ -197,29 +199,20 @@ opaque `@[extern]` it reaches, both symbol layers must be loadable up front:
* the raw Rust symbol it forwards to, taken from that crate's `cdylib`, recorded
 by absolute path so no `LD_LIBRARY_PATH` is needed.

Covered externs: `Blake3.Rust` hashing (with the `Blake3` base module, which
holds the `HasherOps.hash` orchestration `Address.blake3` calls) against
`blake3_rs`, and `Ix.Unsigned.toLEBytes` against `ix-ffi-dyn`. -/
Covers Ix's own externs only -- currently `Ix.Unsigned.toLEBytes` against
`ix-ffi-dyn`. Blake3's are not here: that package precompiles its libraries, so
Lake loads their shared objects into the elaborating process by itself. -/
target ix_native_decide_dynlib pkg : Dynlib := do
 let some blake3Base ← findModule? `Blake3
 | error "module `Blake3` not found; is the Blake3 dependency available?"
 let some blake3Rust ← findModule? `Blake3.Rust
 | error "module `Blake3.Rust` not found; is the Blake3 dependency available?"
 let some ixUnsigned ← findModule? `Ix.Unsigned
 | error "module `Ix.Unsigned` not found"
 -- Raw symbols come from each crate's cdylib, recorded by path, and are built
 -- by fetching the owning package's target (no direct cargo calls here):
 -- Blake3 via its `blake3_rs_shared`, Ix via the minimal `ix_ffi_dyn`.
 let blake3Cdylib := (← blake3Rust.pkg.fetchTargetJob `blake3_rs_shared).map fun _ =>
 blake3Rust.pkg.dir / "rust" / "target" / "release" / nameToSharedLib "blake3_rs"
 -- Raw symbols come from the crate's cdylib, recorded by path, and are built
 -- by fetching the owning target (no direct cargo calls here).
 let ixCdylib ← ix_ffi_dyn.fetch
 -- Boxed entry points are Lean's own generated objects for the declaring modules.
 let mut boxedObjs := #[]
 for mod in #[blake3Base, blake3Rust, ixUnsigned] do
 boxedObjs := boxedObjs ++ (← (mod.nativeFacets true).mapM (·.fetch mod))
 -- Boxed entry points are Lean's own generated objects for the declaring module.
 let boxedObjs ← (ixUnsigned.nativeFacets true).mapM (·.fetch ixUnsigned)
 buildSharedLib "ix_native_decide"
 (pkg.buildDir / nameToSharedLib "ix_native_decide")
 (boxedObjs.push blake3Cdylib |>.push ixCdylib) #[]
 (boxedObjs.push ixCdylib) #[]

/- Formal verification of `Ix.Tc` against the lean4lean `Theory` spec.
Non-default: `lake build ix` never
Expand Down

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Auto-enable theater mode on YouTube\n(function() {\n function tryTheater() {\n var btn = document.querySelector('button[aria-label=\"Theater mode\"], ytd-player #player button[title=\"Theater mode\"]');\n if (btn && !btn.classList.contains('activated')) {\n btn.click();\n }\n }\n \n // Try immediately\n tryTheater();\n \n // Try after navigation (SPA)\n var lastUrl = location.href;\n setInterval(function() {\n if (location.href !== lastUrl) {\n lastUrl = location.href;\n setTimeout(tryTheater, 500);\n }\n }, 1000);\n \n // Also try on player load\n var observer = new MutationObserver(tryTheater);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "YouTube Theater Mode Default");
}
} catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
chore: Update Lean to v4.33.1#593

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Closed

argument-ci-bot
wants to merge
4
commits into

from

 Closed


chore: Update Lean to v4.33.1
#593
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


4 commits


Select commit
Hold shift + click to select a range
0ba9a4d

ci: Exclude CompileFC from lean-update


samuelburnham Aug 27, 2026
024bc51

lakefile: drop Blake3 from the native-decide dynlib


samuelburnham Aug 28, 2026
cdcc54b

ci: Glob Benchmarks and exclude CompileFC by name


samuelburnham Aug 28, 2026
a82579a

chore: Update lean4-nix to e014934


samuelburnham Aug 28, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


37 changes: 24 additions & 13 deletions
.github/workflows/update.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -24,20 +24,31 @@ jobs:
 client-id: ${{ secrets.TOKEN_APP_ID }}
 private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}

 # `dev` carries the fork's bump_mode/release_channel support; `main` only
 # mirrors upstream, which silently ignores these inputs. A PR is opened
 # on an update/lean-{release} branch whether or not the build passes, so
 # an incompatible release shows up as a failing PR to review. Dependencies
 # pinned to a Lean version tag move with the toolchain; a dependency
 # pinned to a commit hash is reported and left alone.
 - uses: argumentcomputer/lean-update@dev
 # `exclude-dir` carries the fork's bump_mode/release_channel support plus
 # the `!` exclusion syntax below; `main` only mirrors upstream, which
 # silently ignores these inputs. Move back to `dev` once the exclusion
 # lands there. A PR is opened on an update/lean-{release} branch whether
 # or not the build passes, so an incompatible release shows up as a
 # failing PR to review. Dependencies pinned to a Lean version tag move
 # with the toolchain; a dependency pinned to a commit hash is reported
 # and left alone.
 - uses: argumentcomputer/lean-update@exclude-dir
 with:
 # 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.
 lake_package_directory: ". Benchmarks/**"
 # The root package plus the benchmark packages. `/**` walks a whole
 # subtree, reaching packages nested inside another package (Catalog's
 # relocation fixtures, Compile's TruthMines) and skipping dotted
 # directories so `.lake` dependency checkouts are never swept up.
 #
 # `!` subtracts a directory and everything beneath it, so the glob can
 # cover Benchmarks while sparing CompileFC, which must stay pinned: it
 # builds against formal-conjectures at a commit hash, which the action
 # leaves alone, so moving its toolchain off v4.27.0 only breaks the
 # build. An exclusion takes no glob of its own, and one matching
 # nothing is reported in the log rather than passing silently.
 lake_package_directory: >-
 .
 Benchmarks/**
 !Benchmarks/CompileFC
 bump_mode: pinned-tags
 pr: true
 token: ${{ steps.app-token.outputs.token }}

6 changes: 3 additions & 3 deletions
flake.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


39 changes: 16 additions & 23 deletions
lakefile.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -7,13 +7,15 @@ package ix where
require LSpec from git
 "https://github.com/argumentcomputer/LSpec" @ "ab4d5eb461941837f48eb891be755c8c73e89fdd"

/- Blake3's `blake3_rs_shared` target builds `blake3-rs` as a `cdylib`
alongside the staticlib. `ix_native_decide_dynlib` fetches it to supply the
BLAKE3 backend to Lean's native evaluator, and that dynlib gates every
`IxTcVerify` module, so this pin must stay at or after the revision that
introduced the target. -/
/- Blake3 precompiles its libraries, so Lake loads their shared objects -- which
bundle the C and Rust FFI objects -- into any process elaborating a module that
imports them. That is what supplies the BLAKE3 backend to Lean's native evaluator
for the `native_decide` proofs in `IxTcVerify`, so this pin must stay at or after
the revision that turned precompilation on. Before it, Blake3 exposed a
`blake3_rs_shared` cdylib that `ix_native_decide_dynlib` had to fetch and link;
that target no longer exists. -/
require Blake3 from git
 "https://github.com/argumentcomputer/Blake3.lean" @ "1b0fbd2bd78b2b873e14264037af8c8b1536b9e9"
 "https://github.com/argumentcomputer/Blake3.lean" @ "5ff5e70b6c7fc371cc6b454b83844f1f5b44ac96"

require Cli from git
 "https://github.com/leanprover/lean4-cli" @ "v4.33.0"
Expand DownExpand Up@@ -197,29 +199,20 @@ opaque `@[extern]` it reaches, both symbol layers must be loadable up front:
* the raw Rust symbol it forwards to, taken from that crate's `cdylib`, recorded
 by absolute path so no `LD_LIBRARY_PATH` is needed.

Covered externs: `Blake3.Rust` hashing (with the `Blake3` base module, which
holds the `HasherOps.hash` orchestration `Address.blake3` calls) against
`blake3_rs`, and `Ix.Unsigned.toLEBytes` against `ix-ffi-dyn`. -/
Covers Ix's own externs only -- currently `Ix.Unsigned.toLEBytes` against
`ix-ffi-dyn`. Blake3's are not here: that package precompiles its libraries, so
Lake loads their shared objects into the elaborating process by itself. -/
target ix_native_decide_dynlib pkg : Dynlib := do
 let some blake3Base ← findModule? `Blake3
 | error "module `Blake3` not found; is the Blake3 dependency available?"
 let some blake3Rust ← findModule? `Blake3.Rust
 | error "module `Blake3.Rust` not found; is the Blake3 dependency available?"
 let some ixUnsigned ← findModule? `Ix.Unsigned
 | error "module `Ix.Unsigned` not found"
 -- Raw symbols come from each crate's cdylib, recorded by path, and are built
 -- by fetching the owning package's target (no direct cargo calls here):
 -- Blake3 via its `blake3_rs_shared`, Ix via the minimal `ix_ffi_dyn`.
 let blake3Cdylib := (← blake3Rust.pkg.fetchTargetJob `blake3_rs_shared).map fun _ =>
 blake3Rust.pkg.dir / "rust" / "target" / "release" / nameToSharedLib "blake3_rs"
 -- Raw symbols come from the crate's cdylib, recorded by path, and are built
 -- by fetching the owning target (no direct cargo calls here).
 let ixCdylib ← ix_ffi_dyn.fetch
 -- Boxed entry points are Lean's own generated objects for the declaring modules.
 let mut boxedObjs := #[]
 for mod in #[blake3Base, blake3Rust, ixUnsigned] do
 boxedObjs := boxedObjs ++ (← (mod.nativeFacets true).mapM (·.fetch mod))
 -- Boxed entry points are Lean's own generated objects for the declaring module.
 let boxedObjs ← (ixUnsigned.nativeFacets true).mapM (·.fetch ixUnsigned)
 buildSharedLib "ix_native_decide"
 (pkg.buildDir / nameToSharedLib "ix_native_decide")
 (boxedObjs.push blake3Cdylib |>.push ixCdylib) #[]
 (boxedObjs.push ixCdylib) #[]

/- Formal verification of `Ix.Tc` against the lean4lean `Theory` spec.
Non-default: `lake build ix` never
Expand Down

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Remove or un-stick sticky/fixed headers that block content\n(function() {\n function unstick() {\n document.querySelectorAll('header, nav, [role=\"banner\"], .header, .navbar, .sticky, .fixed-top, [style*=\"position: fixed\"], [style*=\"position:sticky\"]').forEach(function(el) {\n if (el.style.position === 'fixed' || el.style.position === 'sticky' || \n getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') {\n el.style.position = 'static';\n el.style.top = 'auto';\n el.style.zIndex = 'auto';\n }\n });\n }\n \n unstick();\n \n var observer = new MutationObserver(unstick);\n observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] });\n})();", "Kill Sticky Headers");
}
} catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
chore: Update Lean to v4.33.1#593

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Closed

argument-ci-bot
wants to merge
4
commits into

from

 Closed


chore: Update Lean to v4.33.1
#593
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


4 commits


Select commit
Hold shift + click to select a range
0ba9a4d

ci: Exclude CompileFC from lean-update


samuelburnham Aug 27, 2026
024bc51

lakefile: drop Blake3 from the native-decide dynlib


samuelburnham Aug 28, 2026
cdcc54b

ci: Glob Benchmarks and exclude CompileFC by name


samuelburnham Aug 28, 2026
a82579a

chore: Update lean4-nix to e014934


samuelburnham Aug 28, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


37 changes: 24 additions & 13 deletions
.github/workflows/update.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -24,20 +24,31 @@ jobs:
 client-id: ${{ secrets.TOKEN_APP_ID }}
 private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}

 # `dev` carries the fork's bump_mode/release_channel support; `main` only
 # mirrors upstream, which silently ignores these inputs. A PR is opened
 # on an update/lean-{release} branch whether or not the build passes, so
 # an incompatible release shows up as a failing PR to review. Dependencies
 # pinned to a Lean version tag move with the toolchain; a dependency
 # pinned to a commit hash is reported and left alone.
 - uses: argumentcomputer/lean-update@dev
 # `exclude-dir` carries the fork's bump_mode/release_channel support plus
 # the `!` exclusion syntax below; `main` only mirrors upstream, which
 # silently ignores these inputs. Move back to `dev` once the exclusion
 # lands there. A PR is opened on an update/lean-{release} branch whether
 # or not the build passes, so an incompatible release shows up as a
 # failing PR to review. Dependencies pinned to a Lean version tag move
 # with the toolchain; a dependency pinned to a commit hash is reported
 # and left alone.
 - uses: argumentcomputer/lean-update@exclude-dir
 with:
 # 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.
 lake_package_directory: ". Benchmarks/**"
 # The root package plus the benchmark packages. `/**` walks a whole
 # subtree, reaching packages nested inside another package (Catalog's
 # relocation fixtures, Compile's TruthMines) and skipping dotted
 # directories so `.lake` dependency checkouts are never swept up.
 #
 # `!` subtracts a directory and everything beneath it, so the glob can
 # cover Benchmarks while sparing CompileFC, which must stay pinned: it
 # builds against formal-conjectures at a commit hash, which the action
 # leaves alone, so moving its toolchain off v4.27.0 only breaks the
 # build. An exclusion takes no glob of its own, and one matching
 # nothing is reported in the log rather than passing silently.
 lake_package_directory: >-
 .
 Benchmarks/**
 !Benchmarks/CompileFC
 bump_mode: pinned-tags
 pr: true
 token: ${{ steps.app-token.outputs.token }}

6 changes: 3 additions & 3 deletions
flake.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


39 changes: 16 additions & 23 deletions
lakefile.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -7,13 +7,15 @@ package ix where
require LSpec from git
 "https://github.com/argumentcomputer/LSpec" @ "ab4d5eb461941837f48eb891be755c8c73e89fdd"

/- Blake3's `blake3_rs_shared` target builds `blake3-rs` as a `cdylib`
alongside the staticlib. `ix_native_decide_dynlib` fetches it to supply the
BLAKE3 backend to Lean's native evaluator, and that dynlib gates every
`IxTcVerify` module, so this pin must stay at or after the revision that
introduced the target. -/
/- Blake3 precompiles its libraries, so Lake loads their shared objects -- which
bundle the C and Rust FFI objects -- into any process elaborating a module that
imports them. That is what supplies the BLAKE3 backend to Lean's native evaluator
for the `native_decide` proofs in `IxTcVerify`, so this pin must stay at or after
the revision that turned precompilation on. Before it, Blake3 exposed a
`blake3_rs_shared` cdylib that `ix_native_decide_dynlib` had to fetch and link;
that target no longer exists. -/
require Blake3 from git
 "https://github.com/argumentcomputer/Blake3.lean" @ "1b0fbd2bd78b2b873e14264037af8c8b1536b9e9"
 "https://github.com/argumentcomputer/Blake3.lean" @ "5ff5e70b6c7fc371cc6b454b83844f1f5b44ac96"

require Cli from git
 "https://github.com/leanprover/lean4-cli" @ "v4.33.0"
Expand DownExpand Up@@ -197,29 +199,20 @@ opaque `@[extern]` it reaches, both symbol layers must be loadable up front:
* the raw Rust symbol it forwards to, taken from that crate's `cdylib`, recorded
 by absolute path so no `LD_LIBRARY_PATH` is needed.

Covered externs: `Blake3.Rust` hashing (with the `Blake3` base module, which
holds the `HasherOps.hash` orchestration `Address.blake3` calls) against
`blake3_rs`, and `Ix.Unsigned.toLEBytes` against `ix-ffi-dyn`. -/
Covers Ix's own externs only -- currently `Ix.Unsigned.toLEBytes` against
`ix-ffi-dyn`. Blake3's are not here: that package precompiles its libraries, so
Lake loads their shared objects into the elaborating process by itself. -/
target ix_native_decide_dynlib pkg : Dynlib := do
 let some blake3Base ← findModule? `Blake3
 | error "module `Blake3` not found; is the Blake3 dependency available?"
 let some blake3Rust ← findModule? `Blake3.Rust
 | error "module `Blake3.Rust` not found; is the Blake3 dependency available?"
 let some ixUnsigned ← findModule? `Ix.Unsigned
 | error "module `Ix.Unsigned` not found"
 -- Raw symbols come from each crate's cdylib, recorded by path, and are built
 -- by fetching the owning package's target (no direct cargo calls here):
 -- Blake3 via its `blake3_rs_shared`, Ix via the minimal `ix_ffi_dyn`.
 let blake3Cdylib := (← blake3Rust.pkg.fetchTargetJob `blake3_rs_shared).map fun _ =>
 blake3Rust.pkg.dir / "rust" / "target" / "release" / nameToSharedLib "blake3_rs"
 -- Raw symbols come from the crate's cdylib, recorded by path, and are built
 -- by fetching the owning target (no direct cargo calls here).
 let ixCdylib ← ix_ffi_dyn.fetch
 -- Boxed entry points are Lean's own generated objects for the declaring modules.
 let mut boxedObjs := #[]
 for mod in #[blake3Base, blake3Rust, ixUnsigned] do
 boxedObjs := boxedObjs ++ (← (mod.nativeFacets true).mapM (·.fetch mod))
 -- Boxed entry points are Lean's own generated objects for the declaring module.
 let boxedObjs ← (ixUnsigned.nativeFacets true).mapM (·.fetch ixUnsigned)
 buildSharedLib "ix_native_decide"
 (pkg.buildDir / nameToSharedLib "ix_native_decide")
 (boxedObjs.push blake3Cdylib |>.push ixCdylib) #[]
 (boxedObjs.push ixCdylib) #[]

/- Formal verification of `Ix.Tc` against the lean4lean `Theory` spec.
Non-default: `lake build ix` never
Expand Down

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Universal Dark Mode - works on any site\n(function() {\n var enabled = true;\n \n function applyDarkMode() {\n if (!enabled) return;\n \n // Create style element if it doesn't exist\n var style = document.getElementById('universal-dark-mode-style');\n if (!style) {\n style = document.createElement('style');\n style.id = 'universal-dark-mode-style';\n document.head.appendChild(style);\n }\n \n // Dark mode CSS - inverts colors but preserves images/video\n style.textContent = '\n /* Invert everything except media */\n html {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #1a1a2e !important;\n }\n \n /* Restore images, videos, iframes, canvas */\n img, video, iframe, canvas, svg, picture, [style*=\"background-image\"] {\n filter: invert(1) hue-rotate(180deg) !important;\n }\n \n /* Preserve specific elements that should not be inverted */\n .no-dark-mode, .no-dark-mode *,\n [data-theme=\"light\"], [data-theme=\"light\"],\n .ace_editor, .ace_editor *,\n .CodeMirror, .CodeMirror *,\n .monaco-editor, .monaco-editor *,\n .markdown-body pre, .markdown-body pre *,\n .highlight, .highlight *,\n pre code, pre code * {\n filter: none !important;\n }\n \n /* Fix common UI elements */\n .modal, .popup, .dropdown-menu, .tooltip, .popover {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #2d2d44 !important;\n border-color: #444 !important;\n }\n \n /* Scrollbars */\n ::-webkit-scrollbar { background: #1a1a2e !important; }\n ::-webkit-scrollbar-thumb { background: #444 !important; }\n ::-webkit-scrollbar-thumb:hover { background: #555 !important; }\n \n /* Selection */\n ::selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ';\n }\n \n function removeDarkMode() {\n var style = document.getElementById('universal-dark-mode-style');\n if (style) style.remove();\n }\n \n // Toggle with Alt+Shift+D\n document.addEventListener('keydown', function(e) {\n if (e.altKey && e.shiftKey && e.key === 'D') {\n e.preventDefault();\n enabled = !enabled;\n if (enabled) {\n applyDarkMode();\n console.log('[Universal Dark Mode] Enabled');\n } else {\n removeDarkMode();\n console.log('[Universal Dark Mode] Disabled');\n }\n }\n });\n \n // Apply on load\n applyDarkMode();\n \n // Re-apply on dynamic content\n var observer = new MutationObserver(function(mutations) {\n if (enabled && !document.getElementById('universal-dark-mode-style')) {\n applyDarkMode();\n }\n });\n observer.observe(document.head, { childList: true });\n \n console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle');\n})();", "Universal Dark Mode");
}
} catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); }
})();
})();

Skip to content
chore: Update Lean to v4.33.1#593

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Closed

argument-ci-bot
wants to merge
4
commits into

from

 Closed


chore: Update Lean to v4.33.1
#593
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


4 commits


Select commit
Hold shift + click to select a range
0ba9a4d

ci: Exclude CompileFC from lean-update


samuelburnham Aug 27, 2026
024bc51

lakefile: drop Blake3 from the native-decide dynlib


samuelburnham Aug 28, 2026
cdcc54b

ci: Glob Benchmarks and exclude CompileFC by name


samuelburnham Aug 28, 2026
a82579a

chore: Update lean4-nix to e014934


samuelburnham Aug 28, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


37 changes: 24 additions & 13 deletions
.github/workflows/update.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -24,20 +24,31 @@ jobs:
 client-id: ${{ secrets.TOKEN_APP_ID }}
 private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}

 # `dev` carries the fork's bump_mode/release_channel support; `main` only
 # mirrors upstream, which silently ignores these inputs. A PR is opened
 # on an update/lean-{release} branch whether or not the build passes, so
 # an incompatible release shows up as a failing PR to review. Dependencies
 # pinned to a Lean version tag move with the toolchain; a dependency
 # pinned to a commit hash is reported and left alone.
 - uses: argumentcomputer/lean-update@dev
 # `exclude-dir` carries the fork's bump_mode/release_channel support plus
 # the `!` exclusion syntax below; `main` only mirrors upstream, which
 # silently ignores these inputs. Move back to `dev` once the exclusion
 # lands there. A PR is opened on an update/lean-{release} branch whether
 # or not the build passes, so an incompatible release shows up as a
 # failing PR to review. Dependencies pinned to a Lean version tag move
 # with the toolchain; a dependency pinned to a commit hash is reported
 # and left alone.
 - uses: argumentcomputer/lean-update@exclude-dir
 with:
 # 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.
 lake_package_directory: ". Benchmarks/**"
 # The root package plus the benchmark packages. `/**` walks a whole
 # subtree, reaching packages nested inside another package (Catalog's
 # relocation fixtures, Compile's TruthMines) and skipping dotted
 # directories so `.lake` dependency checkouts are never swept up.
 #
 # `!` subtracts a directory and everything beneath it, so the glob can
 # cover Benchmarks while sparing CompileFC, which must stay pinned: it
 # builds against formal-conjectures at a commit hash, which the action
 # leaves alone, so moving its toolchain off v4.27.0 only breaks the
 # build. An exclusion takes no glob of its own, and one matching
 # nothing is reported in the log rather than passing silently.
 lake_package_directory: >-
 .
 Benchmarks/**
 !Benchmarks/CompileFC
 bump_mode: pinned-tags
 pr: true
 token: ${{ steps.app-token.outputs.token }}

6 changes: 3 additions & 3 deletions
flake.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


39 changes: 16 additions & 23 deletions
lakefile.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -7,13 +7,15 @@ package ix where
require LSpec from git
 "https://github.com/argumentcomputer/LSpec" @ "ab4d5eb461941837f48eb891be755c8c73e89fdd"

/- Blake3's `blake3_rs_shared` target builds `blake3-rs` as a `cdylib`
alongside the staticlib. `ix_native_decide_dynlib` fetches it to supply the
BLAKE3 backend to Lean's native evaluator, and that dynlib gates every
`IxTcVerify` module, so this pin must stay at or after the revision that
introduced the target. -/
/- Blake3 precompiles its libraries, so Lake loads their shared objects -- which
bundle the C and Rust FFI objects -- into any process elaborating a module that
imports them. That is what supplies the BLAKE3 backend to Lean's native evaluator
for the `native_decide` proofs in `IxTcVerify`, so this pin must stay at or after
the revision that turned precompilation on. Before it, Blake3 exposed a
`blake3_rs_shared` cdylib that `ix_native_decide_dynlib` had to fetch and link;
that target no longer exists. -/
require Blake3 from git
 "https://github.com/argumentcomputer/Blake3.lean" @ "1b0fbd2bd78b2b873e14264037af8c8b1536b9e9"
 "https://github.com/argumentcomputer/Blake3.lean" @ "5ff5e70b6c7fc371cc6b454b83844f1f5b44ac96"

require Cli from git
 "https://github.com/leanprover/lean4-cli" @ "v4.33.0"
Expand DownExpand Up@@ -197,29 +199,20 @@ opaque `@[extern]` it reaches, both symbol layers must be loadable up front:
* the raw Rust symbol it forwards to, taken from that crate's `cdylib`, recorded
 by absolute path so no `LD_LIBRARY_PATH` is needed.

Covered externs: `Blake3.Rust` hashing (with the `Blake3` base module, which
holds the `HasherOps.hash` orchestration `Address.blake3` calls) against
`blake3_rs`, and `Ix.Unsigned.toLEBytes` against `ix-ffi-dyn`. -/
Covers Ix's own externs only -- currently `Ix.Unsigned.toLEBytes` against
`ix-ffi-dyn`. Blake3's are not here: that package precompiles its libraries, so
Lake loads their shared objects into the elaborating process by itself. -/
target ix_native_decide_dynlib pkg : Dynlib := do
 let some blake3Base ← findModule? `Blake3
 | error "module `Blake3` not found; is the Blake3 dependency available?"
 let some blake3Rust ← findModule? `Blake3.Rust
 | error "module `Blake3.Rust` not found; is the Blake3 dependency available?"
 let some ixUnsigned ← findModule? `Ix.Unsigned
 | error "module `Ix.Unsigned` not found"
 -- Raw symbols come from each crate's cdylib, recorded by path, and are built
 -- by fetching the owning package's target (no direct cargo calls here):
 -- Blake3 via its `blake3_rs_shared`, Ix via the minimal `ix_ffi_dyn`.
 let blake3Cdylib := (← blake3Rust.pkg.fetchTargetJob `blake3_rs_shared).map fun _ =>
 blake3Rust.pkg.dir / "rust" / "target" / "release" / nameToSharedLib "blake3_rs"
 -- Raw symbols come from the crate's cdylib, recorded by path, and are built
 -- by fetching the owning target (no direct cargo calls here).
 let ixCdylib ← ix_ffi_dyn.fetch
 -- Boxed entry points are Lean's own generated objects for the declaring modules.
 let mut boxedObjs := #[]
 for mod in #[blake3Base, blake3Rust, ixUnsigned] do
 boxedObjs := boxedObjs ++ (← (mod.nativeFacets true).mapM (·.fetch mod))
 -- Boxed entry points are Lean's own generated objects for the declaring module.
 let boxedObjs ← (ixUnsigned.nativeFacets true).mapM (·.fetch ixUnsigned)
 buildSharedLib "ix_native_decide"
 (pkg.buildDir / nameToSharedLib "ix_native_decide")
 (boxedObjs.push blake3Cdylib |>.push ixCdylib) #[]
 (boxedObjs.push ixCdylib) #[]

/- Formal verification of `Ix.Tc` against the lean4lean `Theory` spec.
Non-default: `lake build ix` never
Expand Down