Zulip Chat Archive

Stream: mathlib4

Topic: Error: unreachable @ extractMainModule


Kevin Buzzard (Jul 26 2023 at 17:50):

On line 62 of Data.Nat.Cast.Defs if I type whatsnew in then I get the following error:

Lean (version 4.0.0-nightly-2023-07-12, commit 6e904421304c, Release)
Error: unreachable @ extractMainModule
backtrace:
/media/buzzard/ExternalSSD1TB/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x9e)[0x7f2966905cae]
/media/buzzard/ExternalSSD1TB/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so(l_Lean_Name_append+0x3bd)[0x7f2963eff25d]
/media/buzzard/ExternalSSD1TB/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so(l_Std_Range_forIn_loop___at_Lean_PrettyPrinter_Delaborator_delabConst___spec__4+0x19a)[0x7f29647e17ca]

I'm editing files like Algebra.Group.Defs so my mathlib is in a funny uncompiled state. Can anyone else reproduce?


Last updated: Dec 20 2023 at 11:08 UTC