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.
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.
James King (Jan 07 2020 at 04:41):
It's also a work in progress. Starting with your typical, "Hello, world" style examples.
Johan Commelin (Jan 07 2020 at 05:23):
@James King Nice, it's sort of the complement of the usual guides (-;
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.
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.
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