Installation and usage instructions

Stream: new members

[Kevin Buzzard]

On my blog home page there is an "installing Lean and mathlib" link right at the top now. It takes you here which is a page (not a post, for those of you that understand blogs) which lists everything I could think of which could help a new user getting started. Comments and criticisms very welcome.

[Kevin Buzzard]

@Mario Carneiro Do you want me to mdify this page and push it to the mathlib docs directory?

[Scott Morrison]

Hi Kevin -- the black bar with links in it under the screenshot is really hard to see. It's text on a black background, abutting more text on a black background which you immediately ignore upon starting to read.

[Scott Morrison]

I gave up and was about to come back here and say "I can't find the link", but tried one more time. :-)

[Scott Morrison]

You might just replace the screenshot image with one done in "light mode" in VS Code. :-)

[Kevin Buzzard]

How do I get VS Code into light mode?

[Kevin Buzzard]

ooh, done it

[Kevin Buzzard]

This whole thing is a "theme" issue I guess. Let me fiddle with my wordpress theme.

[Scott Morrison]

The instruction page itself is fantastic.

[Scott Morrison]

Everything in one place, and not too long.

[Scott Morrison]

(I'd reverse the order of the instructions myself, but I appreciate the reason to do it this way.)

[Kevin Buzzard]

As readers of this chat know, being too long is unfortunately one of my failings. I need a good (human) editor. I'm almost surprised you say it's not too long -- almost everything I write is too long. I changed the image. It looks weird now :-)

[Kevin Buzzard]

Of course I can change the order of the instructions. I don't know who my readers are. In some sense my target audience is Imperial's undergraduates and we've just got a new bunch of fresh people and I want as many of them as possible to engage with Lean as soon as possible. How about I switch it in 1 month? :-) I'm serious!

[Scott Morrison]

No, I think overall you're right to put it in this order. The people who most need cocalc and the online version are the people who deserve their instructions first/ :-)

[Scott Morrison]

In my talks I've certainly done it this order: mention online and cocalc, and then say "but for real use we use VS Code"

[Kevin Buzzard]

Thanks for looking by the way! I think the black bar at the top of the new image has been put there by the wordpress theme so people can see where the image starts.

[Scott Morrison]

The new version is much better!

[Kevin Buzzard]

Of course that doesn't mean it's good yet :-) I have no aesthetic feeling or opinion about pretty much anything. I would happily hear any more comments about anything. Part of me wants to find an undergraduate or other random person who wants to be involved and who has a much better feeling for general content delivery. Actually I think there might even be people employed by my university to advise on such things!

[Scott Morrison]

We're getting there. And you writing this just prompted me to improve the mathlib page on installing via elan a little further. :-)

[William Stein]

We just launched X11 Desktop support for CoCalc, so it's also possible to use VS Code and Full Emacs inside CoCalc. Here's a screenshot of using LEAN in VSCode via CoCalc: c.png

[William Stein]

That screenshot is in this blog post on the CoCalc Docker image: http://blog.sagemath.com/cocalc/2018/11/07/cocalc-docker-gcp.html

There's also a blog post on the new X11 Desktop support: http://blog.sagemath.com/cocalc/2018/11/05/x11.html

[Johan Commelin]

@William Stein I saw that blogpost! Really cool! And very impressive what you pulled off!

[Johan Commelin]

I haven't yet tested it. I guess the key question is whether the network connection can handle this, or whether you get a lot of lag.

[Johan Commelin]

This will definitely depend on the connection of your device...

[William Stein]

@William Stein I saw that blogpost! Really cool! And very impressive what you pulled off!

Thanks. There are still some subtle details to address. E.g., vscode shows a menu in the upper right as slightly off the screen, so I need to make sure to manually move such "X11 overlays" so they are fully visible on screen. But overall this approach to Linux graphical applications fits into how CoCalc already works, and adds an enormous amount of new functionality.