RFC: towards a rustup-like tool for creusot

[Armael]

I've been thinking a bit about the current UX for installing creusot, and how we can improve the current situation to make it easier/less brittle for users. We can't solve all problems at once, so I've been trying to think what could be a good first step that would put us in a good position and allow us to later iterate and incrementally solve the remaining problems (e.g. binary builds for why3, better interaction modes, bundled setup through a vscode extension, etc).

I outline below some ideas for a rustup-like tool which I hope could be a move in the right direction, and not very hard to implement on top of what we have right now.

high-level idea

Introduce an additional rustup-like binary for creusot named creusot-setup. (The name is up for discussion.)

creusot-setup manages a "creusot installation" described in ~/.creusot/. The goal is to move towards a world where creusot installs and controls the programs it depends on (why3 and solvers) and makes sure everything has the right versions and is configured properly.

For now, focus on the solvers which have downloadable binaries; why3 and alt-ergo will still have to be installed separately via opam.

There would be support for two types of "creusot installations":

• "managed" setup (recommended), where creusot-setup does as much as it can (downloading known good versions of the solvers, etc);
• "external" setup (only for experts), where creusot-setup only does basic sanity checks and creusot will load whatever is available in $PATH and assume it is adequately configured. (This corresponds to the current workflow.)

state management

creusot-setup reads and writes ~/.creusot/Config.toml (the user is not expected to access this file manually).
When creusot-setup fetches additional files (solver binaries, etc) it will also store them somewhere in ~/.creusot/....

The creusot-setup binary also includes (at build time) a list of "known good" solvers versions, and associated URLs where to download a binary build.
(for why3 and alt-ergo, for now only store their version and assume that they will be installed separately via opam)

the creusot-setup binary

creusot-setup would have two subcommands, status and install.

command: creusot-setup status

Displays the current status of the creusot installation.

A creusot installation can be in roughly three states:

• ~/.creusot/Config.toml does not exist, meaning that creusot-setup install has not been run yet. In this case creusot-setup status should just tell the user to run creusot-setup install --help and follow instructions.
• ~/.creusot/Config.toml exists and indicates that creusot-setup install was run and downloaded its own binaries for solvers (e.g. in ~/.creusot/solvers). ~/.creusot/Config.toml should then list the downloaded solvers and their version as well as the path to the why3 binary. In this case creusot-setup status should check that the versions of why3 and the solvers are not outdated wrt the "known-good" versions stored in the creusot-setup binary. If they are outdated it should advise the user to re-run creusot-setup install.
• ~/.creusot/Config.toml exists and indicates that creusot-setup install was run but told to use globally installed tools (in $PATH) and not manage its own solvers. In this case creusot-setup status could simply check the version of why3 found in the $PATH and emit a warning if it is not "known good", but that's it.
  I've tried to think of the UX for installing creusot, and how to make the current setup easier and less brittle for users,

command: creusot-setup install

Setups a creusot installation.

Without additional options, creusot-setup install produces a setup (in ~/.creusot/) where creusot downloads and manages its own solvers (and, later in the future, its own why3 binaries).
It records in ~/.creusot/Config.toml the list of downloaded solvers, their version, and (for now) the path to the why3 binary found in $PATH.

When run on an existing installation (existing ~/.creusot/Config.toml), running creusot-setup install would update the installation (downloading solvers to replace those that are out of date when needed).

In this mode, creusot-setup install also generates a file ~/.creusot/why3.conf that only refers to the solver binaries it downloaded. (Perhaps doable by running why3 config detect with a modified $PATH that only contains the solvers we want?)

option: creusot-setup install --use-external-tools

When passing --use-external-tools, the creusot-setup install command will instead simply record in ~/.creusot/Config.toml that we'll be using external tools. It only records the path to why3 and stops there.

This mode is the "expert mode" that corresponds to the current setup, where creusot will simply use whatever is reachable in the $PATH (why3, however it is configured) and trust the user that things are setup correctly.

behavior of creusot-rustc

We update slightly the behavior of creusot-rustc to depend on ~/.creusot/Config.toml.

• if ~/.creusot/Config.toml does not exist, stop and ask the user to run creusot-setup
• otherwise, when invoking why3 (eg with "why3 ide" or "why prove"), read the contents of ~/.creusot/Config.toml; if we're in "managed" mode, then pass to why3 a commandline option (-C) to use the why3.conf created by creusot-setup. Otherwise invoke why3 as currently.

notes

• Storing "known good" version numbers/URLs in the creusot-setup binary assumes that creusot-setup, cargo-creusot and creusot-rustc are always installed/updated at the same time. (For now, using cargo install from the creusot git repository.)

[xldenis]

I like this. In spirit it is similar to what Kani does: https://model-checking.github.io/kani/install-guide.html which seems to be a good model to have.

My only potential concern is with changing the behavior of creusot-rustc. I would rather creusot-rustc knows nothing about creusot-setup, and that cargo-creusot manipulates its flags as needed instead. This is a similar distinction to rustc and cargo, rustc has no knowledge of cargo or rustup, instead it is told where to look for relevant files via options.

[Armael]

Thanks for the pointer! I'll have a look at the kani setup.

Re: creusot-rustc, this is a good point. To make sure I understand, the idea is that cargo-creusot would instead be the one reading ~/.creusot/Config.toml, and passing relevant flags to creusot-rustc? If so that seems like a good idea indeed.

[Armael]

I see that kani has cargo kani setup, which does look pretty good. We could do the same and have cargo creusot setup instead of a separate creusot-setup binary.

[xldenis]

To make sure I understand, the idea is that cargo-creusot would instead be the one reading ~/.creusot/Config.toml, and passing relevant flags to creusot-rustc?

I see that kani has cargo kani setup, which does look pretty good. We could do the same and have cargo creusot setup instead of a separate creusot-setup binary.

Yea, I figured that whether it was a separate binary or a subcommand was sort of irrelevant to the meat of the proposal.

[claudemarche]

Your proposal is indeed very coherent with the way the Spark environment and the TIS-Analyzer environment are packaging Why3 and solvers. I imagine it is naturally the way to go. Yet :

(for why3 and alt-ergo, for now only store their version and assume that they will be installed separately via opam)

I'm not sure how this could be manageable. Why not also distributing binary versions of Why3 and Alt-Ergo? Of course an issue is to have such binaries for a bunch of architectures. Wouldn't it be a good thing to consider?

[Armael]

I fully agree that we would much better prefer distributing binary versions of why3 and alt-ergo.
It's just that these don't exist currently (afaik), so I was trying to think of what best-effort strategy we could follow if we were to implement this creusot-setup tool today.
But indeed we should push for why3/alt-ergo binaries to be available, and have creusot-setup fetch those along with the solvers as soon as they exist.

[xldenis]

I also think the approach proposed by @Armael generalizes well to distributing binaries of why3 / alt-ergo, we could subdirectories for why3 and provers. The challenge would then be setting up the packaging infrastructure for that.

[claudemarche]

Distributing binaries for Why3 would be nice for other purpose than Creusot anyway. I even promised to provide sometime a MS-Windows binary for Why3 (without the IDE though)

[Armael]

(Now implemented in #961 and merged!)

[jhjourdan]

Many thanks, @Armael !