Proposal: better "install" link.

Stream: general

[Kevin Buzzard]

I have noticed the following issue several times.

I make or see some gadget, and I want to get people to play around with it, and all they have to do to get that going right away (say they're on Windows, and not computer-savvy, but good at logic on paper) is make sure they have a fully working leanproject. But where's the "install" web page which a the top says "Choose your OS: Windows, Mac, Unix" and then all the other stuff in the small print? I think that a good place to point to would be a real help for beginners.

At the minute I link to the install instructions here on the web pages. However the link itself is right at the bottom of the page, and on my browser the relevant part is not displaying at the top of the output so the "windows" link is pretty hard to spot.

[Alex Peattie]

I wonder if things have gotten to the stage too where it's worth promoting the Regular Install more as the default option? (I think the install instructions makes it almost seem like it's for serious users only). I think with all the helpful things like elan & mathlib-tools in the regular install, it's probably actually more beginner friendly than trylean in many cases.

[Patrick Massot]

Alex, you'd be astonished to see how many people like computers enough to consider playing with a proof assistant yet are unable (or very reluctant) to install a python package. This is completely beyond me, but we've seen it sooo many times here.

[Shing Tak Lam]

Some ideas:

1. Change the organisation of the page(s) so the user goes to the page for their OS of choice, then the information about using the bundle/installing. There'll be duplication but I don't think it's that big of an issue tbh. The current page has OS specific messages in the section about bundles, and splitting it can probably tidy it up a bit.
2. Promote the links there to a list (makes it a lot more visible)

2 should solve the issue of it being hard to discover, and I'm not sure 1 is a good idea.

[Alex Peattie]

Patrick Massot said:

Alex, you'd be astonished to see how many people like computers enough to consider playing with a proof assistant yet are unable (or very reluctant) to install a python package. This is completely beyond me, but we've seen it sooo many times here.

Ah that's interesting! I notice that for the macOS/Ubuntu install instructions, it's all bundled into a shell script so it's just a case of running a single command. So maybe overcomes the "scariness" factor of installing a Python package etc. I'm not as familiar with Windows batch files etc. but I wonder if we could get Windows to the same point (run one command and you're sorted) :thinking: ?

[Patrick Massot]

We could have a one-click install on Windows if a Windows user cares enough to spend a couple of days figuring out how to do that.

[Kevin Buzzard]

I just want to know what to link to to "install mathlib now" in the README in projects like this which I might be plugging on Twitter or CoCalc or whatever.

[Kevin Buzzard]

Every project I will ever have will depend on mathlib I think, because it's either maths or tactics.

[Damiano Testa]

Kevin Buzzard said:

I just want to know what to link to to "install mathlib now" in the README in projects like this which I might be plugging on Twitter or CoCalc or whatever.

I tried playing your game, I think that I mapped the rooms and tried out from all of them, but no room appears to work. I saw from the definition file where the exit is supposed to be, and even so, I cannot get out! I seriously thought that I knew enough lean to be able to solve this... Am I missing something?

[Rob Lewis]

You're not missing something. There's a missing namespace at definition.lean:78

[Johan Commelin]

@Kevin Buzzard https://github.com/kbuzzard/maze-game/pull/1

[Damiano Testa]

Rob Lewis said:

You're not missing something. There's a missing namespace at definition.lean:78

That explains it! Thanks!

[Johan Commelin]

It's like a real maze (-; You can't get out.

[Johan Commelin]

Real mazes are a-mazing!

[Kevin Buzzard]

fixed.

[Kevin Buzzard]

Thanks!