Deprecation without explanations

Stream: lean4

[Patrick Massot]

Trying to update MIL, I get the message:

warning: mil: package configuration option `moreServerArgs` is deprecated in favor of `moreServerOptions`

without a link to a webpage explaining how to migrate to moreServerOptions. I didn't find anything in https://github.com/leanprover/lean4/blob/master/RELEASES.md. Searching and replacing moreServerArgs with moreServerOptions does not work. This isn't the greatest UX...

[Mario Carneiro]

It's also most likely not the option you want to use, you want leanOptions

[Mario Carneiro]

what does the lakefile look like?

[Patrick Massot]

https://github.com/avigad/mathematics_in_lean_source/blob/master/lakefile.lean

[Patrick Massot]

Probably copy-pasted from the mathlib lakefile

[Yaël Dillies]

Funnily enough, the hover for moreServerArgs says instead

warning: mil: package configuration option `moreServerArgs` is deprecated in favor of `moreGlobalServerArgs`

[Yaël Dillies]

I replaced moreServerArgs by moreGlobalServerArgs and it all went well.

[Patrick Massot]

For some reason I'm not in a mood to find this funny.

[Mario Carneiro]

this is what you want now:

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

@[default_target]
lean_lib MIL where

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

[Patrick Massot]

Thanks Mario. Where did you get this information?

[Mario Carneiro]

I was involved in the change

[Shreyas Srinivas]

Breaking changes like this without a smooth transition pathway are very annoying UX-wise. I agree with Patrick. Last week alone there has been a few tactic changes, and now lake changes I have spent hours to fix these issues (and I still have some lean projects to update. Dreading this).

[Mario Carneiro]

Yaël Dillies said:

I replaced moreServerArgs by moreGlobalServerArgs and it all went well.

Don't do this. While this is the literal replacement for the old option, it causes the same issue that these new options are trying to solve (in particular the thing where opening Std from mathlib is broken)

[Utensil Song]

Particularly when it affects projects not using any variants of these options directly .

[Mario Carneiro]

yes, I'm very annoyed at this whole process, migration support in lake is really bad right now

[Patrick Massot]

Shreyas Srinivas said:

Breaking changes like this without a smooth transition pathway are very annoying UX-wise. I agree with Patrick.

A changelog entry would already be a huge improvement. A link to a webpage explaining what to change would be even better. An automatic upgrade would be paradise, but probably tricky to implement.

[Marc Huisinga]

My bad. I agree that this is confusing; it's from lean4#2858 and I should've adjusted the release notes in time before release with additional information instead of there just being a link to the PR.

[Mario Carneiro]

maybe someday we can just have json/toml/yaml lakefiles and then stuff won't break all the time :star_struck:

[Patrick Massot]

I managed to update MIL and I may even manage to be on time for my lecture if there is no traffic jam.

[Joachim Breitner]

maybe someday we can just have json/toml/yaml lakefiles and then stuff won't break all the time

Not that I am disagreeing, but lake changing the name of a field could happen just the same? That particular problem doesn't seem to be fixed by going to a declarative configuration.

[Mario Carneiro]

yes, because it's really easy to implement automatic migrations with those formats

[Mario Carneiro]

indeed lake already has migration of the lake-manifest across 7 versions

[Mario Carneiro]

with lean, if the parser changes you are screwed

[Shreyas Srinivas]

Why is lake packaged with the toolchain? What breaks if lake is separately versioned and updated?

[Shreyas Srinivas]

Is it mathlib cache?

[Mario Carneiro]

mathlib cache is separately versioned and updated

[Joachim Breitner]

It’d be possible to keep supporting moreServerArgs in addition to moreGlobalServerArgs, instead of writing

warning: mil: package configuration option `moreServerArgs` is deprecated in favor of `moreGlobalServerArgs`

wouldn’t it?

Ok, maybe the point is that it’s more annoying to have old cruft in the signature, while some code to support old fields names in a .Xml file doesn’t bother anyone.

[Mario Carneiro]

All of the options are supported

[Mario Carneiro]

not sure if there is a way to turn the warning off though

[Shreyas Srinivas]

The reason I ask is, if lake were separately versioned and updatable, then elan could manage lake updates, and lake update could check the lake version of the next package update (say mathlib) and warn users that they should run something like elan update lake first. This works ofc with one additional assumption: New lake versions can read older lake files upto some point and rewrite them into the new version.

[Mario Carneiro]

elan manages programs that are bundled with lean

[Mario Carneiro]

currently it has no support for separately versioned things or external tools, although I would really like it to

[Marc Huisinga]

To explicitly clear up some of the confusion:

