v4.8.0-rc2 discussion

Stream: general

[Damiano Testa]

I just updated to leanv4.8.0-rc2, but it seems that my lakefile no longer works: what I am doing wrong?

This is what I see:

$ lake exe cache get
error: ././lakefile.lean:1:0: error: object file '/home/damiano/.elan/toolchains/leanprover--lean4---v4.8.0-rc2/lib/lean/Lake/Build.olean' of module Lake.Build does not exist
error: ././lakefile.lean:3:5: error: unknown namespace 'Lake'
error: ././lakefile.lean:5:0: error: unexpected identifier; expected command
error: ././lakefile.lean:21:0: error: unexpected identifier; expected command
error: ././lakefile.lean:35:17: error: unexpected identifier; expected 'abbrev', 'axiom', 'binder_predicate', 'builtin_initialize', 'class', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
error: ././lakefile.lean:42:91: error: unexpected identifier; expected 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_initialize', 'class', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
error: ././lakefile.lean:50:87: error: unexpected identifier; expected 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_initialize', 'class', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
error: ././lakefile.lean:54:100: error: unexpected identifier; expected 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_initialize', 'class', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
error: ././lakefile.lean:59:61: error: unexpected identifier; expected 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_initialize', 'class', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
error: ././lakefile.lean:68:2: error: unexpected identifier; expected 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_initialize', 'class', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
error: ././lakefile.lean:79:14: error: unexpected identifier; expected 'abbrev', 'axiom', 'binder_predicate', 'builtin_initialize', 'class', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
error: ././lakefile.lean:90:2: error: unexpected identifier; expected 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_initialize', 'class', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
error: ././lakefile.lean: package configuration has errors

[Damiano Testa]

This is how my lakefile begins

$ head lakefile.lean
import Lake

open Lake DSL

package mathlib where
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`autoImplicit, false⟩,
    ⟨`relaxedAutoImplicit, false⟩
  ]

...

[Utensil Song]

It seems that you need lake -R exe cache get.

[Damiano Testa]

let me try that!

[Damiano Testa]

No, same error:

$ lake -R exe cache get
error: ././lakefile.lean:1:0: error: object file '/home/damiano/.elan/toolchains/leanprover--lean4---v4.8.0-rc2/lib/lean/Lake/Build.olean' of module Lake.Build does not exist
error: ././lakefile.lean:3:5: error: unknown namespace 'Lake'
error: ././lakefile.lean:5:0: error: unexpected identifier; expected command
...

[Utensil Song]

Also you need to check lean-toolchain to make sure the toolchain is indeed updated.

[Damiano Testa]

$ cat lean-toolchain
leanprover/lean4:v4.8.0-rc2

[Utensil Song]

Try reinstalling the toolchain?

elan uninstall leanprover/lean4:v4.8.0-rc2
elan install leanprover/lean4:v4.8.0-rc2

[Damiano Testa]

This is looking promising...

[Damiano Testa]

Success!! Thanks!

[François G. Dorais]

(Move to v4.8.0-rc2 discussion?)

[Notification Bot]

11 messages were moved here from #general > v4.8.0-rc1 discussion by Damiano Testa.

[Sebastian Ullrich]

@Damiano Testa What is your elan version?

[Damiano Testa]

I do not know what it was, since, after something failed, I typed elan self update. After that, it was (and still is)

$ elan --version
elan 3.1.1 (71ddc6633 2024-02-22)

[Damiano Testa]

I had not looked at the version before updating, however, I still had the errors with the version above.

[Sebastian Ullrich]

Okay, it is good to know at least that it was an old version that downloaded the corrupted toolchain

[Kim Morrison]

I promise that this time I only tagged v4.8.0-rc2 once!

[Yaël Dillies]

It's great to see that wrong imports now don't immediately stall the build!

[Yaël Dillies]

However there are a bunch of things that I'm finding wrong which might be related to that change. Consider my LeanCamCombi project. If you check it out and run ./scripts/update_mathlib.sh; ./scripts/mk_all.sh; lake build, you get a bunch of output ending in

