Mechanics of Proof 8.1 Homework: Imports are out of dat...

Stream: new members

[Siavash Kazemian]

Hi a friend of mine and I are unable to find a way of importing Library.Tactic.Exhaust when we open Homework 8.1 from Mechanics of Proof (Chapter 8 Functions->Injective_Surjective.lean) from https://hrmacbeth.github.io/math2001/. We're using VSCode + Lean 4 on a Mac. Interestingly, we don't have this problem if we use VSCode + Lean 4 extension on linux. Without importing Library.Tactic.Exhaust things load fine. Re-installing the extension and Restarting File have not fixed the problem. Any help would be deeply appreciated.

Here is the log of the Modules that are compiled correctly and what throws errors: (Duper.DUnif.UnifProblem)

01_Injective_Surjective.lean:1:0Messages (1)

01_Injective_Surjective.lean:1:0

/Users/SKazemian/.elan/toolchains/leanprover--lean4---v4.3.0/bin/lake print-paths Init Mathlib.Data.Real.Basic Library.Basic Library.Tactic.Exhaust Library.Tactic.ModEq Library.Theory.ParityModular failed:

stderr:
info: [261/757] Compiling Std.Lean.LocalContext
info: [261/758] Compiling Std.Lean.Parser
...
info: [890/1055] Linking Duper.Util.LazyList
info: [892/1055] Building Duper.DUnif.UnifProblem
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/mathlib/.lake/build/lib:./.lake/packages/Duper/.lake/build/lib:./.lake/packages/autograder/.lake/build/lib:./.lake/build/lib DYLD_LIBRARY_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/mathlib/.lake/build/lib:./.lake/packages/Duper/.lake/build/lib:./.lake/packages/autograder/.lake/build/lib:./.lake/build/lib:/Users/SKazemian/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean:/Users/SKazemian/.elan/toolchains/leanprover--lean4---v4.3.0/lib:./.lake/packages/Duper/.lake/build/lib /Users/SKazemian/.elan/toolchains/leanprover--lean4---v4.3.0/bin/lean -Dlinter.unusedVariables=false ./.lake/packages/Duper/././Duper/DUnif/UnifProblem.lean -R ./.lake/packages/Duper/./. -o ./.lake/packages/Duper/.lake/build/lib/Duper/DUnif/UnifProblem.olean -i ./.lake/packages/Duper/.lake/build/lib/Duper/DUnif/UnifProblem.ilean -c ./.lake/packages/Duper/.lake/build/ir/Duper/DUnif/UnifProblem.c --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-LazyList-1.dylib
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, dlopen(./.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib, 0x0009): tried: './.lake/packages/std/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/packages/Qq/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/packages/aesop/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/packages/proofwidgets/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/packages/Cli/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/packages/mathlib/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/autograder/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), '/Users/SKazemian/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean/libDuper-Util-MessageData-1.dylib' (no such file), '/Users/SKazemian/.elan/toolchains/leanprover--lean4---v4.3.0/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS./.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), '/Users/SKazemian/.elan/toolchains/leanprover--lean4---v4.3.0/lib/./.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), '/Users/SKazemian/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean/./.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), '/usr/lib/./.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file, not in dyld cache), './.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/std/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/packages/Qq/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/packages/aesop/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/packages/proofwidgets/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/packages/Cli/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/packages/mathlib/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/autograder/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), '/Users/SKazemian/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean/libDuper-Util-MessageData-1.dylib' (no such file), '/Users/SKazemian/.elan/toolchains/leanprover--lean4---v4.3.0/lib/libDuper-Util-MessageData-1.dylib' (no such file), './.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/Users/SKazemian/Documents/math2001/.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS/Users/SKazemian/Documents/math2001/.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), '/Users/SKazemian/Documents/math2001/.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag)
error: external command /Users/SKazemian/.elan/toolchains/leanprover--lean4---v4.3.0/bin/lean exited with code 134
info: [893/1055] Compiling Duper.Util.Misc
info: [894/1055] Linking Duper.Util.Misc
info: [895/1055] Building Duper.Util.AbstractMVars
info: [895/1055] Building Duper.Order
error: > ...

Screenshot 2025-08-27 at 3.49.53 PM.png

[Henrik Böving]

This is a known bug and can be fixed by upgrading your Lean version to v4.20.0 or later. Unfortunately the specific resource you are working with is currently stuck at 4.3.0 so it's likely that modern Mac users will be unable to use it until that upgrade happens, CC @Heather Macbeth

[Siavash Kazemian]

Got it! Thank you so much Henrik. I upgraded and tried to port the assignments I wanted to work on.