Install why3 and why3find in local switch

[Lysxia]

Close #1359

• This finally reduces the installation to "clone then install".
• ./INSTALL now creates a local switch in ~/.local/share/creusot/_opam, and reuses it if there already is one.
• an install option --external why3-and-why3find to use whatever is in the $PATH. That is the old behavior, "for experts". CI also uses this option because the new behavior doesn't work well with caching (we do not want to cache the whole opam switch in CI (3Gb)).
• I noticed that cargo test --test why3 does an odd thing where it uses the installed why3, why3find, and provers, but the local prelude. It's a bit ad hoc, but I also couldn't think of a better solution, so I added some comments to remember that oddity.

[arnaudgolfouse]

Could we reduce the size of ~/.local/share/creusot/_opam? I tested removing the .opam-switch subdirectory, and it seems to work fine ; I assume this is just a cache?

[Lysxia]

The binaries would still work, but would opam install still work in that switch to upgrade dependencies?

[jhjourdan]

That's a question I've been asking myself for a long time: there seems to be a lot of duplication in opam switches, and a lot of caches. Which directory is it safe to remove? I've never had an answer.

[Lysxia]

It turns out a couple of those gigs are just the package sources and their build outputs. Removing them keeps the switch working, it will redownload the sources as needed. (I wonder if that breaks packages with custom uninstall scripts that need a built source but there are none in our dependencies.) The remaining files in a fresh switch with why3+why3find occupy 550Mb, almost all of it in bin/ (234M total: 28M dune, 23M ocaml, 23M why3find...) and lib/ (282M total: 147M ocaml, 63M why3, 28M lablgtk3...).

[arnaudgolfouse]

I was thinking that we could do something similar to the Rust dependencies: create the opam switch in /PATH/TO/CLONED_CREUSOT, and then copy only what we need to ~/.local/share/creusot/_opam. That way upgrades can just reuse whatever was cached in the cloned repo, and users that want to save on disk space can safely remove it.
This does make me uneasy though: opam packages may not like being moved around.

[Lysxia]

I think users will be fine with an extra opam switch lying around (especially if it can be reduced to just 0.5Gb).

The issue here is specifically for CI which runs ./INSTALL on every push. That now creates a switch, so we should cache it if we don't want to rebuild ocaml on every push. Previously we naively thought it would take multiple Gbs, but 0.5Gb seems much more reasonable.

[arnaudgolfouse]

Right, that seems reasonable indeed!