_Functional Programming in Lean_ is now done and out the door!
It's a free online book that describes using the interactive theorem prover Lean 4 as a programming language, without assuming any background in functional programming. You don't need to already know Haskell, OCaml, Rust, Scala, or Racket to read this book.
You can read it at https://leanprover.github.io/functional_programming_in_lean/ .
Thank you to everyone who's carefully read prereleases - it's much, much better than it otherwise would have been. The Lean Zulip is a great place to hang out.
Also, thanks to MSR for supporting this project, and to Leonardo de Moura for initiating it. It's been a lot of fun!
@d_christiansen can we buy it somehow? 🙂
@jonn It's free! No purchase necessary!
On a more serious noted, we ended up cutting the PDF and epub versions for time reasons. In an earlier version, there was code that translated from the mdbook dialect of Markdown to the Pandoc dialect, which allowed nice looking PDFs via TeX as well as nice epubs. But all the subtle little incompatibilities added up, and there wasn't time to make it happen in a way that we felt good about.
I would like to have a nice bound version, though. I'm old fashioned that way.
If you're looking to have something you can read away from the computer, the whole thing is CC-BY, so you can make your own and share it with your friends! I did most of my proofreading with a browser-based print-to-PDF on my Remarkable, which was comfortable.
@d_christiansen yeah, I know these trick.
The question was meant purely as a question about supporting your work (in exchange for a typeset PDF :D).
Maybe community should typeset it for you? :)
@jonn Microsoft supported the work quite well already - the best support you can give is to read the book carefully and learn what you can from it. Thanks for wanting to, though!
The work of a typeset version isn't just something like a LaTeX export. To be a quality print book, I'd also have to make an index, figure out how to conditionally export page references instead of internal hyperlinks, etc. I think it's more a task for the author than a community one.
@d_christiansen @jonn It seems that readthedocs supports exporting to EPUBs automatically (https://github.com/readthedocs/readthedocs.org/blob/main/.readthedocs.yml). Is it doable on your side? Not for a quality print book, but a version to read on eInk devices.
@d_christiansen @jonn I don't think that it is something that I can do from my side. If I understand correctly, it is some option on your readthedocs account, and once you enable it, it should produce an EPUB file automatically (without any "support" from you). If it does not work, it is a bug of readthedocs. I see bug reports in their github, e.g. https://github.com/readthedocs/readthedocs.org/issues/8362
@ohThef7y @jonn It's neither built with Sphinx nor hosted at readthedocs, so I don't think I can just use that option. It's built in mdbook and hosted on GH pages. From what I can see, I'd need to spend some time researching epub backends for mdbook, and I'm totally swamped right now. And an epub output would require a proofreading pass that I'd like to give it someday, but not right now.
@jonn I don't know how to do that conveniently from my side, frankly. I mean, I can export page-by-page, and I am not sure whether it would treat the hyperlinks correctly. It would require much more work than an option on the server side.