feat: heuristic selection of lean4web project by version string

[jcreedcmu]

Presently, one can select which "project" is used with the URI fragment, e.g.

https://live.lean-lang.org/#project=mathlib-stable

When another webpage somewhere on the internet makes a link to https://live.lean-lang.org/ with some particular codez, it could name a particular project to run with, but the version of lean specified in that project's lean-toolchain changes over time. It could happen that the lean code would be valid on one date, and silently become invalid as lean4web upgrades its projects' lean version.

It would be useful if there was a way for a link to specify that it intends its code to be run at a fixed version of lean, e.g. v4.123.0. Something like

https://live.lean-lang.org/#version=v4.123.0&codez=...

might look through the available projects and find one that matches the version given. In the event that no such project exists, lean4web might choose an arbitrary project, and display some kind of warning, informing the user that their code might still work on the current version, but that they shouldn't be surprised if it doesn't, and point them perhaps at release notes or whatever other documentation might help them figure out how to migrate it to be valid at more recent versions of lean, or to install an older version on their own machine, or the like.

This feature would be particularly useful for lean reference documentation, because then we could publish versions of the documentation (each one knowing which version it is) to https://live.lean-lang.org/ that would "age gracefully" without needing their URI to change.

[jcreedcmu]

As of now, we have a mechanism for automatically adding links to Live for every example-block in the lean language reference, such that when the manual is deployed, only versions of the manual that are compatible with supported projects have links. However, @kim-em pointed out that there are some other bits of narrative text (for example, this file does so twice) that directly link to Live, and this issue would be still useful for them if they could advertise which version of lean they expect to work at.

[joneugster]

Jason, why don't you just add one project per version to the live.lean-lang.org instance, named e.g. lean-v4.23.0 etc. and then you point your links directly at the relevant project?

I think you cansimply choose not to add these projects to the dropdown to keep that short and clean.

I'm not sure that it would be desirable to switch projects automatically. For example if I specify the duper project on a wrong version, it's no good if the editor chooses plain lean in the right version as duper is not installed there.

[joneugster]

It would be a nice and easy to implement feature IMO to add the version=4.23.0 and always display a warning when the project's toolchain doesn't match the specified version. Something like

Warning: the link was intended for Lean version v4.20.0 but the web editor runs on v4.23.0. It's possible that the code broke or evaluates differently than when the link was created.

[jcreedcmu]

Now that you mention it, I do like the idea of making the selection process more predictable and not heuristic. But I also would ideally like to not make the process of upgrading our instance of lean4web any more complicated than necessary each time we release a new version. It would be nice if we didn't have to change client/src/config/config.tsx frequently, but maybe what you have in mind already doesn't require that. I'm not sure I've thought this through all the way.

The main thing I'd like is for a situation somewhat like the following to be possible:

Both
https://lean-lang.org/doc/reference/latest/
https://lean-lang.org/doc/reference/4.25.0-rc/
have exactly the same content, and they have some links of the form
https://live.lean-lang.org/#version=4.25.0-rc2&codez=IYZwJgZkA...etc.
and if you click on them today they work, and in the future, they might display something like your Warning above.

Both
https://lean-lang.org/doc/reference/stable/
https://lean-lang.org/doc/reference/4.24.0/
have exactly the same content, and they have some links of the form
https://live.lean-lang.org/#version=4.24.0&codez=IYZwJgZkA...etc.
and if you click on them today they work, and in the future, they might display something like your Warning above.

The crucial thing that would be convenient is for the link to not have to know anything about the current status of whether its fixed version number currently is latest or stable. Maybe we do have to pay the price of some configuration data on the lean4web end managing the mapping that has information like "as of today, the best match for version=4.24.0 is using Projects directory MathlibLatest" or something like that.

[nomeata]

Small suggestion, but if you do add something like this, call it toolchain, not version. This way there is no confusion about lean4web versions or mathlib versions etc.

That said, I see no problem with our updater script looking at releases.lean-lang.org and creating a project for every stable release, so that project=lean-v4.42.0 works. I often wanted that myself to easily bisect bug reports.

[nomeata]

I would push back on heuristics trying to find a “better” project and suddenly using a mathlib project when it originally used a plain lean project. That seems too bad hoc.

[nomeata]

Creating these projects dynamically seems easy. Adding them to the config a bit more tedious. Maybe lean4web could (or does it already) support non-listed projects for every directory in the project folder, even without explicit mention in the configuration?

Ah, reading the code that already seems to be the case. So things are easy then, aren't they?

[jcreedcmu]

I like the specificity of toolchain= instead of version=, and I agree that both the UX and DX seems good of lean4web offering a small number of explicitly listed versions in the popup, and allowing config.tsx to not need to change every version update. I don't know enough to be sure that creating the projects dynamically is easy, but I'm inclined to take your word for it.

Likewise I'm not sure I fully understand the disadvantages of using a project that has a dependency on mathlib for a matching-toolchain example that never even says import Mathlib. Is the concern performance? I agree that's a valid concern, but I'm curious if there are others I'm missing.

[jcreedcmu]

Actually, no, maybe I do see after looking at the updater script in
https://github.com/leanprover/fro-infra/blob/master/machines/live/live.nix
that it shouldn't be very hard to create all the directories appropriately.

[jcreedcmu]

Is there a reason why you specifically say "creating a project for every stable release" rather than "creating a project for every release (including rcs)"? If we did the latter then every published version of the reference manual could have links.

[nomeata]

that it shouldn't be very hard to create all the directories appropriately.

Already on it

Is there a reason why you specifically say "creating a project for every stable release" rather than "creating a project for every release (including rcs)"? If we did the latter then every published version of the reference manual could have links.

No, not really. It really only costs a bit of extra disk space, and that’s cheap. Given that elan caches toolchains, not even the update script will be much slower.

[jcreedcmu]

Terrific, thanks

[nomeata]

Here we go:

https://live.lean-lang.org/#project=lean-v4.20.0&codez=MQNwpgTgzglg9gOyA

There is still an issue with old versions that don’t support experimental.module yet…

Feature requests:

• Recognize when the project does not exist, and give a proper error message
  (And in general if the backend doesn’t come up, e.g. if the bubblewrap script fails)
• In the frontend, if a project is given in the URL, add it to the drop down and show it, else the project selector shows a wrong value

[nomeata]

Ok, fixed that one as well, so now

https://live.lean-lang.org/#project=lean-v4.0.0&codez=MQUwbghgNgBAMiCA7AdGEAnAzgSwPZIDKALhjkgOZA

works as well

[nomeata]

RCs are being installed as we speak, so I think we are good here (up to the usability feature requests above about non-configured projects)