Lean 4 version for teaching

Stream: Lean for teaching

[Martin Dvořák]

My course currently runs on leanprover/lean4:nightly-2023-03-07 which I selected when I was working on the first materials.
Do you have any recommendation whether to switch to a newer Lean version and when to do it?
It seems to me that in our 3rd block (which will happen in 2024-01 probably)
https://github.com/madvorak/lean-mam/blob/main/mam/Cislo3.lean
we would benefit from having a newer Mathlib.
In particular library_search might be a bit uncomfortable for my students.

Should we switch to leanprover/lean4:v4.2.0-rc1 or something like it?
If yes, would you do it now, or right before the 3rd block starts? My students have just started solving exercises from our 2nd block.

[Patrick Massot]

Right now is a very bad moment to switch since a new version of Lean is about to be pre-released, with lots of improvements.

[Martin Dvořák]

Thank you very much! Your response is exactly what I wanted to hear!

[Patrick Massot]

Of course there is a risk that I will keep repeating the same advice every day, because Lean 4 and its tooling is evolving so fast!

[Scott Morrison]

I'm trying to get this out today. Anyone who has some time to work on tidying up #7606 would be helping. :-)

[Eric Wieser]

If the goal is to push that through ASAP, I think we should tag every simpNF regression with "probably caused by #7657"

[Eric Wieser]

That way when we fix #7657, it's easy to clean up, and we can remove the comment in the places we were wrong

[Scott Morrison]

I'm tagging every simpNF regression for lemmas generated with simps that way, yes! Almost done.

[Mauricio Collares]

Patrick Massot said:

Right now is a very bad moment to switch since a new version of Lean is about to be pre-released, with lots of improvements.

@Martin Dvořák Scott bumped mathlib to 4.2.0-rc2, so now is probably a good time to upgrade.

[Martin Dvořák]

It is 4.2.0-rc3 now. Is it yet another version?

[Utensil Song]

It's rc2 plus the quick fix for this issue. It's more stable and ready for teaching.

[Martin Dvořák]

I bumped as well! What does the following error mean?

$ lake build
error: > curl -s -f -o .\lake-packages\proofwidgets\build\windows-64.tar.gz -L https://github.com/leanprover-community/ProofWidgets4/releases/download/v0.0.18/windows-64.tar.gz
error: external command `curl` exited with code 35
[2/6] Fetching proofwidgets cloud release

In VS Code, my project still works, but I get annoying messages; every time I open a file, it says that I need to rebuild imports.
It doesn't take long because they all have already been rebuild, but the message appears again and again.

[Sebastian Ullrich]

If Lean tells you dependencies need to be rebuilt when they are up to date, that's a bug. Please file an issue.

[Utensil Song]

code 35 is network issue: unknown SSL protocol error in connection

[Utensil Song]

"need to rebuild imports": I had this too, after bumping to rc3 from rc2, can't resolve after several lake exe cache get variants, resolved by deleting lake-packages and start over.

In theory this can be reproduced by bump from rc1 to rc2, get cache, build, open a project file and have some random edits, then bump to rc3, or a simplified version of the process.

[Martin Dvořák]

Has the default behaviour of convert and convert_to changed since nightly-2023-03-07 significantly? Almost all my convert and convert_to uses that didn't specify using are now broken.

[Scott Morrison]

Oof, a 7 month bump is a long time in Mathlib land at the moment. :-)

[Martin Dvořák]

I tried to bump my experimental branch from 4.2.0-rc3 to 4.2.0 and got the following error in the first file that imports Mathlib (whereäs files that import Std.Data.Nat.Basic only were fine):

`c:\Users\dvora\.elan\toolchains\leanprover--lean4---v4.2.0\bin\lake.exe print-paths Init mam.Cislo2 Mathlib.Data.Real.Basic Mathlib.Tactic.LibrarySearch` failed:

