Issue with `Duper` in `The Mechanics of Proof`

Stream: Lean for teaching

[Jon Bannon]

Maybe there is a quick fix for this weird emergent problem. I'm teaching using Heather Macbeth's book , and everything was going very well. Suddenly, though, on my local machine the import for the exhaust tactic failed. If I comment out this import, things work fine (actually, there is an autograder import that also needs to be removed, but I can live without that because my class is small). The students don't have this trouble (yet), so I expect the problem might be something that I did. I believe the problem is a mismatch of something with Duper, as in the lakefile for my fork of this repo I have

require mathlib from git "https://github.com/leanprover-community/mathlib4" @ s!"v{Lean.versionString}"
require Duper from git "https://github.com/hrmacbeth/duper" @ "main"
require autograder from git "https://github.com/robertylewis/lean4-autograder-main" @ "864b34ce06d8536aec0c38e57448c17d1f83572a"

I've tried changing this local version of Duper to the leanprover-community one, but that didn't work. I've also deleted the repo and re-cloned it, and the problem persists. Has anyone had an issue like this? If so, what's the repair?

[Kevin Buzzard]

If you've deleted and recloned, can you give a more precise repro? i.e. "open this file, add this import, it should work, but I get this error"?

[Jon Bannon]

OK. I deleted and recloned. If I open the file Math2001/Homework/hw9.lean and comment out import AutograderLib and import Library.Tactic.Exhaust things work. If I leave these in then I get the following (too large for comment so I have truncated) error that begins:

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

