Zulip Chat Archive
Stream: mathlib4
Topic: can't `lake update`
Alex Meiburg (Oct 22 2025 at 17:51):
I just ran lake update and it's complaining about some mathlib version mismatch:
info: mathlib: running post-update hooks
Dependency Mathlib uses a different lean-toolchain
Project uses leanprover/lean4:v4.25.0-rc2
Mathlib uses leanprover/lean4:v4.25.0-rc1
Alex Meiburg (Oct 22 2025 at 17:52):
How can I fix this ... ? I can't find anything much at all relevant on Zulip!
Yaël Dillies (Oct 22 2025 at 17:53):
Can you copy-paste your lakefile here?
Alex Meiburg (Oct 22 2025 at 17:53):
import Lake
open System Lake DSL
package «quantumInfo»
require "mathlib" from git
"https://github.com/leanprover-community/mathlib4.git"
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
@[default_target]
lean_lib QuantumInfo
Alex Meiburg (Oct 22 2025 at 17:56):
Is this somehow related to https://github.com/leanprover-community/mathlib4/pull/30785 and #mathlib4 > Build error in Tactic file ?
Bryan Gin-ge Chen (Oct 22 2025 at 18:02):
This might indeed be related; there were errors with v4.25.0-rc2 so I reverted us back to v4.25.0-rc1, but there are still errors there that we're still trying to figure out, unfortunately.
Yaël Dillies (Oct 22 2025 at 18:28):
The state of the art for having project docs is to not depend on doc-gen, but instead to use the leanprover-community/docgen-action. See ClassFieldTheory for an example.
Yaël Dillies (Oct 22 2025 at 18:29):
This will ensure that you don't get a toolchain mismatch when mathlib's toolchain is bumped but not doc-gen's, or vice-versa
Alex Meiburg (Oct 22 2025 at 18:43):
Hmm. I tried to address it locally by changing it to
require "mathlib" from git
"https://github.com/leanprover-community/mathlib4.git" @ "d9d1cc1012eccfc8d01215b1b7943b0e7f8b7757"
which is the v4.25.0-rc2 tag. But when I lake build QuantumInfo:docs, I started getting panics and stack traces!
ℹ [13768/18155] Built Mathlib.Algebra.Order.CompleteField:docs
info: stdout:
WARNING: Failed to obtain information for: ConditionallyCompleteLinearOrderedField: goal ?[anonymous]
info: stderr:
PANIC at DocGen4.Process.Info.ofTypedName DocGen4.Process.NameInfo:74:12: RatCast.ratCast is a declaration without position
backtrace:
0 doc-gen4 0x0000000107b1a41c _ZN4leanL15lean_panic_implEPKcmb + 268
1 doc-gen4 0x0000000107b1a900 lean_panic_fn + 40
2 doc-gen4 0x00000001004480d0 l_panic___at___DocGen4_Process_Info_ofTypedName_spec__3 + 56
3 doc-gen4 0x000000010045e9bc l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___DocGen4_Process_getFieldTypes_spec__1 + 612
4 doc-gen4 0x000000010045f2a0 l_DocGen4_Process_getFieldTypes___lam__0 + 532
5 doc-gen4 0x000000010045f680 l_DocGen4_Process_getFieldTypes___lam__0___boxed + 28
6 doc-gen4 0x0000000107b2f830 lean_apply_7 + 1040
7 doc-gen4 0x000000010045b01c l_DocGen4_Process_withFields___redArg___lam__0___boxed + 32
8 doc-gen4 0x0000000107b2e5ec lean_apply_6 + 1104
9 doc-gen4 0x0000000107b2d0f4 lean_apply_5 + 980
10 doc-gen4 0x0000000104713220 l_Lean_Meta_withNewLocalInstance___at_____private_Lean_Meta_Basic_0__Lean_Meta_withNewLocalInstancesImp_spec__0___redArg + 16
11 doc-gen4 0x00000001020797b0 l_Lean_Meta_withLocalDecl___at___Lean_Meta_withLocalDeclD___at_____private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkEnumOfNat_spec__11_spec__11___redArg + 164
12 doc-gen4 0x0000000102079994 l_Lean_Meta_withLocalDeclD___at_____private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkEnumOfNat_spec__11___redArg + 56
13 doc-gen4 0x000000010045b244 l_DocGen4_Process_withFields___redArg___lam__1___boxed + 32
14 doc-gen4 0x0000000107b2f884 lean_apply_7 + 1124
15 doc-gen4 0x0000000107b2f830 lean_apply_7 + 1040
16 doc-gen4 0x0000000107b2d288 lean_apply_5 + 1384
17 doc-gen4 0x0000000104714098 l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAux___redArg + 728
18 doc-gen4 0x00000001075e1058 l_Lean_Meta_forallTelescopeReducing___at_____private_Lean_Server_Completion_CompletionCollectors_0__Lean_Server_Completion_isDotCompletionMethod_spec__1___redArg + 160
19 doc-gen4 0x000000010045b19c l_DocGen4_Process_withFields___redArg + 312
20 doc-gen4 0x000000010045fe44 l_DocGen4_Process_StructureInfo_ofInductiveVal + 1288
21 doc-gen4 0x0000000100464e70 l_DocGen4_Process_DocInfo_ofConstant + 2648
22 doc-gen4 0x0000000100471994 l_DocGen4_Process_process___lam__0 + 5496
23 doc-gen4 0x000000010047699c l_DocGen4_Process_process___lam__0___boxed + 52
24 doc-gen4 0x0000000107b30ea0 lean_apply_8 + 2508
25 doc-gen4 0x000000010046d61c l_Std_DHashMap_Internal_AssocList_foldlM___at___Lean_SMap_forM___at___DocGen4_Process_process_spec__5_spec__5___redArg + 332
26 doc-gen4 0x000000010046f550 l___private_Init_Data_Array_Basic_0__Array_foldlMUnsafe_fold___at___Lean_SMap_forM___at___DocGen4_Process_process_spec__5_spec__11___redArg + 500
27 doc-gen4 0x000000010046faf4 l_Lean_SMap_forM___at___DocGen4_Process_process_spec__5___redArg + 344
28 doc-gen4 0x0000000100475ec8 l_DocGen4_Process_process + 2028
29 doc-gen4 0x000000010047a22c l_DocGen4_load + 2116
30 doc-gen4 0x000000010042d78c l_runSingleCmd + 424
31 doc-gen4 0x000000010042dde0 l_runSingleCmd___boxed + 20
32 doc-gen4 0x0000000107b2814c lean_apply_2 + 372
33 doc-gen4 0x0000000107b28550 lean_apply_2 + 1400
34 doc-gen4 0x0000000107b28550 lean_apply_2 + 1400
35 doc-gen4 0x0000000107b282ec lean_apply_2 + 788
36 doc-gen4 0x0000000107b282ec lean_apply_2 + 788
37 doc-gen4 0x0000000107b282ec lean_apply_2 + 788
38 doc-gen4 0x0000000107b282ec lean_apply_2 + 788
39 doc-gen4 0x0000000107b282ec lean_apply_2 + 788
40 doc-gen4 0x0000000107b282ec lean_apply_2 + 788
41 doc-gen4 0x0000000107b282ec lean_apply_2 + 788
42 doc-gen4 0x0000000107b282ec lean_apply_2 + 788
43 doc-gen4 0x0000000107b282ec lean_apply_2 + 788
44 doc-gen4 0x0000000100431da4 main + 216
45 dyld 0x0000000193167154 start + 2476
what is going on!?
Last updated: Dec 20 2025 at 21:32 UTC