Remove Mathlib dependency to shrink the compiled binary - #44
Merged
Conversation
Linking the `yul-semantics` executable currently compiles + links native object code for every transitively imported Mathlib module (~8500 C files), which dominates both CI time and binary size. The library's actual footprint in Mathlib is tiny, so we remove the dependency: 1. YulSemantics/Adequacy.lean — drop `import Mathlib.Data.Nat.Basic`; nothing from it is used (omega/simp are core). 2. YulSemantics/Dialect/EVM.lean — drop `import Mathlib.Tactic.SplitIfs`; replace the single `split_ifs at h1 h2` with core `split at ...`. 3. YulSemantics/Equiv.lean — drop `import Mathlib.Data.List.Forall2`; define a local `Forall₂` inductive with the `imp` lemma (the only Mathlib API used). 4. YulSemantics/FibExample.lean — drop `import Mathlib.Data.Nat.Fib.Basic`; define a local `fib` with a `fib_add_two` defining equation and state the theorems against it. 5. lakefile.toml — replace `require mathlib` with a direct `require batteries` (small, pure-Lean), kept only for the `batteries/runLinter` lint driver and the `nolint` attribute used in YulSemantics/Dialect.lean. Regenerate lake-manifest.json. 6. .github/workflows/lean_action_ci.yml — set use-mathlib-cache to false. Each step keeps `lake build` green; verified locally before push. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Implements the plan from the previous commit: * Adequacy.lean: drop the unused `Mathlib.Data.Nat.Basic` import; spell the two `le_rfl` uses as core `Nat.le_refl`. * Dialect/EVM.lean: drop `Mathlib.Tactic.SplitIfs`; replace the single `split_ifs at h1 h2` with core `repeat1' (first | split at h1 | split at h2)`. * Equiv.lean: drop `Mathlib.Data.List.Forall2`; add a local `Forall₂` inductive with the `imp` lemma (all the file used). * FibExample.lean: drop `Mathlib.Data.Nat.Fib.Basic`; add a local `fib` and `fib_add_two`, and state the theorems against them. * lakefile.toml: require batteries v4.31.0 directly (only for the `batteries/runLinter` lint driver and the `nolint` attribute used in Dialect.lean) instead of mathlib. The manifest shrinks from 9 packages to 1. * CI: no Mathlib cache step; Batteries builds from source in minutes. * README/DESIGN/docstrings updated accordingly. Verified: `lake build`, `lake lint`, and `lake build yul-semantics` all succeed from a clean checkout; the placeholder exe runs. The linked executable is 114M unstripped / 76M stripped, and no longer pulls any Mathlib object code. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
chris-ai1
changed the title
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
Linking the
yul-semanticsexecutable currently compiles + links native object code for every transitively imported Mathlib module (~8500 C files), which dominates both CI time and binary size. The library's actual footprint in Mathlib is tiny, so we remove the dependency:import Mathlib.Data.Nat.Basic; nothing from it is used (omega/simp are core).import Mathlib.Tactic.SplitIfs; replace the singlesplit_ifs at h1 h2with coresplit at ....import Mathlib.Data.List.Forall2; define a localForall₂inductive with theimplemma (the only Mathlib API used).import Mathlib.Data.Nat.Fib.Basic; define a localfibwith afib_add_twodefining equation and state the theorems against it.require mathlibwith a directrequire batteries(small, pure-Lean), kept only for thebatteries/runLinterlint driver and thenolintattribute used in YulSemantics/Dialect.lean. Regenerate lake-manifest.json.Each step keeps
lake buildgreen; verified locally before push.