doc: initialize a user-facing mdbook

[RaitoBezarius]

@sonmarcho @R1kM Here's my proposal regarding documenting progress among other things that I learned during the FV of AVL trees.

A mdBook-style user facing documentation with a part on "Proving Rust code with Lean" which dumps all that I know about using Aeneas & Lean in practice on Rust code.

Question is: do I do everything in this PR or shall we just get the CI right and improve on it incrementally as we commit to an outline, etc. ?

[sonmarcho]

Thanks for starting this, it was much needed!
Following our conversation, we should first get the CI right and do things incrementally. In particular, once we get the outline and the CI working, anybody can start making changes.

Also, I would like to use Alectryon to generate the documentation for Lean: I believe it would be super useful if we could display the goals in the documentation (it makes it easier to understand what the tactics do) and it will also give us a way of ensuring that the documentation stays up to date with the code (by checking that proofs in the doc don't break).

[RaitoBezarius]

Moved to an Alectryon setup.

[sonmarcho]

@Nadrieril I think it's important that you keep an eye on this PR as well. I just discussed with @RaitoBezarius : the PR will push to the branch gh-pages; I will set up the github pages for this branch once it is created.

[RaitoBezarius]

@Nadrieril ping on this :)

[RaitoBezarius]

@Nadrieril can i ping you for the merge?

[sonmarcho]

The PR #282 is blocked because the doc building fails.

[RaitoBezarius]

Urgh.

[RaitoBezarius]

Sent a hotfix in another PR.