Newbie Question

Stream: new members

[TimP]

Starting at https://leanprover.github.io/programming_in_lean/#01_Introduction.html
I click the blue `Try it yourself' buttons. The system responds, in differing amounts of time, with Done. Not sure how, or whether, to proceed.

[Mario Carneiro]

Ah, that editor is out of date

[Mario Carneiro]

We suggest https://leanprover-community.github.io/lean-web-editor/ if you want an online editor

[Mario Carneiro]

But I think it still works. When I press the "try it yourself" button, the right side pane fills with the code from the snippet, and you can edit that code (it's a text editor)

[Mario Carneiro]

If you make a modification, errors should show up on the left gutter, and lots of things have hovers

[TimP]

It works in some sense, but does not output anything other than Done! So the Hello World only outputs Done. It would be good to update to remove this stumbling block for the hesitant adopter.

[Mario Carneiro]

The bottom panel only shows compilation status. The hello world should be in an information thing in the gutter

[Mario Carneiro]

(again, it's out of date, although I don't think that book has specifically been updated to use the new stuff, seeing as it's unfinished/abandoned)

[Mario Carneiro]

A newer resource for CS minded folks is the hitchhiker's guide to logical verification

[Mario Carneiro]

in any case, we don't have any access to change that particular site, we can only hope that SEO favors https://leanprover-community.github.io/learn.html

[Mario Carneiro]

@TimP