• moreGlobalServerArgs is just moreServerArgs renamed, but it has the issue that it applies the options declared there to all packages, so you should typically not use it
• moreServerOptions is the direct replacement for moreServerArgs that does not have this issue
• leanOptions feeds into both moreServerOptions and moreLeanArgs, thereby eliminating the need to declare both even when they're typically the same set of options

[Utensil Song]

Lake has been progressing rapidly lately, it's doing it in a non-backward-compatible way. It has broken ABI to cause deleting the whole project, and many times it has broken existing lakefile by removing or renaming (or even adding) options (e.g. weakLeanArgs, occs, buildO signature, :=, leanOption) without a deprecation period. It also adds new features that turn out to have ramifications, e.g. lakefile.olean saving state, .lake, lake exe cache get and copying toolchain after lake update.

With all due respect, Lake indeed has become one of the most bleeding edges of Lean for end users. (Other changes will mostly cause complicated bumping PRs of Std and Mathlib, but seldom affects end users it seems)

[Mario Carneiro]

There are many programs that could benefit from that, like doc-gen and lean4export

[Shreyas Srinivas]

Shouldn't elan eventually work with reservoir?

[Mario Carneiro]

Marc Huisinga said:

• leanOptions feeds into both moreServerOptions and moreLeanArgs, thereby eliminating the need to have both at the same time

and in particular, all existing uses of the moreServerArgs option were for people setting project level options like autoImplicit=true and these should be leanOptions on the package

[Mario Carneiro]

On the topic of removed features without migration assistance, lake print-paths no longer exists on the latest version, and there is no line in the release notes about this. I'm looking at a shell script for mathport which contains this command, and am not sure what it did or what the best replacement is

[Mario Carneiro]

@Mac Malone

[Sebastian Ullrich]

Mario, didn't you review the PR that changed it? #2858
The reason it's not listed in the changelog is that it's a purely internal command, it's not even listed in lake --help

[Mario Carneiro]

It was "replaced" by setup-file with a change in functionality

[Sebastian Ullrich]

An extension of functionality

[Mario Carneiro]

The puzzle remains though

[Mario Carneiro]

this script calls lake print-paths without arguments

[Marc Huisinga]

Do you have a link to the script in question?

[Mario Carneiro]

https://github.com/leanprover-community/mathlib3port/blob/master/update.sh#L31

[Sebastian Ullrich]

Wow... that is a puzzling line

[Mario Carneiro]

I suspect that this is doing something like preparing lake's auxiliary files

[Mario Carneiro]

is there a lake nop?

[Mario Carneiro]

This doesn't build the project, right?

[Sebastian Ullrich]

lake env would be one non-internal way I think

[Sebastian Ullrich]

It shouldn't without further arguments, no

[Mario Carneiro]

Oh I think I see what this is for, it prints the paths in the CI log

[Mario Carneiro]

actually nvm it fetches oleans

target fetchOleans (_pkg) : Unit := do
  let libDir : FilePath := __dir__ / "build" / "lib"
  IO.FS.createDirAll libDir
  let oldTrace := Hash.ofString tag
  let _ ← buildFileUnlessUpToDate (libDir / oleanTarName) oldTrace do
    logInfo "Fetching oleans for Mathbin"
    untarReleaseArtifact releaseRepo tag oleanTarName libDir
  return .nil

[Mario Carneiro]

I guess this is listed as an extraDepTarget of the package so it gets run in lake print-paths

[Mario Carneiro]

I don't think lake env will run this

[Sebastian Ullrich]

An interesting puzzle indeed. Does lake build fetchOleans not work?

[Sebastian Ullrich]

But to give the most direct equivalent, lake setup-file Mathbin should not build any Lean files

[Mario Carneiro]

note that I have to wait an hour to test any change to the script so I'm making a test case instead

[Mario Carneiro]

I see that extraDep is a "facet", I assume that means I can do something like lake build mathlib3port:extraDep?

[Mario Carneiro]

huh, lake's readme does not say what the syntax of lake build <....> is

[Mario Carneiro]

lake build fetchOleans does seem to work, as does lake build :extraDep

[Mario Carneiro]

I'm going to do the former since it's a bit clearer for future mario

[Mario Carneiro]

(and it has less of a look of something that will break tomorrow)

[Marc Huisinga]

The release notes now contain a short migration guide for the Lakefile change. Sorry for the confusion.

[Mac Malone]

Mario Carneiro said:

indeed lake already has migration of the lake-manifest across 7 versions

No it doesn't? It only migrates from v5+. Second, it is just as easy to migrate declarative options across lakefiles as it is to migrate flexible declarative formats like YAML/TOML which have customizable formats/comments (it would just be a matter of reprinting the file). The manifest is easier to auto-update only because it is not meant to be edited by humans and thus does not need to preserve formatting.

[Mac Malone]

