This is a first sketch of user documentation for Aeneas to prove things
with Lean.

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>

Well, this is required… Following Loogle's steps, we add fake files for
ProofWidgets4 and we can produce an .olean from Aeneas' base library
without Lake involvement!

Free parallelization and caching :).

TODOs are to improve the hash handling when lake-manifest.json bumps,
but this requires extending Lake to produce the NAR hash serializations.

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>

I extracted a Factorial example in Rust to Lean.

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>

As upstream is moving to a non-user-facing Nix library,
we are vendoring some of the useful code such as `buildLeanPackage`.

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>

Adds the TODO list for infrastructure.

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>

Micro-guide for update:

- Update the Lean flake.
- Update all the sha256 hashes of every dependency if you have a
compilation error, e.g. batteries changed, etc.

The day where `inputs.lean.packages.${system}.deprecated` disappear, we
will need to consider an alternative for the nixpkgs from lean, etc.

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>