Zulip Chat Archive

Stream: new members

Topic: Newbie Question


view this post on Zulip TimP (Oct 19 2020 at 11:18):

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.

view this post on Zulip Mario Carneiro (Oct 19 2020 at 11:20):

Ah, that editor is out of date

view this post on Zulip Mario Carneiro (Oct 19 2020 at 11:21):

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

view this post on Zulip Mario Carneiro (Oct 19 2020 at 11:22):

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)

view this post on Zulip Mario Carneiro (Oct 19 2020 at 11:24):

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

view this post on Zulip TimP (Oct 21 2020 at 11:05):

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.

view this post on Zulip Mario Carneiro (Oct 21 2020 at 11:13):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 11:13):

(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)

view this post on Zulip Mario Carneiro (Oct 21 2020 at 11:15):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 11:16):

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

view this post on Zulip Mario Carneiro (Oct 21 2020 at 11:17):

@TimP


Last updated: May 12 2021 at 04:19 UTC