chore: explain a Nix-powered workflow

[RaitoBezarius]

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.

cc @Nadrieril @sonmarcho

[Nadrieril]

I'm working onremoving the need for rustup

[sonmarcho]

What was the issue exactly?

[RaitoBezarius]

What was the issue exactly?

It's easy to delude myself (anyone-self?) to use Charon and Aeneas separately and have difficult to debug issues because Charon and Aeneas are non-synchronized.

This workflow explains how to avoid this by design by reusing the Charon that Aeneas is depending on.

[Nadrieril]

Btw, rustup should no longer be needed

[Nadrieril]

Actually, why not add charon to the dev shell? You'd have to find a way to male charon-ml available to opam. The idea being that someone who only wants to dev on aeneas doesn't need to figure out how to build charon. Those who dev on both an have a special override

[RaitoBezarius]

Actually, why not add charon to the dev shell? You'd have to find a way to male charon-ml available to opam. The idea being that someone who only wants to dev on aeneas doesn't need to figure out how to build charon. Those who dev on both an have a special override

Seems orthogonal to me? People will nix run ..., not nix develop ... in general.
Or they would do what I did in https://github.com/RaitoBezarius/avl-verification/blob/main/default.nix#L9-L15 for longer term setups IMHO.

[Nadrieril]

Oh you're right, I was thinking of aeneas devs but this PR is for aeneas users. Nevermind

[RaitoBezarius]

Btw, rustup should no longer be needed

Removed.

[RaitoBezarius]

Wait, don't merge. This won't work without rustup, I think.

[Nadrieril]

Oh yeah this needs latest charon; I'll bump soon

[RaitoBezarius]

I need to do a test with that workflow, I recently had some issues while trying to extract stuff.

[sonmarcho]

Looks good, thanks!