Add 'cargo creusot setup' to manage creusot installations #961
Conversation
|
Since this changes a bit the CLI workflow (now you have to go through the setup phase even if it's just for |
cargo-creusot/src/setup/config.rs
Outdated
| let s = match fs::read_to_string(p) { | ||
| Err(e) => return Err(Error::Invalid(e.to_string())), | ||
| Ok(s) => s, | ||
| }; |
There was a problem hiding this comment.
If we want more ergonomic error handling here we could look at eyre or more generally return a Box<dyn Error> object as the error case. Of you could define an instance of From for the appropriate types.
It doesn't matter much here, but in case you wanted comments for future changes.
There was a problem hiding this comment.
Ah I see you're using anyhow down below. The general approach seems to be thiserror in libraries and eyre (improved version of anyhow) in applications.
The implementation follows the design outlined here: creusot-rs#946 'cargo creusot setup' comes with the following subcommands: - 'status': displays the state of the current installation - 'install': sets up creusot in "managed" mode, downloading solver binaries at known-good versions and configuring why3 to use them. (Can also be invoked on an existing creusot installation to upgrade out-of-date solvers.) - 'install-external': minimal setup of creusot in "external" mode, that assumes that the user manages the external tools (why3, solvers, etc) themselves. For now, even the "managed mode" setup assumes that why3 and alt-ergo have been installed separately (e.g. using opam), but the goal is to later have 'creusot setup' download binaries when we have them.
Armael
force-pushed
the
setup-cmd
branch
3 times, most recently
from
2c9e3fc
to
820f3cd
Compare
- either use a .creusot-config directory from the root of the git repository, if it exists - or load the gloal creusot config directory (as setup by 'cargo creusot setup')
(this is what the CI uses currently)
Armael
force-pushed
the
setup-cmd
branch
2 times, most recently
from
6f2b732
to
5fddc1b
Compare
as a bonus, cache solver binaries using this file as cache key
…h to a library and also provide a why3 wrapper binary to use in shell scripts
|
I've updated the PR. There is quite a bit of new code: I've been working on the developer workflow (for people hacking on creusot, running the testsuite, etc) and tried to harmonize it with the "user" workflow introduced by The idea is that someone who has a working creusot setup (using I've also updated the user setup instructions in README.md to use the new All in all this is a bit more logic/code than I initially expected, but this is what I came up with trying to make things more robust. |
I think this is a good workflow, most of the time we are not working against custom solver versions or custom why3 versions. I also think it drastically simplifies the new contributor experience which is valuable as well. |
|
I've been reading over the code today, it all looks really good to me, and I can't wait to try it out. |
|
🎉 |
The implementation follows the design outlined here: #946 .
Note that this the first time I'm writing a non-trivial amount of Rust code, so I'm happy to take any comments regarding code style, organization, etc.
cargo creusot setupcomes with the following subcommands:status: displays the state of the current installationinstall: sets up creusot in "managed" mode, downloading solver binaries at known-good versions and configuring why3 to use them. (Can also be invoked on an existing creusot installation to upgrade out-of-date solvers.)install-external: minimal setup of creusot in "external" mode, that assumes that the user manages the external tools (why3, solvers, etc) themselves.For now, even the "managed mode" setup assumes that why3 and alt-ergo have been installed separately (e.g. using opam), but the goal is to later have 'creusot setup' download binaries when we have them.