chore: explain a Nix-powered workflow

To avoid divergence between Charon and Aeneas, we should re-export
Charon via our Flake and tell users to use this as a source of truth.

Here's an appendix on how I do refresh of my files, which can serve as
inspiration for a quick start workflow.

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

README.md

@@ -120,6 +120,30 @@ and tactics specialized for monadic programs (see
 
 A tutorial for the Lean backend is available [here](./tests/lean/Tutorial.lean).
 
+## Quick start for Nix users
+
+Assuming Nix is installed, with a support for Flakes (`*`):
+
+```console
+$ nix run github:aeneasverif/aeneas#charon -L
+$ # The default package for Aeneas is Aeneas.
+$ nix run github:aeneasverif/aeneas -L -- -backend your_preferred_backend your_llbc.file
+```
+
+To regenerate the extraction, just run step 2 and step 3 again.
+
+Sometimes, Charon and Aeneas can become desynchronized, changes of the LLBC on
+Charon side will not have been taken into account on Aeneas side yet. We try to
+avoid this as much but if you are using Nix, this is the simple way to avoid
+that problem. https://github.com/AeneasVerif/charon/issues/35 is related to that matter.
+
+`(*)` : Flakes are not necessary, here is an example of how to do similar steps without it:
+
+```console
+$ nix-shell '<aeneas>' -A packages.x86_64-linux.charon --run "charon" -I aeneas=https://github.com/AeneasVerif/aeneas/archive/main.tar.gz
+$ nix-shell '<aeneas>' -A packages.x86_64-linux.default --run "aeneas --backend your_preferred_backend your_llbc.file" -I aeneas=https://github.com/AeneasVerif/aeneas/archive/main.tar.gz
+```
+
 ## Formalization
 
 The translation has been formalized and published at ICFP2022: [Aeneas: Rust

flake.nix

@@ -152,6 +152,7 @@
       in {
         packages = {
           inherit aeneas;
+          inherit (charon.packages.${system}) charon-ml charon;
           default = aeneas;
         };
         devShells.default = pkgs.mkShell {