guides

Stream: general

[James King]

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]

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]

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

[Johan Commelin]

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

[Alex J. Best]

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]

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]

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