stderr:
info: [2/5] Fetching proofwidgets cloud release
info: [45/342] Building Std.Tactic.Instances
info: [66/524] Building Std.Tactic.Relation.Symm
info: [77/679] Building Std.Tactic.Relation.Rfl
info: [96/690] Building Std.CodeAction.Misc
info: [96/690] Building Std.CodeAction.Deprecated
info: [97/690] Building Std.Tactic.GuardMsgs
info: [97/690] Building Std.Tactic.Lint.Simp
info: [101/690] Building Std.Tactic.TryThis
error: > curl -s -f -o .\lake-packages\proofwidgets\build\windows-64.tar.gz -L https://github.com/leanprover-community/ProofWidgets4/releases/download/v0.0.21/windows-64.tar.gz
error: external command `curl` exited with code 35
error: > LEAN_PATH=.\lake-packages\std\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\Cli\build\lib;.\lake-packages\proofwidgets\build\lib;.\lake-packages\mathlib\build\lib;.\build\lib PATH c:\Users\dvora\.elan\toolchains\leanprover--lean4---v4.2.0\bin\lean.exe -Dlinter.missingDocs=true -DwarningAsError=true .\lake-packages\std\.\.\Std\CodeAction\Deprecated.lean -R .\lake-packages\std\.\. -o .\lake-packages\std\build\lib\Std\CodeAction\Deprecated.olean -i .\lake-packages\std\build\lib\Std\CodeAction\Deprecated.ilean -c .\lake-packages\std\build\ir\Std\CodeAction\Deprecated.c
error: > LEAN_PATH=.\lake-packages\std\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\Cli\build\lib;.\lake-packages\proofwidgets\build\lib;.\lake-packages\mathlib\build\lib;.\build\lib PATH c:\Users\dvora\.elan\toolchains\leanprover--lean4---v4.2.0\bin\lean.exe -Dlinter.missingDocs=true -DwarningAsError=true .\lake-packages\std\.\.\Std\Tactic\GuardMsgs.lean -R .\lake-packages\std\.\. -o .\lake-packages\std\build\lib\Std\Tactic\GuardMsgs.olean -i .\lake-packages\std\build\lib\Std\Tactic\GuardMsgs.ilean -c .\lake-packages\std\build\ir\Std\Tactic\GuardMsgs.c
error: stdout:
.\lake-packages\std\.\.\Std\CodeAction\Deprecated.lean:63:39: error: invalid field 'versionedIdentifier', the environment does not contain 'Lean.Server.FileWorker.EditableDocument.versionedIdentifier'
  doc
has type
  FileWorker.EditableDocument
error: stdout:
.\lake-packages\std\.\.\Std\Tactic\GuardMsgs.lean:190:36: error: invalid field 'versionedIdentifier', the environment does not contain 'Lean.Server.FileWorker.EditableDocument.versionedIdentifier'
  doc
has type
  FileWorker.EditableDocument
error: > LEAN_PATH=.\lake-packages\std\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\Cli\build\lib;.\lake-packages\proofwidgets\build\lib;.\lake-packages\mathlib\build\lib;.\build\lib PATH c:\Users\dvora\.elan\toolchains\leanprover--lean4---v4.2.0\bin\lean.exe -Dlinter.missingDocs=true -DwarningAsError=true .\lake-packages\std\.\.\Std\Tactic\Lint\Simp.lean -R .\lake-packages\std\.\. -o .\lake-packages\std\build\lib\Std\Tactic\Lint\Simp.olean -i .\lake-packages\std\build\lib\Std\Tactic\Lint\Simp.ilean -c .\lake-packages\std\build\ir\Std\Tactic\Lint\Simp.c
error: external command `c:\Users\dvora\.elan\toolchains\leanprover--lean4---v4.2.0\bin\lean.exe` exited with code 1
error: stdout:
.\lake-packages\std\.\.\Std\Tactic\Lint\Simp.lean:81:53: error: type expected, got
  (DiscrTree α : Bool → Type)
.\lake-packages\std\.\.\Std\Tactic\Lint\Simp.lean:232:43: error: unknown identifier 'simpDtConfig'
.\lake-packages\std\.\.\Std\Tactic\Lint\Simp.lean:232:71: error: unknown identifier 'simpDtConfig'
error: external command `c:\Users\dvora\.elan\toolchains\leanprover--lean4---v4.2.0\bin\lean.exe` exited with code 1
error: external command `c:\Users\dvora\.elan\toolchains\leanprover--lean4---v4.2.0\bin\lean.exe` exited with code 1
error: > LEAN_PATH=.\lake-packages\std\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\Cli\build\lib;.\lake-packages\proofwidgets\build\lib;.\lake-packages\mathlib\build\lib;.\build\lib PATH c:\Users\dvora\.elan\toolchains\leanprover--lean4---v4.2.0\bin\lean.exe -Dlinter.missingDocs=true -DwarningAsError=true .\lake-packages\std\.\.\Std\Tactic\TryThis.lean -R .\lake-packages\std\.\. -o .\lake-packages\std\build\lib\Std\Tactic\TryThis.olean -i .\lake-packages\std\build\lib\Std\Tactic\TryThis.ilean -c .\lake-packages\std\build\ir\Std\Tactic\TryThis.c
error: stdout:
.\lake-packages\std\.\.\Std\Tactic\TryThis.lean:105:43: error: invalid field 'versionedIdentifier', the environment does not contain 'Lean.Server.FileWorker.EditableDocument.versionedIdentifier'
  doc
