Lean 3 extension name

Stream: lean4

[Floris van Doorn]

I just noticed that the Lean 3 VSCode Extension is called lean. Can we rename that to lean3, so that it looks less like the default Lean extension?

[Patrick Massot]

I think that obsolete_lean would be even clearer. Hopefully we are converging towards a situation where people won’t need to see a number to understand when we talk about Lean 4.

[Eric Wieser]

I think that changing the name might cause breakage, but we could certainly change the displayName and description

[Eric Wieser]

https://github.com/leanprover/vscode-lean is archived, so we cannot change it

[Eric Wieser]

I've made the fix at https://github.com/eric-wieser/vscode-lean/commit/8c6dc5c436cb670d5ab5d7ff9eab071e5025c1ce, but can't PR it

[Eric Wieser]

@Marc Huisinga, would you be able to unarchive the repo when you get back from vacation?

[Marc Huisinga]

Unfortunately, the tricky part here is actually publishing the Lean 3 VS Code extension, since it stopped building long ago due to an issue with some dependency. The only way to still update that extension is to patch an existing VSIX.

Personally, I think the description below the name is sufficient to designate it as the Lean 3 extension:
image.png

However, it is very unfortunate that when searching for lean in the extensions menu, lean is shown first, then a bunch of other extensions and only then the lean4 extension. I wonder if changing the display name of the Lean 4 extension to include a space could improve this situation, since I think this search is using a fuzzy matcher that prefers full words over word substrings.
Since the build is broken and it is entirely unmaintained, I also plan to unpublish the Lean 3 extension in a couple of months so that it can only be installed from a VSIX file (e.g. the one attached to https://github.com/leanprover/vscode-lean/releases/tag/v0.16.59).

[Shreyas Srinivas]

@Marc Huisinga : this will break people's old lean3 projects which can be opened in gitpod for now

[Shreyas Srinivas]

This could include code which was published with papers. Gitpod and codespaces currently use marketplace extensions

[Marc Huisinga]

You can easily install extensions from VSIX in Gitpod.

[Eric Wieser]

Not if you're reading a paper that says "click this gitpod link to have everything set up for you", then it transpires that actually you have to find this zulip thread to realize that you have to install the VSIX manually

[Eric Wieser]

since it stopped building long ago due to an issue with some dependency.

I guess pinning to the old dependency version doesn't help due to some incompatibility with vscode?

[Marc Huisinga]

Eric Wieser said:

since it stopped building long ago due to an issue with some dependency.

I guess pinning to the old dependency version doesn't help due to some incompatibility with vscode?

The dependency is pinned. Attempting to build the extension results in some inscrutable error that Google yields no results for.

Eric Wieser said:

Not if you're reading a paper that says "click this gitpod link to have everything set up for you", then it transpires that actually you have to find this zulip thread to realize that you have to install the VSIX manually

To be clear, with the way things are now (the Lean 3 extension being both unmaintained and unbuildable), it is only a matter of time until the Lean 3 extension breaks entirely for new VS Code versions, since VS Code frequently breaks backwards compatibility in subtle ways. If you have a suggestion to resolve this, please let me know.
Outside of vscode-lean, the last time I tried to build an old Lean 3 project, I couldn't get it to work without adjustments because of the redirect issue.

As far as I can see (and as unfortunate as that is), the only way that you can be sure to get a working build for old Lean 3 projects is to use a specific old VS Code version, elan version and vscode-lean version and then perform a series of rain dances to set it up correctly. Gitpod is also not guaranteed to be around forever.

[Shreyas Srinivas]

Gitpod may not be. But short of catastrophic events, some form of containerisation method which is compatible with docker is likely to exist.

[Shreyas Srinivas]

Also, I was able to build lean3 projects eventually and make a container of it. Just had trouble getting cache

[Marc Huisinga]

VS Code, the VS Code extension and the VS Code marketplace are not part of the container in the Gitpod setup.

Also, I was able to build lean3 projects eventually

I didn't claim otherwise.

[Shreyas Srinivas]

The issue here is that most countries and grant agencies have rules about research artefact preservation for X many users, where X is 10 in many places. The less troublesome we make it to run old stuff the easier it is for people to use lean for a paper. Not being able to run something just 4 years old is not a good sign.

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

Letting the extension remain on the marketplace removes one step necessary to build old projects

[Eric Wieser]

Marc Huisinga said:

The only way to still update that extension is to patch an existing VSIX.

Changing the displayName sounds like a pretty straightforward patch of the VSIX file, unless there's a signature or checksum in there somewhere

[Eric Wieser]

Marc Huisinga said:

Outside of vscode-lean, the last time I tried to build an old Lean 3 project, I couldn't get it to work without adjustments because of the redirect issue.

This problem only exists for leanprover/lean; leanprover-community/lean was never redirected precisely to avoid this breakage.

[Marc Huisinga]

Eric Wieser said:

Marc Huisinga said:

The only way to still update that extension is to patch an existing VSIX.

Changing the displayName sounds like a pretty straightforward patch of the VSIX file, unless there's a signature or checksum in there somewhere

Yes, it's just a bit annoying to publish this as well. I'd be happy to do it if we agree that we want to change the name of the extension in a more clear manner (e.g. something like Lean 3 (obsolete)) so that it sends a stronger signal than the description already does.

[Mario Carneiro]

There is a way to formally mark extensions as deprecated and point to other extensions, I've seen it before

[Mario Carneiro]

for example OCaml and Reason IDE is shown with a strikethrough and there is a warning next to the install button saying "This extension is deprecated. Use the OCaml Platform extension instead."

[Mario Carneiro]

Apparently you don't do this in the extension itself, instead you can report the extension deprecation request to microsoft here

[Marc Huisinga]

From a cursory search, it looks like this is not something that can be configured in the extension manifest and that needs to be done by the maintainers of the VS Code marketplace. I also wonder whether there is an equivalent for OpenVSX.
It also seems to prevent the installation of the extension using the UI, which means that this would be an alternative to eventually removing it from the marketplace, not changing the name to make it more clear that the extension is probably not what you need.

[Mario Carneiro]

you can still install via the ext install <extension name> method suggested by the marketplace webpage

[Mario Carneiro]

so this isn't truly blocking people who need to install it anyway

[Marc Huisinga]

Yes, I agree that this is a bit nicer than removing it from the marketplace, though unfortunately it doesn't look like OpenVSX supports deprecations.

[Mario Carneiro]

we could still do the display name thing for OpenVSX, that seems to be fairly common

[Mario Carneiro]

but also, it would be great to get it building again, I would like the lean 3 tech stack to keep working as long as possible for archival purposes

[Mario Carneiro]

I'll investigate that when I get a chance

[Marc Huisinga]

I'd be happy to unarchive and merge a PR if you are willing to do this.

[Marc Huisinga]

I've merged a display name change to Lean 3 (deprecated). I'll wait with releasing it until the build is fixed.

[Shreyas Srinivas]

I would suggest testing any vscode marketplace based deprecation strategy with gitpod and/or devcontainers. We just got flypitch running on gitpod last week (without cache though, so build took a while)