That said, I do agree that Lake should strive to be backwards-compatible at least for some deprecation period. That is why it issues deprecation warnings. If there are problems with the current deprecation approach, please report them and feel free to suggest possible solutions. I would like to make Lake upgrades more seamless.

[Mac Malone]

One thing I have noticed is that a lot of breakage comes from upgrading between release candidates or between a release candidate and a stable release. Thus, it worth noting that release candidates are not stable and it is expected for there to possibly be significant breakages between them and other releases.

[Shreyas Srinivas]

Mac Malone said:

One thing I have noticed is that a lot of breakage comes from upgrading between release candidates or between a release candidate and a stable release. Thus, it worth noting that release candidates are not stable and there is expected to possibly be significant breakages between them and other releases.

Even if this is the case, as you explained in the community meeting, there is no current option to jump only to stable releases, so the problem remains unavoidable unless one precisely times their updates.

[Mac Malone]

Shreyas Srinivas said:

As you explained in the community meeting, there is no current option to jump only to stable releases, so the problem remains.

What do you mean by this? I am sorry, but I do not recall the context for this explanation. One can certainly update Lean/Std/Mathlib to only stable releases.

[Mac Malone]

(e.g., use only Lean stable toolchains, and require the dependencies at @ "stable".)

[Shreyas Srinivas]

Back in the meeting I asked if it is possible to lake update only to stable toolchains (include deps like mathlib)

[Shreyas Srinivas]

currently lake update takes us to whatever rc happens to be latest on mathlib

[Mac Malone]

@Shreyas Srinivas Oh, sorry. I guess I was confused about the goal. I was explaining that lake update itself has no such specific option. However, if the goal is just to remain on stable toolchains, you can depend on e.g., Mathlib's stable branch instead of master.

[Shreyas Srinivas]

Thanks. This is new to me. Could this be the default setting when lake new <ProjectName> math generates a new project?

[Shreyas Srinivas]

or at least optionally so? On the vscode mathlib setup process, this would save one round of update + cache

[Mac Malone]

Good idea! Could you create an issue for that? I working on Reservoir until holiday vacation, so I will likely not get around to it soon (sorry!), so the issue will help keep it in mind. Alternatively, if you want to PR the change, I would be happy to review it! One design thought I had is might be wise to depend on stable only if we are on a stable toolchain (i.e., Lean.specialDescr is empty) and otherwise use master?

[Shreyas Srinivas]

My idea was to change the math template to have @ "stable" after the github link when new is called. Maybe add an extra command

1. lake new <proj> math stable : Generate lake file with @ "stable" for the mathlib require line.
2. lake new <proj> math latest : Generate current lakefile.
3. lake new <proj> math : Defaults to lake new <proj> math stable (or latest if there is significant opposition to defaulting to stable).

[Shreyas Srinivas]

From what I understand, lake fixes the toolchain according to mathlib anyway.

[Shreyas Srinivas]

so the initial toolchain i.e. before project creation doesn't matter.

[Mac Malone]

Shreyas Srinivas said:

so the initial toolchain i.e. before project creation doesn't matter.

True, the question is just whether a user already on a non-stable toolchain wans to be migrated to stable or just continue using whatever master mathlib is using. However, I think defaulting to the safest option is probably smartest. More explorative users can modify the lakefile themselves should they so desire. Thus, a universal default to stable seems fine.

[Mac Malone]

Adding additional arguments to the template generation would be a more significant change, and one I think would be more complicated to review (i.e., it is something I would likely need to do myself).

[Shreyas Srinivas]

I'll get on with the Issue and then PR.

[Shreyas Srinivas]

Oh okay. For now I will just change the math template to point mathlib4 dep to the stable branch by default

[Patrick Massot]

I don't think this is a good idea.

[Mac Malone]

@Patrick Massot would you like to elaborate?

[Patrick Massot]

Mathlib users typically want the latest version, not an ancient Mathlib (where ancient means more than one week old).

[Mac Malone]

@Patrick Massot Is that as true for mathlib users (i.e., people who writing a package depending on it) and as mathlib developers/contributors (i.e., those working inside the repository)?

[Henrik Böving]

I think the issue here is that the set of people that depend on mathlib is almost a subset of the people that contribute to it.

[Patrick Massot]

Yes, I meant users. Of course Mathlib developers need the master branch.

[Utensil Song]

Shreyas Srinivas said:

Oh okay. For now I will just change the math template to point mathlib4 dep to the stable branch by default

IMHO the conversation above is just like other conversations that drove lake to suddenly change its default behavior, creating new paper cuts.

If lake can add new features without immediately dropping the old behavior (the default one or the one with the same configurations), there will be less paper cuts.

[Shreyas Srinivas]

whence this suggestion. We could modify 3 to make latest the default. Of course the extension should then offer an option for creating a stable project with mathlib.