has type
  FileWorker.EditableDocument
error: external command `c:\Users\dvora\.elan\toolchains\leanprover--lean4---v4.2.0\bin\lean.exe` exited with code 1
error: > LEAN_PATH=.\lake-packages\std\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\Cli\build\lib;.\lake-packages\proofwidgets\build\lib;.\lake-packages\mathlib\build\lib;.\build\lib PATH c:\Users\dvora\.elan\toolchains\leanprover--lean4---v4.2.0\bin\lean.exe -Dlinter.missingDocs=true -DwarningAsError=true .\lake-packages\std\.\.\Std\Tactic\Relation\Symm.lean -R .\lake-packages\std\.\. -o .\lake-packages\std\build\lib\Std\Tactic\Relation\Symm.olean -i .\lake-packages\std\build\lib\Std\Tactic\Relation\Symm.ilean -c .\lake-packages\std\build\ir\Std\Tactic\Relation\Symm.c
error: > LEAN_PATH=.\lake-packages\std\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\Cli\build\lib;.\lake-packages\proofwidgets\build\lib;.\lake-packages\mathlib\build\lib;.\build\lib PATH c:\Users\dvora\.elan\toolchains\leanprover--lean4---v4.2.0\bin\lean.exe -Dlinter.missingDocs=true -DwarningAsError=true .\lake-packages\std\.\.\Std\Tactic\Relation\Rfl.lean -R .\lake-packages\std\.\. -o .\lake-packages\std\build\lib\Std\Tactic\Relation\Rfl.olean -i .\lake-packages\std\build\lib\Std\Tactic\Relation\Rfl.ilean -c .\lake-packages\std\build\ir\Std\Tactic\Relation\Rfl.c
error: stdout:
.\lake-packages\std\.\.\Std\Tactic\Relation\Symm.lean:22:39: error: overloaded, errors
  failed to synthesize instance
    EmptyCollection WhnfCoreConfig

  invalid {...} notation, expected type is not of the form (C ...)
    WhnfCoreConfig
.\lake-packages\std\.\.\Std\Tactic\Relation\Symm.lean:26:43: error: application type mismatch
  Array DiscrTree.Key
argument
  DiscrTree.Key
has type
  Bool → Type : Type 1
but is expected to have type
  Type : Type 1
.\lake-packages\std\.\.\Std\Tactic\Relation\Symm.lean:26:43: error: application type mismatch
  Array DiscrTree.Key
argument
  DiscrTree.Key
has type
  Bool → Type : Type 1
but is expected to have type
  Type : Type 1
.\lake-packages\std\.\.\Std\Tactic\Relation\Symm.lean:43:8: error: failed to infer binder type
.\lake-packages\std\.\.\Std\Tactic\Relation\Symm.lean:43:8: error: don't know how to synthesize placeholder for argument 'α'
context:
decl : Name
x✝ : Syntax
kind : AttributeKind
declTy : Expr := ConstantInfo.type __do_lift✝
xs : Array Expr
fst✝ : Array BinderInfo
targetTy✝ : Expr
fail : MetaM Unit :=
  Lean.throwError
    (toMessageData "@[symm] attribute only applies to lemmas proving x ∼ y → y ∼ x, got " ++ toMessageData declTy ++
      toMessageData "")
val✝ targetTy rel arg✝¹ arg✝ : Expr
⊢ Type
.\lake-packages\std\.\.\Std\Tactic\Relation\Symm.lean:43:14: error: don't know how to synthesize implicit argument
  @withReducible MetaM (instMonadControlT_1 MetaM) instMonadMetaM
    (Array (DiscrTree.Key (?m.2770 decl x✝ kind __do_lift✝ __discr✝² xs fst✝ targetTy✝ val✝ targetTy rel arg✝¹ arg✝)))
    (liftM (DiscrTree.mkPath rel symmExt.config))
context:
decl : Name
x✝ : Syntax
kind : AttributeKind
declTy : Expr := ConstantInfo.type __do_lift✝
xs : Array Expr
fst✝ : Array BinderInfo
targetTy✝ : Expr
fail : MetaM Unit :=
  Lean.throwError
    (toMessageData "@[symm] attribute only applies to lemmas proving x ∼ y → y ∼ x, got " ++ toMessageData declTy ++
      toMessageData "")