stderr:
info: [614/898] Building Duper.Order
info: [617/913] Building Duper.DUnif.UnifProblem
info: [631/925] Building Duper.Util.AbstractMVars
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/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean:/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib:./.lake/packages/Duper/.lake/build/lib /Users/jon/.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/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean/libDuper-Util-MessageData-1.dylib' (no such file), '/Users/jon/.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/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/./.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), '/Users/jon/.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/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean/libDuper-Util-MessageData-1.dylib' (no such file), '/Users/jon/.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/jon/LeanRepos/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/jon/LeanRepos/math2001/.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (no such file), '/Users/jon/LeanRepos/math2001/.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag)
error: external command /Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/bin/lean exited with code 134
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/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean:/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib:./.lake/packages/Duper/.lake/build/lib /Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/bin/lean -Dlinter.unusedVariables=false ./.lake/packages/Duper/././Duper/Order.lean -R ./.lake/packages/Duper/./. -o ./.lake/packages/Duper/.lake/build/lib/Duper/Order.olean -i ./.lake/packages/Duper/.lake/build/lib/Duper/Order.ilean -c ./.lake/packages/Duper/.lake/build/ir/Duper/Order.c --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-Reduction-1.dylib --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Expr-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-Misc-1.dylib, 0x0009): tried: './.lake/packages/std/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/Qq/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/aesop/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/proofwidgets/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/Cli/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/mathlib/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/autograder/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), '/Users/jon/.elan/toolchains/leanprover--...
`

[Eric Wieser]

@ s!"v{Lean.versionString}" doesn't look particularly sensible to me I guess that's upstream though

[Jireh Loreaux]

@Jon Bannon I just did a fresh clone of this repo, ran lake exe cache get and open hw9.lean without issue (after it built the files leading up to it).

[Jireh Loreaux]

What version of elan do you have?

[Jireh Loreaux]

elan --version (mine: 4.0.0)

[Kevin Buzzard]

Me too: git clone <repo>, lake exe cache get, lake build (runs mostly without errors), I open the file and it's fine. I'm on elan 4.0.0. (elan self update if you're not)

[Jireh Loreaux]

Kevin, this is on a really old version of the Lean toolchain (4.3.0), so the errors don't all collect at the end. You got no errors at all?

[Jireh Loreaux]

(try running lake build again)

[Kevin Buzzard]

You're right -- scrolling up a I see a few errors, but the file in question was fine. I was misled by there being no reporting at the end of the form "here are the files with errors" but as you say this is because it's an old version of Lean. I'll edit.

[Jireh Loreaux]

The first file to error for me is Math2001/09_Sets/02_Set_Operations.lean and when you open it, it's failing at the check_equality_of_explicit_sets tactic, just saying that it failed to rule out other cases.

[Jon Bannon]

I'm away from my computer, but I expect my elan version is wrong.

[Jon Bannon]

Strange. My elan version is elan 4.0.0 (bb75b50d2 2025-01-30)

[Jon Bannon]

I deleted the repo again, and then cloned Heather's : https://github.com/hrmacbeth/math2001

There, her hw 9 doesn't use exhaust, but the file Jireh mentioned :

Math2001/09_Sets/02_Set_Operations.lean

won't compile for me if I don't comment out the Exhaust import, as above.

[Kevin Buzzard]

Oh so we're not cloning the same repo?? So your question is "I changed the repo and then it broke and I'm asking why but I'm not telling you which repo I'm using"??

[Jon Bannon]

Sorry Kevin. That was indeed EVIL. :sad:

[Jon Bannon]

Originally I was using my own fork of the repo (which I just realized). Alas, the original repo you cloned (which given my crime I should explicitly state as https://github.com/hrmacbeth/math2001) still gives me the error I was seeing. Sorry again!

Here is the error, too:

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

stderr:
info: [613/894] Building Duper.Order
info: [621/913] Building Duper.DUnif.UnifProblem
info: [642/936] Building Duper.Util.AbstractMVars
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/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean:/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib:./.lake/packages/Duper/.lake/build/lib /Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/bin/lean -Dlinter.unusedVariables=false ./.lake/packages/Duper/././Duper/Order.lean -R ./.lake/packages/Duper/./. -o ./.lake/packages/Duper/.lake/build/lib/Duper/Order.olean -i ./.lake/packages/Duper/.lake/build/lib/Duper/Order.ilean -c ./.lake/packages/Duper/.lake/build/ir/Duper/Order.c --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-Reduction-1.dylib --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Expr-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-Misc-1.dylib, 0x0009): tried: './.lake/packages/std/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/Qq/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/aesop/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/proofwidgets/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/Cli/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/mathlib/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/autograder/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), '/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean/libDuper-Util-Misc-1.dylib' (no such file), '/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS./.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), '/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/./.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), '/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean/./.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), '/usr/lib/./.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file, not in dyld cache), './.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/std/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/Qq/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/aesop/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/proofwidgets/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/Cli/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/mathlib/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/autograder/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), '/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean/libDuper-Util-Misc-1.dylib' (no such file), '/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/libDuper-Util-Misc-1.dylib' (no such file), './.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/Users/jon/LeanRepos/math2001/.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS/Users/jon/LeanRepos/math2001/.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib' (no such file), '/Users/jon/LeanRepos/math2001/.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag)
error: external command /Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/bin/lean exited with code 134

[Kevin Buzzard]

OK so just to be clear, if you do this:

git clone git@github.com:hrmacbeth/math2001.git
cd math2001
lake exe cache get
lake build Math2001.Homework.hw9

are you error-free?

[Kevin Buzzard]

That error looks to me like it says "you are using a version of Duper which doesn't play well with some of your other choices"

[Jon Bannon]

Let me try this explicit sequence ot steps to ensure we are on the same page...

[Kevin Buzzard]

Huh, this time I got an error!

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/autograder/.lake/build/lib:./.lake/build/lib /Users/buzzard/.elan/toolchains/leanprover--lean4---v4.3.0/bin/lean -Dlinter.unusedVariables=false -DquotPrecheck=false -DwarningAsError=false -Dpp.unicode.fun=true ./././Math2001/Homework/hw9.lean -R ././. -o ./.lake/build/lib/Math2001/Homework/hw9.olean -i ./.lake/build/lib/Math2001/Homework/hw9.ilean -c ./.lake/build/ir/Math2001/Homework/hw9.c --load-dynlib=./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, dlopen(./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib, 0x0009): tried: './.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/Users/buzzard/.elan/toolchains/leanprover--lean4---v4.3.0/lib/./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/Users/buzzard/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean/./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/usr/lib/./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file, not in dyld cache), './.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/Users/buzzard/crap/math2001/.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS/Users/buzzard/crap/math2001/.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/Users/buzzard/crap/math2001/.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag)
error: external command /Users/buzzard/.elan/toolchains/leanprover--lean4---v4.3.0/bin/lean exited with code 134

[Jon Bannon]

It doesn't like the Autograder import, right? If you comment that out it should get rid of the error (except for all of the [@autograder _] attributes)?

[Kevin Buzzard]

I tried on a mac this time. Previously I was on linux. @Jireh Loreaux which OS were you on? And Jon?

[Jon Bannon]

I'm on a Mac, running Sequoia 15.4 (and recently allowed an update for this!)

[Jon Bannon]

I'm pretty sure Jireh is on a PC...running Arch Linux (see below).

[Kevin Buzzard]

I just ssh'ed into my linux machine (Ubuntu 24.04) and confirm that those commands I posted above work fine on it. The errors I'm seeing are also on Mac Sequoia 15.4.

[Jon Bannon]

I performed those steps, and am still getting the error on hw9 :

error loading library, dlopen(./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib, 0x0009): tried: './.lake/packages/std/.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/Qq/.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/aesop/.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/proofwidgets/.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/Cli/.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/mathlib/.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/Duper/.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean/libAutograderLib-1.dylib' (no such file), '/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean/./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/usr/lib/./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file, not in dyld cache), './.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/std/.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/Qq/.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/aesop/.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/proofwidgets/.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/Cli/.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/mathlib/.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/Duper/.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean/libAutograderLib-1.dylib' (no such file), '/Users/jon/.elan/toolchains/leanprover--lean4---v4.3.0/lib/libAutograderLib-1.dylib' (no such file), '/Users/jon/LeanRepos/math2001/.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS/Users/jon/LeanRepos/math2001/.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/Users/jon/LeanRepos/math2001/.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag)

[Kevin Buzzard]

I think we can escalate this to #lean4 , I'll post there.

[Jon Bannon]

And...if I comment out import AutograderLib then the file works (aside from not recognizing @[autograder _])

[Derek Rhodes]

I followed the steps with Mac Sequoia 15.3 and did not get any compiler errors, only warnings about sorries.

[Jon Bannon]

Huh! Maybe it was the recent update to Sequoia 15.4? This is the only thing I did differently between now and the last time I was teaching...so maybe there is something in the update...

[Kevin Buzzard]

Warnings about sorrys are fine, I think the idea of the homework is to fill in them in :-)

[Jon Bannon]

Ah...and the students all have PCs, I think.

[Jireh Loreaux]

Kevin Buzzard said:

I tried on a mac this time. Previously I was on linux. Jireh Loreaux which OS were you on? And Jon?

@Kevin Buzzard Arch Linux, so this is reproducible under different systems.

[Jon Bannon]

@Jireh Loreaux Should the fact that this is reproducible under different systems appear in (#lean4 > Mac Sequoia 15.4 regression?)?

[Jireh Loreaux]

I will, I'm just confirming my repro example.

[Derek Rhodes]

Hi, I've updated the math2001 (Mechanics of Proof) code base from v4.3.0 to v4.18.0, the changes can be found here:
https://github.com/drhodes/math2001/tree/v4.18.0

Some things have not yet been updated:

• dependencies for duper / autograder have been commented out in the lakefile. (they might work now!)
• Duper imports and the exhaust tactic are entirely commented out, along with the ~60 examples that depend on them.
• The numbers tactic is not fully working, but @Mario Carneiro provided a solution here on zulip
• The TruthTable widget needs work, therefore #truth_table cmds have been commented.
• addarith has a hiccup, but my sense is that there is an easy fix. (three addarith examples have been commented)

I also introduced TODOs when commenting something out , but always on the mathlib commit (in the lakefile) where the relevant code broke, which localizes the cause, so git diff on mathlib at that commit will hold some debugging clues.

[Kim Morrison]

cc'ing @Heather Macbeth.

[Kevin Buzzard]

I spoke to Heather about this yesterday. The correct fix really is to make the project not depend on duper any more and to write a new tactic which does the things that duper was doing. Unfortunately grind is too powerful! Heather said she'd spent some time last year trying to persuade other people to write the tactic she wanted but now knows enough metaprogramming to write it herself.

[Derek Rhodes]

Nice! I don't know if it was announced anywhere but @Siddhartha Gadgil has an excellent series of metaprogramming videos, good for people interested in learning how to write custom tactics. (I'm working through them now).