Some builds logged failures:
- Mathlib.GroupTheory.Subgroup.Basic
- LeanCamCombi.Kneser.Mathlib
- Mathlib.GroupTheory.Subgroup.Actions
- LeanCamCombi.Kneser.MulStab
- LeanCamCombi.Kneser.Kneser
- LeanCamCombi.Archive.CauchyDavenportFromKneser
- LeanCamCombi.Impact
- Mathlib.Data.Finset.LocallyFinite.Basic
- LeanCamCombi.Mathlib.Algebra.BigOperators.LocallyFinite
- LeanCamCombi.Incidence
- LeanCamCombi.Kneser.KneserRuzsa
- Mathlib.Algebra.Parity
- Mathlib.GroupTheory.Submonoid.Operations
- LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
- Mathlib.Data.Set.Intervals.OrdConnected
- LeanCamCombi.Mathlib.Data.Finset.PosDiffs
- Mathlib.Order.LocallyFinite
- LeanCamCombi.Mathlib.Order.LocallyFinite
- LeanCamCombi
- LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
- LeanCamCombi.Mathlib.Order.Partition.Finpartition
- LeanCamCombi.KruskalKatona
- LeanCamCombi.SimplicialComplex.Simplex

[Martin Dvořák]

I just upgraded to v4.8.0-rc2 and I totally love it. Really amazing version!

[Yaël Dillies]

I would hope this is a list of the files I need to fix. However it is really far from this:

• Mathlib.Algebra.Parity, Mathlib.Order.LocallyFinite, Mathlib.GroupTheory.Submonoid.Operations, etc... are all files that don't exist (anymore, because I removed them from mathlib). They all are imported in some other file of my project. Why do they (and not just the files importing them) show up in the list of files that failed to build?
• LeanCamCombi.Kneser.Kneser, LeanCamCombi, etc... indeed failed to build, but their dependencies failed to build as well. Why report failure of files that I can't yet fix?

[Kim Morrison]

@Yaël Dillies, please file an issue for point 1. I'm skeptical of point 2, but don't have time to check it out myself. Can you produce a smaller example showing this issue.

[Yaël Dillies]

For point 1, I've opened lean#4256. For point 2, I'm not sure how to provide a small example given that's a cross-file issue, but here's one way to reproduce:

• Create a new project MyProject
• Add a file MyProject.Foo containing example : False := trivial
• Add a file MyProject.Bar containing import MyProject.Foo
• Run lake build MyProject.Bar

The output will end in

Some builds logged failures:
- MyProject.Foo
- MyProject.Bar

instead of the expected

Some builds logged failures:
- MyProject.Foo

[Kim Morrison]

@Yaël Dillies, can't reproduce. I tried doing exactly that, and I only get the file containing example : False := trivial reported after "Some builds logged failures".

[Kim Morrison]

Are you using globs, or importing everything in the main file?

[Yaël Dillies]

In LeanCamCombi, I am importing everything in LeanCamCombi.lean and this is the main target

[Kim Morrison]

Could you make a repo?

[Kim Morrison]

I did lake new and followed your instructions but couldn't reproduce.

[Yaël Dillies]

Hmm, there's clearly something wrong when running it on LeanCamCombi, as evidenced by the - LeanCamCombi line in my above snippet. You can checkout https://github.com/YaelDillies/LeanCamCombi/commit/c64efb6b6b2447b1966e7c71506353b73140d504, run ./scripts/update-mathlib.sh; ./scripts/mk_all.sh; lake build and hopefully you will see the same output as I did.

[Yaël Dillies]

If that's not enough to convince you there's something wrong, I'll try minimising later

[Mario Carneiro]

@Mac Malone I'm getting failures in a lake script in rc2 because #synth MonadLiftT JobM FetchM no longer succeeds. Was this replaced by something else?

[Mario Carneiro]

(cargo-culted my way to Job.async but it would be nice to get confirmation)

[Mac Malone]

@Mario Carneiro No that is bug. :sad: (And one that I though I had ensured worked.) (Oh, I actually I think I broke it after I did that check.)

[Mario Carneiro]

do you know what the equivalent of the lift is? Is Job.async adding additional asynchrony on top?

[Mac Malone]

After saying that, I realized there actually isn't one any longer.

[Mac Malone]

The problem is that the old JobM actions should be LogIO instead.

[Mario Carneiro]

what's the context of this change? I'm not sure I have a great understanding of what these monads represent

[Mario Carneiro]