Shreyas Srinivas said:

My idea was to change the math template to have @ "stable" after the github link when new is called. Maybe add an extra command

1. lake new <proj> math stable : Generate lake file with @ "stable" for the mathlib require line.
2. lake new <proj> math latest : Generate current lakefile.
3. lake new <proj> math : Defaults to lake new <proj> math stable (or latest if there is significant opposition to defaulting to stable).

[Shreyas Srinivas]

This way the change is _slightly_ more complicated from dev end, but transparent to current users who don't care for the stable option.

[Marc Huisinga]

Of course the extension should then offer an option for creating a stable project with mathlib.

I would prefer to keep the UI for project initialization simple and not offer options that are likely to confuse new users.

[Marc Huisinga]

Someone who is new to Lean won't be able to answer the question of whether they should depend on a stable or the latest version of Mathlib.

[Shreyas Srinivas]

@Marc Huisinga : Normally I agree but there is a good reason to offer this complexity. A new mathlib user should probably stick to stable so as to not be hit by RC whirlwinds. The exception is when they are being taught by one of the experts here who keep up with the latest changes. In this case the instruction will be simple: "choose latest". Even if a student accidentally chooses stable, The expert teacher can delete the @ "stable" bit and run lake update and everything is hunky dory.

Since there is debate for now, I'll create the issue when the dust is settled and I have some spare time again.

[Shreyas Srinivas]

If the new users are not well-versed in lean to understand the latest changes in the RC and also not being guided by say @Patrick Massot or @Kevin Buzzard, then they could be playing with fire (specifically lake update here, but also something like the 4.1.0 rc1 - 4.1.0-rc2 issue, which was far more severe)

[Utensil Song]

Maybe only teaching projects will depend on stable Mathlib, formalization projects is more likely to need the latest Mathlib with many PRs merged every day. I also can't think of any other projecrs that use Mathlib would have chosen stable.

Waiting for a stable release to avoid paper cuts, is not an approach that scales.

[Shreyas Srinivas]

teaching is where you want to have the least setup trouble.

[Shreyas Srinivas]

also can't think of any other projecrs that use Mathlib would have chosen stable.

I can. My projects will sail along perfectly well without Mathlib's latest updates, except maybe once in a while when some nice tactic like the inequality rewrite one or omega lands or there are some nice new inequalities or norm_num extensions.

[Patrick Massot]

My experience with teaching using Lean 4 so far is that nothing can save students. It's amazing how they are able to screw up things. Many times I was only able to tell them to restart from scratch creating a project. I have no idea what they are doing.

[Henrik Böving]

Dont worry patrick, this behavior is not limited to students :P

[Utensil Song]

If nightly Lean has frequent paper cuts, that's understandable for rapid progressing. If this is frequently happening to release candidates which Mathlib is using it as a semi-stable base, this is far from ideal, and a practice far from normal software release model. When this is happening to a theorem prover that is expected to be used to prove math and build reliable software, the frustration of users is understandable. And when these issues affecting many active users are not mentioned (not the issue, and not how it's fixed or replaced with something else unexpected) in release notes, but only scattered in Zulip chats, it's probably not the best way to handle this.

[Shreyas Srinivas]

Utensil Song said:

If nightly Lean has frequent paper cuts, that's understandable for rapid progressing. If this is frequently happening to release candidates which Mathlib is using it as a semi-stable base, this is far from ideal, and a practice far from normal software release model. When this is happening to a theorem prover that is expected to be used to prove math and build reliable software, the frustration of users is understandable. And when these issues affecting many active users are not mentioned (not the issue, and not how it's fixed or replaced with something else unexpected) in release notes, but only scattered in Zulip chats, it's probably not the best way to handle this.

I get the frustration. I have it too. Last week it was simp and norm_num. This week it is lake update. But your reasons are also precisely why it makes sense for unguided new users to jump only from stable to stable.

[Utensil Song]

I just read https://github.com/leanprover/lean4/commit/7ff7cf9b5a7246d584a4b31fad35feb72ce1adf8 and realized it has a perfectly well written commit log, explaining every change in detail, and a proper deprecation period seems to exist. May the issue is even if lake is only adding new features, toolchain inconsistency could still cause issues, and end users don't really have a reliable way to avoid it or figure out how to get back to normal. The safety tip and warning regarding what's potentially dangerous is quickly changing in the last few weeks. I miss an experience writing rust, if I have done something wrong or I triggered an edge case that's still being discussed and fixed, in the error message, it's explained to me succinctly, with a simple tip to fix, and a link to the issue tracking the patch.

[Utensil Song]

Shreyas Srinivas said:

I get the frustration. I have it too. Last week it was simp and norm_num. This week it is lake update. But your reasons are also precisely why it makes sense for unguided new users to jump only from stable to stable.

