[GH-ISSUE #21] fixing errors in lake build --- correct dependency version in mathlib4/lakefile.lean #13

New issue

Open

opened 2026-10-26 21:06:36 +00:00 by bsakaguchi · 0 comments

bsakaguchi commented

2026-10-26 21:06:36 +00:00

Owner

Originally created by @zhangjf-nlp on GitHub (May 6, 2025).
Original GitHub issue: https://github.com/deepseek-ai/DeepSeek-Prover-V1.5/issues/21

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.

Originally created by @zhangjf-nlp on GitHub (May 6, 2025). Original GitHub issue: https://github.com/deepseek-ai/DeepSeek-Prover-V1.5/issues/21 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](https://github.com/xinhjBrant/mathlib4/tree/2f65ba7f1a9144b20c8e7358513548e317d26de1) 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](https://github.com/leanprover/lean4/releases/download/v4.9.1/lean-4.9.0-linux.tar.zst) (following the DeepSeek-Prover-V1.5/V2 papers). I hope this issue helps others interested in DeepSeek-Prover series work.

No labels

pull-request

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference

deepseek-ai/DeepSeek-Prover-V1.5#13

No description provided.

Rows
Columns