val✝ targetTy rel arg✝¹ arg✝ : Expr
⊢ Type
.\lake-packages\std\.\.\Std\Tactic\Relation\Symm.lean:43:31: error: don't know how to synthesize implicit argument
  @DiscrTree.mkPath (?m.2770 decl x✝ kind __do_lift✝ __discr✝² xs fst✝ targetTy✝ val✝ targetTy rel arg✝¹ arg✝) rel
    symmExt.config
context:
decl : Name
x✝ : Syntax
kind : AttributeKind
declTy : Expr := ConstantInfo.type __do_lift✝
xs : Array Expr
fst✝ : Array BinderInfo
targetTy✝ : Expr
fail : MetaM Unit :=
  Lean.throwError
    (toMessageData "@[symm] attribute only applies to lemmas proving x ∼ y → y ∼ x, got " ++ toMessageData declTy ++
      toMessageData "")
val✝ targetTy rel arg✝¹ arg✝ : Expr
⊢ Bool
.\lake-packages\std\.\.\Std\Tactic\Relation\Symm.lean:76:4: error: failed to synthesize instance for 'for_in%' notation
  ForIn (ReaderT Context (StateRefT' IO.RealWorld State CoreM)) (?m.4446 tgt k rel arg✝¹ arg✝ __do_lift✝¹) ?m.5691
.\lake-packages\std\.\.\Std\Tactic\Relation\Symm.lean:76:4: error: invalid field notation, type is not of the form (C ...) where C is a constant
  r✝
has type
  ?m.4448 tgt k rel arg✝¹ arg✝ __do_lift✝¹ __do_lift✝
.\lake-packages\std\.\.\Std\Tactic\Relation\Symm.lean:76:4: error: invalid field notation, type is not of the form (C ...) where C is a constant
  r✝
has type
  ?m.4448 tgt k rel arg✝¹ arg✝ __do_lift✝¹ __do_lift✝
error: external command `c:\Users\dvora\.elan\toolchains\leanprover--lean4---v4.2.0\bin\lean.exe` exited with code 1
error: stdout:
.\lake-packages\std\.\.\Std\Tactic\Relation\Rfl.lean:21:39: error: overloaded, errors
  failed to synthesize instance
    EmptyCollection WhnfCoreConfig
(...)

Any idea what is wrong?

[Kevin Buzzard]

One thing that's wrong is that you're on rc3 which was one of the versions with the bug which deletes all your files and git history. Don't type lake clean.

[Mauricio Collares]

First, delete lakefile.olean to avoid the bug Kevin mentioned. Then change lakefile.lean to use mathlib revision "v4.2.0" instead of mathlib master (which currently uses Lean v4.3.0-rc1). Finally, use "lake update" to update mathlib (and therefore std4) to the correct versions.

[Martin Dvořák]

Too late. I already did lake clean at least twice. Can I nevertheless progress in the way @Mauricio Collares suggested?

[Mauricio Collares]

Kevin was telling you to avoid lake clean because it could have deleted your repository folder due to a change between v4.2.0-rc3 and v4.2.0. The way to avoid this risk is manually deleting the lakefile.olean file. If you weren't unlucky and still have your folder, you may proceed normally.

[Martin Dvořák]

Normally means the way you described above?

[Mauricio Collares]

Yes, that's what I meant. Sorry, should have been more specific.

[Martin Dvořák]

Which folder in "and still have your folder" should I check I have?

[Mauricio Collares]

The repository root. Usually contains .git, lean-toolchain, and a subfolder containing your source files.

[Mauricio Collares]

I'd assume this doesn't affect windows users, though, because deleting open files/folders is near impossible on Windows

[Dan Velleman]

Could someone explain a little more about the lakefile.olean issue? Where did this file come from? Am I supposed to delete it because it shouldn't be there at all? Or because some bug caused a flawed version of the file to be created, and I need to delete it so that a corrected version will be created?

[Mauricio Collares]

The latter. lakefile.olean is a legitimate file and it being generated is a good thing because it speeds up lake. However, versions generated by Lean 4.2.0-rc2 and 4.2.0-rc3 are incompatible with all other Lean versions (4.2.0-rc4 and later versions are compatible with 4.2.0-rc1 and former versions; just 4.2.0-rc2 and -rc3 are special). If a file generated by 4.2.0-rc2 or 4.2.0-rc3 is read by other Lean versions, lake gets confused and thinks the source directory is the build directory (leading to lake clean deleting the source directory, for example).