abandoning the "trylean" bundles?

Stream: general

[Scott Morrison]

There's been some suggestion to get rid of the "maybe a couple of nights" section of the installation instructions:
https://leanprover-community.github.io/get_started.html#maybe-a-couple-of-nights
mostly for the sake of simplifying the options.

Without any suggest that this is meant to be binding, I'll put a poll up, and hopefully get some discussion.

[Scott Morrison]

/poll What should we do with the trylean bundles on the installation page?
Remove them
Keep them as they are
Keep them, but lower down the page / less prominent

[Scott Morrison]

In favour of keeping them --- some people may find them useful! Do we have data on this? Even anecdotal?

[Scott Morrison]

In favour of removing them:

• reducing the amount of text on the installation page
• hopefully getting people to the default install instructions (which are currently at the bottom) faster
• reducing the maintenance burden by abandoning these bundles

[Damiano Testa]

I personally do not mind that there is the option of a trylean, but I have actually not taken that option. Another choice could be "Do not have a view, but would not use trylean"?

[Scott Morrison]

I made a PR suggesting some changes to the installation page, that moves "regular install" to the top, and makes everything a bit terser. Comments welcome. We can do the textual changes and rearrangements independently, etc.

[Kevin Buzzard]

Just to be clear -- I'm not complaining about the individual OS instructions at all -- far from it. I just want to be able to say e.g. on Twitter "here is a Lean thing. Want to play with it? Click here <blah> to install lean and mathlib." Currently the best link I know is misleading because it links to a small number of comments at the very bottom of a web page (so is easy to misunderstand) as opposed to the very top of a web page (which Scott's PR seems to do).

[Scott Morrison]

yes -- this doesn't touch the actual instructions for installing, just tries to get people to them faster

[Patrick Massot]

I like Scott's PR, although I would probably have kept the first sentence explaining there are several options.

[Patrick Massot]

I'd be curious to know whether our GitHub pages experts have access to any kind of download statistics for the bundled versions.

[Patrick Massot]

I know I want to keep bundles for use with students. There is no way I can ask my regular 1st year students (who have a mandatory course using Lean, not a club like Kevin) to follow any installation procedure that has more than one step or require admin rights. The key point here is the existence of the python script building the bundles, and I could run them on my computer once per year when new students arrive. And maybe in a couple of years I'll use Lean 4 and everything will be different, who knows? But then these scripts will be very hard to discover for people who would be tempted to also use Lean for teaching.

[Scott Morrison]

@Patrick Massot I've added a summary at the top of the page.

[Patrick Massot]

Merged

[Rob Lewis]

Patrick Massot said:

I'd be curious to know whether our GitHub pages experts have access to any kind of download statistics for the bundled versions.

The bundles are hosted on Azure. I don't know a way to get per-click analytics in Azure, but Azure is so confusing I could easily be missing it. GH Pages has no built in analytics AFAIK.

[Gihan Marasingha]

I've been using the Lean game maker to create teaching resources for the past term, but the later levels in my game run very slowly in the browser. I might move to using bundled versions of Lean + Mathlib + vscode.

Is creating my own bundle simply a matter of modifying the contents of the bundles avaialble on the lean community website? I imagine I could create a lean project first and then turn it into a bundle by:

• replacing the lean folder of trylean with the contents of the lean toolchain used by my repository (which I can find via elan which lean).
• Replace the mathlib folder of trylean with the copy from my lean project.
• Replace the src folder of trylean with the src folder of my lean project.

Is that it?

Thanks.

[Kevin Buzzard]

You're not tempted to move to lean 4?

[Gihan Marasingha]

@Kevin Buzzard that's the plan once I have stable teaching resources working in Lean 3. Is there something like either the Lean Game Maker or bundled versions of Lean for Lean 4?

[Kevin Buzzard]

I'm afraid I don't know! My point was just that making more bespoke lean 3 infrastructure seems somehow like it's going in the wrong direction. Ask about lean 4 stuff in the lean 4 stream maybe?

[Eric Wieser]

I assume you've already ruled out codespaces/gitpod-based setups? Those will still be faster than the game-maker

[Gihan Marasingha]

@Eric Wieser thanks. I am using GitHub Codespaces for assessing my students' lean work. I could continue using that approach for teaching (perhaps with Sphinx-based notes).

I like the bundled approach as it's a no-cost option if people outside my institution want to use the teaching resources.

[Martin Dvořák]

Is there any Windows wizard installer for Lean 4 + mathlib4 + VScode?

[Patrick Massot]

Gihan Marasingha said:

I've been using the Lean game maker to create teaching resources for the past term, but the later levels in my game run very slowly in the browser. I might move to using bundled versions of Lean + Mathlib + vscode.

Is creating my own bundle simply a matter of modifying the contents of the bundles avaialble on the lean community website? I imagine I could create a lean project first and then turn it into a bundle by:

• replacing the lean folder of trylean with the contents of the lean toolchain used by my repository (which I can find via elan which lean).
• Replace the mathlib folder of trylean with the copy from my lean project.
• Replace the src folder of trylean with the src folder of my lean project.

Sorry about the slow answer, I'm on vacation and my computer power supply died. There is no mystery about how those bundles are created, it all happens at https://github.com/leanprover-community/azure-scripts/blob/master/mk_bundle.py

[Patrick Massot]

The main tricks are https://code.visualstudio.com/docs/editor/portable and https://vscodium.com/ if you are serious about not distributing VSCode. Note the current setup has one flow: it doesn't ship a suitable font. I plan to try to fix that before the end of January. It sounds like a purely esthetic issue but the CSS tricks that do indentation in the info view get bad in a really nasty way with the wrong kind of font.

[Martin Dvořák]

In case the font must be hardcoded, I vote for: https://www.jetbrains.com/lp/mono/