Skip to content

fixing errors in lake build --- correct dependency version in mathlib4/lakefile.lean #21

@zhangjf-nlp

Description

@zhangjf-nlp

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions