-
Notifications
You must be signed in to change notification settings - Fork 232
Open
Description
When setting up the environment for Lean 4.9.0 (as required by DeepSeek-Prover-V2), I encountered errors during the lake build step in the mathlib4 @ 2f65ba7 repository. The issue arose due to unspecified or outdated dependency versions in mathlib4/lakefile.lean, which is cloned recursively in the first step.
After troubleshooting, I identified the correct dependency versions that resolve the build errors. Below are the necessary changes to mathlib4/lakefile.lean:
Original Configuration:
/-!
## Mathlib dependencies on upstream projects.
-/
meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
require batteries from git "https://github.com/leanprover-community/batteries" @ "main"
require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.36"
require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
require importGraph from git "https://github.com/leanprover-community/import-graph.git" @ "main"
require REPL from git "https://github.com/xinhjBrant/repl.git" @ "deepseek"
Updated Configuration (Working):
/-!
## Mathlib dependencies on upstream projects.
-/
meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "bump_to_v4.9.0"
require batteries from git "https://github.com/leanprover-community/batteries" @ "bump/v4.9.0"
require Qq from git "https://github.com/leanprover-community/quote4" @ "bump/v4.9.0"
require aesop from git "https://github.com/leanprover-community/aesop" @ "8a2b60ac1d3e5b6295abc5ca07b9473594c3bcb1"
require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.36"
require Cli from git "https://github.com/leanprover/lean4-cli" @ "039d23aebf2ccb980bc86e93179e7e340f99b4f0"
require importGraph from git "https://github.com/leanprover-community/import-graph.git" @ "bump_to_v4.9.0"
require REPL from git "https://github.com/xinhjBrant/repl.git" @ "deepseek"
Verification:
This configuration was tested successfully on Linux using Lean-4.9.0 (following the DeepSeek-Prover-V1.5/V2 papers). I hope this issue helps others interested in DeepSeek-Prover series work.
KyrieXiao25
Metadata
Metadata
Assignees
Labels
No labels