error with dependencies

Stream: lean4

[Alexandre Rademaker]

I want to start a project that will depend on

• proofWidget (to display SVG in the Infoview)
• SciLean (for basic matrix operations)

SciLean depends on Mathlib, and since https://github.com/lecopivo/SciLean/blob/master/lean-toolchain says it depends on v4.15.0-rc1, I executed

lake +v4.15.0-rc1 new project math
cd project

Next, I edited my lakefile.toml to have

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.15.0-rc1"

[[require]]
name = "scilean"
scope = "lecopivo"

Next, I run lake update. At this point, I see some possible problems with the mismatching of some lean-toolchain files:

• Cli version 4.14
• LeanSearchClient version 4.13
• Qq version 4.14:

% for f in `find . -name 'lean-toolchain'`; do echo $f $(cat $f); done
./lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/mathlib/lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/plausible/lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/proofwidgets/lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/scilean/lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/batteries/lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/Cli/lean-toolchain leanprover/lean4:v4.14.0-rc1
./.lake/packages/aesop/lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/importGraph/lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/LeanSearchClient/lean-toolchain leanprover/lean4:v4.13.0
./.lake/packages/Qq/lean-toolchain leanprover/lean4:v4.14.0

I executed

% lake clean
% lake build
...
✖ [1142/2514] Running Mathlib.Lean.Meta.RefinedDiscrTree
error: no such file or directory (error code: 2)
  file: ././.lake/packages/mathlib/././Mathlib/Lean/Meta/RefinedDiscrTree.lean
✖ [1143/2514] Running Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
error: no such file or directory (error code: 2)
  file: ././.lake/packages/mathlib/././Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean
✖ [1144/2514] Running SciLean.Tactic.RefinedSimp
error: ././.lake/packages/scilean/././SciLean/Tactic/RefinedSimp.lean: bad import 'Mathlib.Lean.Meta.RefinedDiscrTree'
error: ././.lake/packages/scilean/././SciLean/Tactic/RefinedSimp.lean: bad import 'Mathlib.Lean.Meta.RefinedDiscrTree.Lookup'
...
- SciLean
- Test.Basic
- Test
error: build failed

I tried SciLean first, following the README at https://github.com/lecopivo/SciLean

% git clone https://github.com/lecopivo/SciLean.git
% cd SciLean

% lake exe cache get
...
Completed successfully!

% for f in `find . -name 'lean-toolchain'`; do echo $f $(cat $f); done
./lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/mathlib/lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/plausible/lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/proofwidgets/lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/batteries/lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/Cli/lean-toolchain leanprover/lean4:v4.14.0-rc1
./.lake/packages/aesop/lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/importGraph/lean-toolchain leanprover/lean4:v4.15.0-rc1
./.lake/packages/LeanSearchClient/lean-toolchain leanprover/lean4:v4.13.0
./.lake/packages/Qq/lean-toolchain leanprover/lean4:v4.14.0

% lake build
...
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, dlopen(././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib, 0x0009): tried: '././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '././.lake/packages/batteries/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '././.lake/packages/Qq/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '././.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '././.lake/packages/aesop/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '/Users/ar/.elan/toolchains/leanprover--lean4---v4.15.0-rc1/lib/././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '/Users/ar/.elan/toolchains/leanprover--lean4---v4.15.0-rc1/lib/lean/././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '/usr/lib/././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file, not in dyld cache), '././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '././.lake/packages/batteries/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '././.lake/packages/Qq/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '././.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '././.lake/packages/aesop/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '/Users/ar/r/temp/SciLean/.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS/Users/ar/r/temp/SciLean/.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '/Users/ar/r/temp/SciLean/.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag)
error: Lean exited with code 134
Some required builds logged failures:
- SciLean.Tactic.CompiledTactics
error: build failed

So, SciLean is indeed broken. Am I right @Tomas Skrivan ? To make sure..

% lake clean -- this should remove all precompiled files that `lake exe cache get` got, right?
% lake build
...
Some required builds logged failures:
- SciLean.Tactic.CompiledTactics
error: build failed

So, I guess if I made something wrong, what would be the appropriate step-by-step procedure for creating my project with such dependencies?

On the other hand, it may only be that Mathlib 4.15.0-rc1 is broken, and it is causing SciLean to break, too.

[Yaël Dillies]

Careful! I don't think this (the whole of) your issue, but

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.15.0-rc1"

means "Make me depend on mathlib commit 41ff1f7899c971f91362710d4444e338b8acd644 (the one tagged with v4.15.0-rc1). In particular, this is not the commit that SciLean depends on which is instead df255e235cde3ac9e4325de51cfa2bc82b7b2416 (see SciLean's lake-manifest.json).

[Tomas Skrivan]

Just depend on SciLean and you will get mathlib as a transitive dependency

[Yaël Dillies]

You should remove that rev line in the mathlib part of your lakefile, and instead run lake update scilean