It's possibly safer for status quo, but it's far from ideal for the long run, especially with many active user that needs Mathlib master are also the ones that probably never would be guided enough to avoid undefined behavior when API/API changes without a smooth migration process. A jump between stable releases could involve even more little details to migrate, facing a combination of various issues that need more rounds of exchange on Zulip as long as the current practice doesn't change.

[Mac Malone]

Utensil Song said:

I just read https://github.com/leanprover/lean4/commit/7ff7cf9b5a7246d584a4b31fad35feb72ce1adf8 and realized it has a perfectly well written commit log, explaining every change in detail, and a proper deprecation period seems to exist.

Yes, I believe, at least in this case, the problem is not a lack of information existing or being noted in the release notes, but rather an issue of discovery and highlighting.

Utensil Song said:

May the issue is even if lake is only adding new features, toolchain inconsistency could still cause issues, and end users don't really have a reliable way to avoid it or figure out how to get back to normal.

Another issue is that we don't know exactly what behaviors users are relying on, so it is easy to make a change which we believe should be non-breaking (like the change in the internal lake print-paths command) and still break some unknown edge case that is depending on it.

Utensil Song said:

I miss an experience writing rust, if I have done something wrong or I triggered an edge case that's still being discussed and fixed, in the error message, it's explained to me succinctly, with a simple tip to fix, and a link to the issue tracking the patch.

Currently Lean/Lake error messages/warnings are often very succinct, which in my experience is rather standard for developer software. Now that is not to say it is necessarily best practice. For example, I know debugging error messages is often a pain point for students and other new users. Thus, if more verbosity and hyperlinks to reference documentation would help, that might be a good style change to apply to future deprecation notices and new or revamped error messages.

[Mac Malone]

Utensil Song said:

If nightly Lean has frequent paper cuts, that's understandable for rapid progressing. If this is frequently happening to release candidates which Mathlib is using it as a semi-stable base, this is far from ideal.

Yes, it appears to me that the underlying problem here is that Mathlib users are relying on release candidates and this creates the expectation that they will be semi-stable, which is not the intent. Neither is it really possible since the release candidates are the vector by which we aim to quality test a beta version of Lean to ensure the final version is widely stable.

[Mac Malone]

The conundrum is that we need some representative sample of the community to be using nightlies and/or release candidates to beta test them to ensure that the resulting stable is, in fact, stable for the rest of the community. The problem is that if too many people are on the release candidate, then there is no split. On the other hand, if there are too few, more unanticipated breakages will arise.

[Mac Malone]

The hope behind the mathlib master / stable split was that master being on a release candidate would give us feedback on how to properly ensure the stable is stable via the Mathlib developers while allowing new Mathlib users to stay on the then well-tested versions via stable.

[Mac Malone]

An issue appears to be that Mathlib wants to follow an essentially nightly release model with frequent breakage while not expecting to rely on a Lean doing the same. Or, at least, that is my takeaway from this:

Patrick Massot said:

Mathlib users typically want the latest version, not an ancient Mathlib (where ancient means more than one week old).

[Floris van Doorn]

I think using stable for mathlib is fine if it is actually somewhat more stable than master. Is it more stable though? My understanding of the current workflow is that the lean version is a bit more stable, but mathlib is still just on an arbitrary commit that is (on average) equally buggy as master.