In the script in question, it was using buildUnlessUpToDate inside a target := declaration

[Mac Malone]

JobM is the monad of a job. It now includes state about that job which is absent from FetchM.

[Mac Malone]

Mario Carneiro said:

In the script in question, it was using buildUnlessUpToDate inside a target := declaration

Oh, in that case, it definitely should have been using Job.async.

[Mario Carneiro]

which does what?

[Mac Malone]

Produces an asynchronous Job from the JobM action.

[Mario Carneiro]

somehow this doesn't explain things

[Mario Carneiro]

I can see that much from the name of the function. I don't know what that actually means though

[Mario Carneiro]

what's the reason you say it "should" be using Job.async?

[Mac Malone]

Not much more than that? It spawns asynchronous task performing the JobM actions, wraps it in the Job structure, and returns it.

[Mario Carneiro]

if it's not async, why is that bad

[Mac Malone]

Because that will unnecessarilyhalt the rest of the jobs wherever it is in the dependency graph from starting until it finishes?

[Mario Carneiro]

I don't know, does it? Lake has a ton of parallelism, I don't know what thread it's on to begin with

[Mario Carneiro]

will it block the main thread?

[Mac Malone]

Yes

[Mac Malone]

Everything runs on the main thread unless it spawns a job.

[Mario Carneiro]

So is FetchM only for determining dependencies and not doing "work"?

[Mac Malone]

Yes

[Mac Malone]

Yaël Dillies said:

I would hope this is a list of the files I need to fix. However it is really far from this:

• Mathlib.Algebra.Parity, Mathlib.Order.LocallyFinite, Mathlib.GroupTheory.Submonoid.Operations, etc... are all files that don't exist (anymore, because I removed them from mathlib). They all are imported in some other file of my project. Why do they (and not just the files importing them) show up in the list of files that failed to build?
• LeanCamCombi.Kneser.Kneser, LeanCamCombi, etc... indeed failed to build, but their dependencies failed to build as well. Why report failure of files that I can't yet fix?

For point (1), an import , in Lake's mind is a reuqest to build the corresponding olean of the module. Thus, lake attempts to do just (thus creating a Lake job for it), but that job then fails when it cannot find the source file from which to build. It is important to note that a missing source file is not necessarily an error at import time. For example, binport of mathport succesfully produces oleans without source files.

For point (2), Lake does not yet know how to distinguish between a build failing for its own reason versus for a reason caused by its dependencies. However, this should be fixable in a future refactor. As for why Kim could not reproduce this, I suspect this is likely because the oleans in quesition already existing in your cases but not in theirs, but I am not sure why exactly that would make a difference.

[Yaël Dillies]

I understand exactly why point 1 is happening, but I am claiming this is not useful behavior, or at least not useful default behavior.

[Jens Petersen]

I have a Fedora Linux Copr repo where I built the rc's in the lean4-rc package there
https://copr.fedorainfracloud.org/coprs/petersen/lean4/monitor/detailed
(in addition to the main lean4 package)

[Kim Morrison]

Perhaps you know this already, but we advise users to never install a fixed version of Lean from a package manager, but always to install elan and allow it to dynamically provide Lean toolchains depending on the lean-toolchain file in each project.

[Jens Petersen]

I want to ship programs written in Lean4 in the future in Fedora

[Mario Carneiro]

for plain executables written in lean, you should be able to get them statically linked with lean, in which case you don't need to provide lean separately after the build step and can ship only the executable

[Jens Petersen]

To be clear by "ship" I meant include in the Fedora Linux distro. Static linking is probably fine, but I want to have packages using Lean in Fedora, ie that requires having Lean4 in Fedora too to build them. Admittedly I am still rather new to Lean so it is not going to happen overnight - eg I might port some of my existing tools written in Haskell which are in Fedora to Lean over time...

[Eric Wieser]

Either you need multiple incompatible versions of lean in fedora to build those tools, or fedora needs to take on the job of patching a bunch of lean packages to all be mutually compatible on every release

[Joachim Breitner]

Correct. It's qualitatively not very different from the situation with Haskell and GHC. I also expect that normal “programs” written in lean will be less sensitive to lean changes that proof developments like mathlib, which falls apart whenever you touch just about anything in lean :-)