Lean tutorial first version.

[maximebuyse]

This PR adds documentation about the Lean backend in the hax tutorial. It covers:

• How to setup a lakefile.toml to verify a Rust crate using hax and Lean.
• Basic description of the Lean backend, and its specificity, in particular the difference with respect to panic-freedom.
• The example of the square function, how to specify panic-freedom, prove it using a pre-condition, and prove a simple post-condition.

[maximebuyse]

I added the playground integration for lean! I took the opportunity to make small fixes in the playground integration like fixing the "extract + type-check" button which was missing. For now the code snippets that are expected to type-check don't, that's because of the missing lib stuff that are part of this PR (so everything should work once the PR gets merged). @W95Psp I have a small problem: in the result of the playground queries Done.success is set to true for lean, event when type-checking fails.

[W95Psp]

@maximebuyse and I discussed in some other places about that bug, I fixed it in the playground.
(the captured and returned exit code was wrong)

[karthikbhargavan]

Looks good. Let's merge and improve.

[karthikbhargavan]

Unless there is something left here, please merge.

[W95Psp]

After some discussion we decided to split the tutorial in two: one for F*, one for Lean, and probably one for other backends in the future.

[maximebuyse]

@W95Psp @clementblaudeau This is ready for re-review.

[W95Psp]

Looking at it now

[clementblaudeau]

Very nice addition ! I've added a few suggestions.

[maximebuyse]

The CI fails because of missing space. I wonder if the addition of mkdocs-awesome-nav to the nix inputs could be the reason. But this should affect only docs and the failing jobs are unrelated. I don't really know how to debug that.

[W95Psp]

Seems like some of our CI runs on the self hosted runners?
anyway, it seems the disk is full, I'm running some garbage collection for nix (with the playground, we can end up with a big number of hax in the same time that eats up quickly the disk)

[maximebuyse]

Seems like some of our CI runs on the self hosted runners? anyway, it seems the disk is full, I'm running some garbage collection for nix (with the playground, we can end up with a big number of hax in the same time that eats up quickly the disk)

Yes, I also noticed it was an issue on self hosted runners only. I don't think there is a good reason to do so and it was probably by mistake, so I pushed a change to run all jobs on github hosted runners.