If we had a stable branch that has no new "features" but only "bug fixes" for a period of time (whatever "feature"/"bug fix" means exactly in the context of mathlib), I think that would be the preferred default. However, creating/maintaining such a branch sounds nontrivial (I'm not volunteering).

I'm saying that I would prefer stable instead of master, because when I updated my Lean course repo to use v4.2.0 the exists-delaborator suddenly broke (fixed in #8070), which is also annoying.

[Mario Carneiro]

Mac Malone said:

Utensil Song said:

I miss an experience writing rust, if I have done something wrong or I triggered an edge case that's still being discussed and fixed, in the error message, it's explained to me succinctly, with a simple tip to fix, and a link to the issue tracking the patch.

Currently Lean/Lake error messages/warnings are often very succinct, which in my experience is rather standard for developer software. Now that is not to say it is necessarily best practice.

Yes, that's a nice way to say that error reporting in most software is terrible. The key difference with rust error messages is that they are written from the user's perspective, not the developer's. The idea is that you think about how the user could possibly have arrived at this error condition and explain the steps needed to get back out, because this is the information that is valuable to them, rather than (or in addition to) explaining what the error is, which is most direct but very high-context and will likely be impenetrable to the user. (Famous lean examples of bad error messages include motive is not type correct and failed to synthesize instance.)

[Mac Malone]

Mario Carneiro said:

The key difference with rust error messages is that they are written from the user's perspective, not the developer's.

Yep, the aim is different.

[Shreyas Srinivas]

Shreyas Srinivas said:

Oh okay. For now I will just change the math template to point mathlib4 dep to the stable branch by default

What is the consensus on this? I see two :+1: s and two :-1: s

[Shreyas Srinivas]

Alternatively, what is the consensus on the more transparent version of the change I proposed that leaves current users unaffected, which will however take up more time dev and review-wise

[Utensil Song]

Adding the feature of having a way to generate stable dependency on Mathlib and Lean is probably not :-1: are disagreeing. The issue is the development/release model of changing existing behavior that unknown number of people might be depending on or expecting.

Of course, developers can't predict all ramifications of a change, but it's reasonable to assume all changes might break something then proceed with a more stable release model (even for rc or nightlies), let's call it flag-verify-link: new potential breaking change (renaming options, directory, even the ones considered internal details) provides a flag or that can be enabled per project; if it's enabled, it'll verify the environment and assumptions it make and errors if something unexpected happens; the error comes with the link to the PR where people can read the change description, possibly a migration guide. This is an analogy to what Rust nightly did with feature gates/rustc explain, I was never really cut or left puzzled by its nightly. This document (UPDATE: see the better link below) explains the mechanisms it uses to help keeping nightly reasonably stable because it's trying to live up to be a "safe" programming language, which is also somewhat expected from a theorem prover/general purpose programming language.

[Utensil Song]

"Safe" for tooling means downstream projects have control over keeping existing tooling behavior while enjoying latest application level features (e.g. Mathlib features).

So, as a user, I would insist to expect I can have both a "safe" tooling and a latest Mathlib, not that I should give up the latter so I can stay safe with the tooling.

Personally, I expect this for better use of my Lean time, and for the experience of people that I would recommend Lean to.

[Utensil Song]

Being "safe" doesn't mean the rc/nightly tooling never break, but it breaks in a way that can be mitigated by a small group of predictable simple steps that everyone can learn after reading something no more than half-screen-length, and use the same trick for like a few months. Or just resolve it with the guide came with the error message.

[Utensil Song]

It also means users don't need to immediately pay for the potential breakage of a new change, e.g. it's OK to see lake warns about it's going to change build to .lake as its default behavior while keep using build so users can adapt their CI to that when they have time for that. This is the opt-in model.

Or even if lake has changed build to .lakedirectly, but warns about this change and tells the user about how to keep using build (opt-out) or migrate the CI, it's still an almost smooth (i.e. not frustrating) experience.

[Mario Carneiro]

note, your link is about unstable features in rustdoc, not unstable features in rustc (although the basic ideas are similar)

[Utensil Song]

Thanks, the better link seems to be 16. Procedures for Breaking Changes and also 11-14 for new features, which covers feature gates, deprecated attribute, issuing future compatibility warnings etc.

[Mac Malone]

Utensil Song said:

This document explains the mechanisms it uses to help keeping nightly reasonably stable because it's trying to live up to be a "safe" programming language, which is also somewhat expected from a theorem prover/general purpose programming language.

I think one key detail that may be missing here is that Lean is not yet in its v1.x phase like Rust is. The current state of Lean is much closer to v0.x Rust. The language is still missing a number of key features before it is at that level. The point of our "stable" releases is to provide some level of quality assurance above and beyond the previous nightly releases, which were only verified by the Lean 4 CI and could arbitrarily break literally anything without notice. Now we are the point were we are tracking breaking changes and notifying about them, but still not in the realm of providing any strong guarantees about compatibility going forward.

[Mac Malone]

In other words, the stability guarantee of Lean stable releases is about quality assurance of the release itself (i.e., any major damage like deleting important files has hopefully been caught during the release candidate process). However, it is not providing any strong guarantee of stability across releases.

[Utensil Song]

Thanks for the explanation. I'll save these hopes for the long run. With reservoir, tracking the impacts to downstream projects would be easier, I guess, provided that there's a CI for nightly besides rc.

[Mario Carneiro]

I'm not sure all parties are on board with that definition of "stable"

[Shreyas Srinivas]

1. Lean isn't where rust was even in 2016, though lean will hopefully get there sooner than later. I agree with you that changes shouldn't break anything if they don't have to. Updates should be more careful.
2. There is always a trade off between having the latest features and not risking breaking anything (stable). You can't have both. It is really one or the other with some reasonable trade off.
3. There is a way to make this particular change such that current users don't notice a thing other than maybe one new option on the vscode menu
4. The notion of stability is a relative one. Stable doesn't mean nothing will break. It just means there has been more beta testing with RC releases to find catastrophic issues.
5. As Floris says, Mathlib doesn't have a notion of stability yet. So features and breakages could also come from there (in the form of tactic changes or API changes). I am not aware of any public announcements about any plans to have a more stable release schedule for Mathlib either (although scalability issues and frustrations will eventually make this unavoidable).

So why is this request coming up? Not all of us work on the latest bleeding edge of mathlib, and we don't want to be caught every week in a new debugging situation, because some breaking change was pushed through. The RCs do imply a comparatively higher chance of breaking things. If you are a new user or someone who isn't working on mathlib's bleeding edge features, and isn't working with one of the experts here, there is a fairly good chance that getting bitten by these rapid and breaking updates will discourage you from using lean. This includes all the people who may not feel comfortable posting on zulip for help

[Shreyas Srinivas]

@Mac Malone : I think I should hold off for now on making a PR until the community agrees on something. I wonder if posting an RFC issue would be a better option for now, as a reference point for discussions. This conversation is bound to happen again sooner or later, and multiple times.

[Mauricio Collares]

Presumably people run lake update when they want some new feature that landed in mathlib. Is there any other use case for it? For this use case, tracking stable seems bad: you see a new commit you like, and then you have to wait up to four weeks to have it.

If you're updating for no reason other than to stay on top of the new changes, then it also seems bad because you're getting four weeks of breakage at once, whereas upgrading weekly would probably be less painful since things are rarely reverted. (By the way, upgrading unnecessarily seems like a waste of time, but I sympathize with it because I'm also very prone to doing it.)

I guess my (perhaps unpopular) point is: Staying up-to-date is a virtue only when security updates are involved. Otherwise, the best allocation of time is to upgrade only whenever there is a compelling reason to.

[Shreyas Srinivas]

The goal of updating to stable is to avoid the experimental changes in RCs that get reverted or fixed by the next release

[Shreyas Srinivas]

It also makes sense to update from time to time so that one doesn't land up in a situation of having to go through six months of updates when a critical change arrives, or when you want to have a reasonable chance of eventually using new features with the least possible update friction

[Scott Morrison]

Note that rather few of the breaking changes being made in Lean ever get reverted during the release candidate process. I think at this point, better than encouraging users to delay updating (i.e. by staying on stable), which then makes for more difficult bigger bumps, we should be thinking about ways to make it easier for users to update often (i.e. every new RC). I hope this is something Reservoir will help with, by giving us the information about projects which would be able to moving to a subsequent RC without breakage.

[Mario Carneiro]

I think we should be focusing more on migration as a mechanism for keeping things working rather than stability in the settling-down sense

[Mario Carneiro]

If we could just press a button and automatically upgrade the project I don't think this would be an issue

[Mario Carneiro]

plus, migrations stack much better, since you can just apply them in order and support as long a time horizon as you want

[Utensil Song]

I +1ed for both ideas because I think they are orthogonal, and both valid.

One can observe that rc versions are becoming more frequent lately, which is a great thing (Many thanks! Particularly Scott's work on Std/Mathlib side to bump and fix issues) for getting back to normal if a user hit an issue. This is definitely better than persuading people to stay on an ancient stable version of Lean. This is usually an non-option for the people who just see what they need landed into Mathlib or Std after days or weeks, and the feature is relying on the latest Lean, but then they are told, for their safety, they need to wait for a few more weeks until it's made sure there is no paper cuts.

One fruit from this thread that I hope is the migration mechanism Mario mentioned. This thread will be all for nothing, if this thread only ends in more and more explanations about why thing is how it is now (that Lean is nowhere near Rust back in 2016), or a tip for people to stay away from the latest Lean because there are no (more) railguards planned in this stage yet.

[Mac Malone]

Utensil Song said:

This is definitely better than persuading people to stay on an ancient stable version of Lean.

Calling a month "ancient" would be quite a surprise in essentially every other language release schedule. Furthermore, it is entirely unclear to me how one could ensure a level of release stability (non-breakage) without some preview time (a month max is already rather short for that). We have already had some critical failures in release candidates in the past, and it seems very desirable to steer new users away from such possible bad impressions.

[Mac Malone]

Hopefully, Reservoir will allow us to detect package breakages across the ecosystem from an RC (or nightly), which will help with writing release notes and smoothing the transition into a new version. But even that process will take some time post-release to hammer out, so there still needs to be a test window.

[Utensil Song]

Mac Malone said:

Hopefully, Reservoir will allow us to detect package breakages across the ecosystem from an RC (or nightly), which will help with writing release notes and smoothing the transition into a new version. But even that process will take some time post-release to hammer out, so there still needs to be a test window.

Preferably nightly, then a better chance of finding out before RC. But if Reservoir fixes its CI according to the change, then it would still be missing the opportunity to know how wide the impact to downstream projects.

[Utensil Song]

I'm particularly confused by why additive changes to lake (e.g. adding leanOption) with a normal migration step (e.g. lake update) will still causing breaking on the user side e.g. this thread about breaking the auto-update of lean4web instances on possibly live.lean-lang.org. (Not technically, but the release model as a whole)

Is there a safer migration step to avoid additive changes (which should not be breaking traditionally) become breaking changes ?

[Utensil Song]

Utensil Song said:

I +1ed for both ideas because I think they are orthogonal, and both valid.

One can observe that rc versions are becoming more frequent lately, which is a great thing (Many thanks! Particularly Scott's work on Std/Mathlib side to bump and fix issues) for getting back to normal if a user hit an issue. This is definitely better than persuading people to stay on an ancient stable version of Lean. This is usually an non-option for the people who just see what they need landed into Mathlib or Std after days or weeks, and the feature is relying on the latest Lean, but then they are told, for their safety, they need to wait for a few more weeks until it's made sure there is no paper cuts.

One fruit from this thread that I hope is the migration mechanism Mario mentioned. This thread will be all for nothing, if this thread only ends in more and more explanations about why thing is how it is now (that Lean is nowhere near Rust back in 2016), or a tip for people to stay away from the latest Lean because there are no (more) railguards planned in this stage yet.

This message is meant to explain why staying on stable is a non-option for many (that are not the intended fewer people for RC test window), particularly for users who need the latest features. Using "ancient" and triggering a reply only on this word is not the intention, the word is only measuring the PR count (just see how many commit messages in the rss channel per day ) that one will lose if staying on Lean stable. These PRs are not only providing new features, it also fixes issues, and changes the idiomatic way to do things, they will render many downstream code (e.g. working around the issue, write proofs in the old way) based on the older version obsolete quickly. Even if we distribute that number by math areas, the more active a math area is, the PRs change things more frequently.

In all these PRs, there will be a few PRs are not about any specific math area, but about Lean changes, the consequences of these changes. Mathlib can't afford to maintain a branch that cherry-pick these changes out, leaving only the changes users actually need. This will bind the new features to the latest Lean version. One can't stay to a stable Lean weeks ago without losing some features they care about landed into Mathlib days ago. The tension between them builds up.

At any rate, my point is not against telling the ones who are willing to stay on stable Lean to stay on stable Lean, but this is not a solution to others who can't afford to stay on stable Lean, but hopes to spend less Lean time on debugging technical details like file paths, option names etc. that they don't care about or have knowledge about.

Whether Mathlib has a stable release model is irrelevant here. Breaking in Mathlib, like a tactic failing on edge cases, annoying as it might be, but at least it's something that interests the audience (even a new math user will expect to be able to understand how tactics work, and these failing cases can provide case studies into the the understanding of how they work, so do the workarounds). They are in stark contrast to the breaking changes in lake.

[Shreyas Srinivas]

I get that you want a stable lake and a constantly up to date mathlib. But I also believe this an unrealistic expectation in the short run.
: It is a "you can't have your cake and eat it too" kind of situation. Lake development happens in parallel with the rest of the ecosystem and also in response to mathlib's needs. What Mario and Mac suggest, migrations and stable releases, are the best long term option. You can't get 0-breakages without some real world testing. 1 week is too short a time window for that. I suspect we will know more once reservoir is out. But fwiw, my suggestions don't preclude working with mathlib's latest version in any sense.

[Utensil Song]

Not a stable lake, an easily migrate-able lake

[Mario Carneiro]

Mac Malone said:

Utensil Song said:

This is definitely better than persuading people to stay on an ancient stable version of Lean.

Calling a month "ancient" would be quite a surprise in essentially every other language release schedule.

I'm sure this was a joke but it's also kinda true. Keeping up with changes in lean is a full time job.

[Mario Carneiro]

Utensil Song said:

I'm particularly confused by why additive changes to lake (e.g. adding leanOption) with a normal migration step (e.g. lake update) will still causing breaking on the user side e.g. this thread about breaking the auto-update of lean4web instances on possibly live.lean-lang.org. (Not technically, but the release model as a whole)

Is there a safer migration step to avoid additive changes (which should not be breaking traditionally) become breaking changes ?

I talked to @Mac Malone about this and we agree that this should not have been a breaking change and we want the facility to add new options in the future without causing similar breakage. We floated two (non-exclusive) solutions to this: (1) Make the package macro ignore unknown options instead of erroring. This would make adding an option non-breaking. (2) Use the proposed trackToolchain option to allow users to opt in to the toolchain copying behavior, so that we don't use old lake to process a new lakefile. This should avoid all instances of this issue, although only for toolchain-tracked dependencies (for most projects that would be std or mathlib).

[Utensil Song]

That's great news, both sound very reasonable, thanks! Will there be 2 issues to track them?

[Yaël Dillies]

What's proofs.withType in this new paradigm?