update to 4.9.0 problems

Stream: new members

[rzeta0]

so I saw the announcement that Lean 4.9.0 is out.

I asked on social media all I had to do was update the lean-toolchain file from
leanprover/lean4:v4.9.0-rc1

to
leanprover/lean4:v4.9.0

I was advised as follows:

1.for the default active lean toolchain elan update.

2. To update a project managed by lake, cd into it, run lake update.

elan update worked by lake update didn't

So the further advice was:

Troubleshooting tips:

1. If lake complains about something (usually manifests or syntax changes in lake's configuration files), delete the file lake-manifest.json and the build folder named .lake
2. If that fails, ask for help* on the very active leanprover.zulipchat.com

However this didn't work. So I deleted the entire folder and restored it from my GitHub backup which only brings down the lean-toolchain file (now updated to 4.9.0) and the lakefile.lean file.

Trying to open a lean file gives the following error:

`/Users/tariq/.elan/toolchains/leanprover--lean4---v4.9.0/bin/lake setup-file /Users/tariq/Desktop/Lean-First-Steps/04_algebra.lean Init Mathlib.Tactic --no-build` failed:

stderr:
info: leantest: no previous manifest, creating one from scratch
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '././.lake/packages/mathlib'
trace: .> git clone https://github.com/leanprover-community/mathlib4.git ././.lake/packages/mathlib
trace: stderr:
Cloning into '././.lake/packages/mathlib'...
error: ././.lake/packages/mathlib/lakefile.lean:21:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean:22:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean:23:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean:24:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean:25:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean: package configuration has errors
Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file.

Any tips?

[rzeta0]

I should say I use Visual Studio Code and the Lean extension on macOS, all of which are auto updated as far as I can tell.

[Mario Carneiro]

you are trying to use 4.9.0 to compile latest mathlib, which is on 4.10.0-rc1. You should either use the stable branch of mathlib in your lakefile, or update your lean-toolchain to 4.10.0-rc1

[Mario Carneiro]

(Note that mathlib usually bumps to the first RC of the upcoming version immediately after a stable release)

[Mario Carneiro]

concretely, you should edit your lakefile to contain:

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.9.0"

[Mario Carneiro]

or

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "stable"

[rzeta0]

hi Mario - I appreciate your help, thanks.

This lakefile.lean is automatically recreated by the lean4 VSC extension? Is that correct?

Pointing to the next RC seems like the wrong default behaviour. Surely most users would want a stable/latest release install - and only the developers or experts would want to be working on an RC?

The important question for me is that if I want other beginners to clone my GitHub repo of lean example files do I need to ensure the @ "4.9.0" in the lakefile.lean file so that their experience is as smooth as possible?

Question for the developers - if lean-toolchain points to 4.9.0 surely we shouldn't have lakefile.lean try to pull down an RC?

[Shreyas Srinivas]

Given how fast the lean ecosystem continues to move, there are a lot of good reasons to continue with RC being the default. There is a tradeoff between having a smooth experience and keeping up with great changes and sometimes breaking ones. For example, with 4.9.0 there is incremental compilation, some nice changes to the omega tactic, and a breaking change with type inference in have statements among others.

[Shreyas Srinivas]

A reasonable trade off it to use the "stable" branch option Mario mentioned above

[Shreyas Srinivas]

Roughly you have a new stable release every month

[rzeta0]

If I'm creating a set of resources for people to use in the coming months and even years - is the advice to pin to a specific version eg 4.9.0 or can I depend on "stable" being backwards compatible?

[Shreyas Srinivas]

Although the language is most likely not going to change substantially, one shouldn't expect backward compatibility as a given, particularly for tactic mode and library Def/theorem names. Sometimes the changes are additive so nothing breaks with updates. When there are breaking changes, the release notes specify how to handle them. Of course, one option is to simply pin your project's lean version for a longer time and have a slower update cycle for your resource, at the risk of having bigger breakages with each such update.

A slight aside: If you provide a gitpod/codespaces setup in your project, then users will be able to spin up your GitHub repo

[Shreyas Srinivas]

So they won't have to deal with any of these breakages and updates

[Eric Wieser]

Users don't have to deal with updates anyway unless they decide they want to update your package for you

[Shreyas Srinivas]

"stable" has two different meanings in this context:

1. As far as the lean toolchain is concerned (i.e. language + lake +Std) it means the release is more bug free than the release candidates where issues get ironed out
2. For mathlib and batteries, stable just means that they were built with the corresponding stable lean toolchain version

[Shreyas Srinivas]

Eric Wieser said:

Users don't have to deal with updates anyway unless they decide they want to update your package for you

Then it could become rapidly out of date as a learning resource.