Installing Lean for Waterproof

Stream: lean4

[Pim Otte]

Just another small question with respect to our Lean support in Waterproof. We would like to provide an easy install experience for students. What the Lean 4 extension provides would be perfect. Currently, we have our own LSP client, but have to disable any active Lean 4 extension, to prevent doubling of error messages and other conflicts. The current instructions are "Follow the official installation instructions", but we would like to activate these through the Waterproof extension.

I see a couple of options:

1. Vendor the relevant files from the Lean 4 extension and duplicate the installation code
2. Refactor to a runtime dependency on the Lean 4 extension
3. Roll our own (not my preference)
4. Stick with "Install Lean 4 using official instructions"
5. Something else?

Option 1 seems least effort, but also introduces some technical debt/the need to synchronize every once in a while.
Option 2 might have some additional benefits, such as being able to rely on the Lean 4 extension for part of our functionality.

@Marc Huisinga (or others with good ideas): Any thoughts? In particular, I'm wondering if having a runtime dependency on the Lean 4 extension is something that you think is feasible from a stability point of view.

[Marc Huisinga]

Please stick with 4 for now.

We might make the extension more modular in the future so that 2 becomes more feasible (or perhaps even factor out some components into separate packages so that they do not depend on VS Code at all anymore), but it is not feasible at the moment.

[Emilio Jesús Gallego Arias]

Cc @Jason Reed , the upcoming workbench could be a great fit for the Waterproof use case.

I'm really looking forward to LeanWaterproof!