Zulip Chat Archive

Stream: general

Topic: guides

view this post on Zulip James King (Jan 07 2020 at 04:28):

I'm coming to Lean as a programmer first who is working on group and category theory on the side. In order to fill in the gap on documentation on how to use Lean from the perspective of a programmer I created, https://agentultra.github.io/lean-for-hackers/

It's a guide meant for programmers and enthusiasts, for Lean 3, hence the title.

I hope someone finds it useful. Appreciate any feedback.

view this post on Zulip James King (Jan 07 2020 at 04:29):

I was inspired a bit by my own frustrations and watching George Hotz's twitch stream when he was running into issues getting started.

view this post on Zulip James King (Jan 07 2020 at 04:41):

It's also a work in progress. Starting with your typical, "Hello, world" style examples.

view this post on Zulip Johan Commelin (Jan 07 2020 at 05:23):

@James King Nice, it's sort of the complement of the usual guides (-;

view this post on Zulip Alex J. Best (Jan 07 2020 at 05:52):

This is really nice! One comment: "Lean doesn’t have any concept of an implicit entry-point into our program", if you run lean as lean --run then function main is run as an entry point, this might be more familiar for hackers.

view this post on Zulip Bryan Gin-ge Chen (Jan 07 2020 at 06:31):

If you don’t use one of those editors, Lean speaks LSP.

Lean 3 doesn't actually speak LSP, though apparently Lean 4 will. For Lean 3, you can send JSON messages to lean --server via stdin and then receive JSON responses from stdout. The message format can be deduced from the code in the lean-client-js-core package.

view this post on Zulip James King (Jan 07 2020 at 14:14):

Thanks for the feedback! I'll get that updated ASAP. And maybe add a disclaimer that it's a work in progress. :smiley:

Last updated: May 13 2021 at 05:21 UTC