[Tomas Skrivan]

But you still seem to have an issue building clean SciLean on its own. I will investigate that.

[Yaël Dillies]

Relatedly, Tomas, may I convince you to bump your SciLean to tagged versions of mathlib and release accordingly-tagged versions of SciLean?

[Tomas Skrivan]

Yes I will do that

[Alexandre Rademaker]

Thank you, @Tomas Skrivan and @Yaël Dillies, for investigating it. The error in the building of Scilean alone is problematic. The mismatch of the Mathlib version in the lake-manifest.json of SciLean is strange... Actually, SciLean depends on the HEAD of the main branch of Mathlib.

https://github.com/lecopivo/SciLean/blob/master/lakefile.lean#L90

Moreover, my project's primary concern is making SciLean closely follow ProofWidgets, which in turn follows Mathlib. We must create a PR to ProofWidgets to support more SVG primitives.

[Alexandre Rademaker]

But I don't know when and how the lake-manifest.json is updated.

Actually, I found the following information on the lake README: https://github.com/leanprover/lean4/blob/master/src/lake/README.md#adding-dependencies.

It suggests that the manifest is updated after the building. I was expecting it to be updated during the lake update. ' If I understood it right, the lake exe cache get consults the manifest to retrieve a specific version of the compiled files.

[Tomas Skrivan]

Alexandre Rademaker said:

Moreover, my project's primary concern is making SciLean closely follow ProofWidgets, which in turn follows Mathlib. We must create a PR to ProofWidgets to support more SVG primitives.

Right, the SVG example was not designed to be easily extensible by the user which is not ideal. You can probably copy all the code of SVG and InteractiveSVG and extend that. Ideally redesign it to make it user extensible.

[Tomas Skrivan]

This is self contained file depending on ProofWidgets that redefines all the SVG things again so you can extend them however you want without making a PR to ProofWidgets

[Tomas Skrivan]

Alexandre Rademaker said:

So, SciLean is indeed broken. Am I right Tomas Skrivan ? To make sure..

% lake clean -- this should remove all precompiled files that `lake exe cache get` got, right?
% lake build
...
Some required builds logged failures:
- SciLean.Tactic.CompiledTactics
error: build failed

So, I guess if I made something wrong, what would be the appropriate step-by-step procedure for creating my project with such dependencies?

On the other hand, it may only be that Mathlib 4.15.0-rc1 is broken, and it is causing SciLean to break, too.

I can't reproduce this. I tried:

$ git clone git@github.com:lecopivo/SciLean.git
$ cd SciLean/
$ lake exe cache get
$ lake build

and it finished successfully. I'm on Ubuntu 22.04 and not on MacOS which you are running if I'm not mistaken.

[Alexandre Rademaker]

I got an error; see https://gist.github.com/arademaker/c743e015d78071dcb6c7b3e5aa334308

Yes, I am running on MacOS 15.4 (24E248), Apple M4 with 24GB of RAM.

[Tomas Skrivan]

This looks like a bug in Lean related to the precompiledModules:=true option and arm architecture. Not sure what to do about this :/

[Alexandre Rademaker]

Regarding the ProofWidgets.. I was not clear. We will eventually make a PR to ProofWidgets because we need more primitives to implement our visualization library. See https://github.com/leanprover-community/ProofWidgets4/issues/110. We are not talking about the SVG examples in the SciLean repository.

[Alexandre Rademaker]

It looks like the same error was reported by @Sebastian Ullrich in October. I added a comment in https://github.com/leanprover/lean4/issues/5649.

[Tomas Skrivan]

Alexandre Rademaker said:

Regarding the ProofWidgets.. I was not clear. We will eventually make a PR to ProofWidgets because we need more primitives to implement our visualization library. See https://github.com/leanprover-community/ProofWidgets4/issues/110. We are not talking about the SVG examples in the SciLean repository.

I understood that, the gist I shared contained all the SVG code in ProofWidgets.

What I was just trying to say is that by using that code you can extend the SVG type and use it with SciLean without making a PR to ProofWidgets and then waiting until it gets merged to ProofWidgets and then to mathlib and then to SciLean.

[Alexandre Rademaker]

I see, but @Tomas Skrivan, in this case, my project would still depend on SciLean, which in turn depends on Mathlib, which depends on ProofWidgets.

So adding https://gist.github.com/lecopivo/f151f73b0ef6fe803fbb48356fe33d97 in my project would not cause errors related to the redefinition of symbols loaded from the proofWidgets?

[Tomas Skrivan]

Yes it would still depend on SciLean, Mathlib and ProofWidgets. The SVG already lives in the ProofWidgets namespace so there should be no clash. Maybe just put yours in MySVG namespace or whatever.

Once your project works as you want, back porting your additions to ProofWidgets.SVG would be great. But having your own version now prevents you from the painful roundtrip of PRs that would be partially out of your control.