Merge pull request #1003 from Armael/setup-v2

creusot setup v2: more flexible per-tool settings for managed/external status and version checking

.github/workflows/nightly.yml

@@ -34,6 +34,6 @@ jobs:
     - name: run cargo creusot setup install
       if: steps.cache-creusot-setup.outputs.cache-hit != 'true'
       run: |
-        cargo run --bin cargo-creusot creusot setup install
+        cargo run --bin cargo-creusot creusot setup install --no-check-version why3
     - run: cargo test --test why3 "" -- --replay=none --diff-from=origin/master
     - run: cargo test --test why3 "" -- --skip-unstable

.github/workflows/rust.yml

@@ -45,7 +45,9 @@ jobs:
     - name: Build
       run: cargo build
     - name: dummy creusot setup
-      run: cp -r .creusot-config.sample .creusot-config
+      run: |
+        mkdir -p ~/.config/creusot
+        cp ci/creusot-config-dummy.toml ~/.config/creusot/Config.toml
     - name: Run tests
       run: cargo test
   why3:

HACKING.md

@@ -5,32 +5,20 @@ working on the Creusot codebase.
 
 ## Setup
 
-The "Creusot developer setup" sometimes requires more flexibility in how it
-looks up why3 and related solvers, compared to the standard "user" workflow
-provided by `cargo creusot setup install`. You have two options:
-
-- **By default** the testsuite will use the global Creusot configuration managed
-  by `cargo creusot setup`. You first need to have successfully run `cargo
-  creusot setup install` (or `cargo creusot setup install-external`).
-- **Alternatively** you can set a custom "developer" Creusot configuration in
-  `.creusot-config/` at the root of the git repo. Start by running `cp -r
-  .creusot-config.sample .creusot-config`. This will tell the testsuite to use
-  whichever `why3` binary is in the PATH, but you can also tweak
-  `.creusot-config/Config.toml` to point to a specific binary.
-
-The first option is recommended if you simply want a working setup to run the
-testsuite.
-
-The second option is useful if you need to try custom versions of Why3 or the
-solvers.
-
-Notes:
-- to avoid first installing the `cargo-creusot` binary before running `cargo
+The testsuite will use the global Creusot configuration managed by 
+`cargo creusot setup`. 
+You first need to have successfully run `cargo creusot setup install` as
+detailed in the README installation instructions.
+
+**To be able to use custom versions of Why3 or the solvers** (instead of the
+built-in ones expected by Creusot), one can pass extra flags to 
+`cargo creusot setup install` (see also `--help`):
+- `--external <TOOL>` to specify that a solver should be looked up from the path
+- `--no-check-version <TOOL>` to allow unexpected versions of a given tool
+
+To avoid first installing the `cargo-creusot` binary before running `cargo
   creusot setup`, one can directly call it from the git repository: `cargo run
   --bin cargo-creusot creusot setup`
-- the format of the `.creusot-config/` directory is simply the same as
-  `~/.config/creusot`, which is where `cargo creusot setup` writes its
-  configuration.
 
 ## Running the testsuite
 

cargo-creusot/src/main.rs

@@ -55,7 +55,7 @@ fn main() -> Result<()> {
                 (subcmd, false)
             };
 
-            let config_args = setup::status_for_creusot(&cargs.config_dir)?;
+            let config_args = setup::status_for_creusot()?;
             let creusot_args = CreusotArgs {
                 options: cargs.options,
                 why3_path: config_args.why3_path.clone(),
@@ -70,9 +70,7 @@ fn main() -> Result<()> {
                 // why3 configuration
                 let mut b = Why3LauncherBuilder::new();
                 b.why3_path(config_args.why3_path);
-                if let Some(p) = &config_args.why3_config {
-                    b.config_file(p.clone());
-                }
+                b.config_file(config_args.why3_config);
                 b.output_file(mlcfg_filename);
                 // temporary: for the moment we only launch why3 via cargo-creusot in Ide mode
                 b.mode(Why3Mode::Ide);
@@ -91,12 +89,22 @@ fn main() -> Result<()> {
 
             Ok(())
         }
-        Setup(SetupSubCommand::Status) => setup::status(&cargs.config_dir),
-        Setup(SetupSubCommand::Install) => {
-            setup::install(&cargs.config_dir, setup::InstallMode::Managed)
-        }
-        Setup(SetupSubCommand::InstallExternal { no_resolve_paths }) => {
-            setup::install(&cargs.config_dir, setup::InstallMode::External { no_resolve_paths })
+        Setup(SetupSubCommand::Status) => setup::status(),
+        Setup(SetupSubCommand::Install { external, no_check_version }) => {
+            let extflag =
+                |name| setup::ExternalFlag { check_version: !no_check_version.contains(&name) };
+            let managedflag = |name, mname| setup::ManagedFlag {
+                check_version: !no_check_version.contains(&name),
+                external: external.contains(&mname),
+            };
+            let flags = setup::InstallFlags {
+                why3: extflag(SetupTool::Why3),
+                altergo: extflag(SetupTool::AltErgo),
+                z3: managedflag(SetupTool::Z3, SetupManagedTool::Z3),
+                cvc4: managedflag(SetupTool::CVC4, SetupManagedTool::CVC4),
+                cvc5: managedflag(SetupTool::CVC5, SetupManagedTool::CVC5),
+            };
+            setup::install(flags)
         }
     }
 }

ci/creusot-config-dummy.toml

@@ -0,0 +1,21 @@
+version = 2
+
+[why3]
+path = "why3"
+check_version = false
+
+[altergo]
+path = "alt-ergo"
+check_version = false
+
+[z3]
+mode = "builtin"
+check_version = false
+
+[cvc4]
+mode = "builtin"
+check_version = false
+
+[cvc5]
+mode = "builtin"
+check_version = false

creusot-args/src/options.rs

@@ -47,7 +47,7 @@ pub struct CreusotArgs {
     pub why3_path: PathBuf,
     /// Specify an alternative location for Why3's configuration
     #[arg(long)]
-    pub why3_config_file: Option<PathBuf>,
+    pub why3_config_file: PathBuf,
     #[command(subcommand)]
     pub subcommand: Option<CreusotSubCommand>,
     #[clap(last = true)]
@@ -72,9 +72,6 @@ pub enum CreusotSubCommand {
 pub struct CargoCreusotArgs {
     #[clap(flatten)]
     pub options: CommonOptions,
-    /// Custom path for Creusot's config directory (managed by 'cargo creusot setup')
-    #[arg(long)]
-    pub config_dir: Option<PathBuf>,
     /// Subcommand: why3, setup
     #[command(subcommand)]
     pub subcommand: Option<CargoCreusotSubCommand>,
@@ -101,18 +98,34 @@ pub enum Why3SubCommand {
     Replay,
 }
 
+#[derive(Debug, ValueEnum, Serialize, Deserialize, Clone, PartialEq)]
+pub enum SetupManagedTool {
+    Z3,
+    CVC4,
+    CVC5,
+}
+
+#[derive(Debug, ValueEnum, Serialize, Deserialize, Clone, PartialEq)]
+pub enum SetupTool {
+    Why3,
+    AltErgo,
+    Z3,
+    CVC4,
+    CVC5,
+}
+
 #[derive(Debug, Parser, Clone)]
 pub enum SetupSubCommand {
     /// Show the current status of the Creusot installation
     Status,
     /// Setup Creusot or update an existing installation
-    Install,
-    /// Setup Creusot but use external tools configured manually (not recommended, for experts)
-    InstallExternal {
-        /// Do not lookup and resolve paths to the external binaries (they will
-        /// instead be looked up in PATH at each Creusot invocation)
-        #[arg(long, default_value_t = false)]
-        no_resolve_paths: bool,
+    Install {
+        /// Look-up <TOOL> from PATH instead of using the built-in version
+        #[arg(long, value_name = "TOOL")]
+        external: Vec<SetupManagedTool>,
+        /// Do not error if <TOOL>'s version does not match the one expected by creusot
+        #[arg(long, value_name = "TOOL")]
+        no_check_version: Vec<SetupTool>,
     },
 }
 

creusot-dev-config/src/bin/dev-env.rs

@@ -18,9 +18,7 @@ pub fn main() -> anyhow::Result<()> {
     };
     println!("PATH={:?}; export PATH;", &new_path);
 
-    if let Some(config) = &paths.why3_config {
-        eprintln!("Using Why3 config at: {}", config.display());
-        println!("WHY3CONFIG='{}'; export WHY3CONFIG;", &config.display());
-    }
+    eprintln!("Using Why3 config at: {}", &paths.why3_config.display());
+    println!("WHY3CONFIG='{}'; export WHY3CONFIG;", &paths.why3_config.display());
     Ok(())
 }

creusot-dev-config/src/lib.rs

@@ -4,29 +4,14 @@ use std::{path::PathBuf, process::Command};
 /// calling why3 in development workflows. This is used in particular by the
 /// testsuite.
 
-/// We look for configuration specifying Why3's path and configuration in the
-/// following places:
-/// - in the .creusot-config directory at the root of the git repo, if it exists
-/// - otherwise, in the global config repository used by creusot setup
-
-pub fn custom_config_dir() -> Option<PathBuf> {
-    let local_config = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("../.creusot-config");
-    if local_config.is_dir() {
-        Some(std::fs::canonicalize(local_config).unwrap())
-    } else {
-        None
-    }
-}
-
 pub struct Paths {
     pub why3: PathBuf,
-    pub why3_config: Option<PathBuf>,
+    pub why3_config: PathBuf,
 }
 
 /// Fails if the config could not be loaded
 pub fn paths() -> anyhow::Result<Paths> {
-    let custom_config_dir = custom_config_dir();
-    let paths = creusot_setup::status_for_creusot(&custom_config_dir)?;
+    let paths = creusot_setup::status_for_creusot()?;
     Ok(Paths { why3: paths.why3_path, why3_config: paths.why3_config })
 }
 
@@ -36,8 +21,6 @@ pub fn paths() -> anyhow::Result<Paths> {
 pub fn why3_command() -> anyhow::Result<Command> {
     let p = paths()?;
     let mut cmd = Command::new(p.why3.clone());
-    if let Some(ref config) = p.why3_config {
-        cmd.arg("-C").arg(config);
-    }
+    cmd.arg("-C").arg(p.why3_config);
     Ok(cmd)
 }

creusot-rustc/src/options.rs

@@ -8,7 +8,7 @@ pub trait CreusotArgsExt {
 
 fn why3_command(
     path: PathBuf,
-    config_file: Option<PathBuf>,
+    config_file: PathBuf,
     cmd: CreusotSubCommand,
 ) -> options::Why3Command {
     let CreusotSubCommand::Why3 { command, args, .. } = cmd;

creusot-setup/src/config.rs

@@ -7,28 +7,33 @@ use std::{
 // identifies a version of the config file.
 // the goal is to avoid silently mis-interpreting a past or future version of
 // the config file whenever its format changes.
-pub const CURRENT_CONFIG_VERSION: i64 = 1;
+pub const CURRENT_CONFIG_VERSION: i64 = 2;
+
+// bump CURRENT_CONFIG_VERSION if you change this definition
+#[derive(Serialize, Deserialize)]
+pub struct ExternalTool {
+    pub path: PathBuf,
+    pub check_version: bool,
+}
 
 // bump CURRENT_CONFIG_VERSION if you change this definition
 #[derive(Serialize, Deserialize)]
 #[serde(tag = "mode")]
-pub enum ToolsConfig {
-    #[serde(rename = "managed")]
-    Managed {
-        why3_path: PathBuf,
-        altergo_path: PathBuf,
-        z3: String,   // version
-        cvc4: String, // version
-        cvc5: String, // version
-    },
+pub enum ManagedTool {
+    #[serde(rename = "builtin")]
+    Builtin { check_version: bool },
     #[serde(rename = "external")]
-    External { why3_path: PathBuf, altergo_path: PathBuf },
+    External(ExternalTool),
 }
 
 // bump CURRENT_CONFIG_VERSION if you change this definition
 #[derive(Serialize, Deserialize)]
 pub struct Config {
-    pub tools: ToolsConfig,
+    pub why3: ExternalTool,
+    pub altergo: ExternalTool,
+    pub z3: ManagedTool,
+    pub cvc4: ManagedTool,
+    pub cvc5: ManagedTool,
 }
 
 pub enum Error {
@@ -76,21 +81,23 @@ impl Config {
     }
 }
 
-impl fmt::Display for ToolsConfig {
+impl fmt::Display for ExternalTool {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        writeln!(f, "- path: {}", self.path.display())?;
+        writeln!(f, "- check_version: {}", self.check_version)
+    }
+}
+
+impl fmt::Display for ManagedTool {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
-            ToolsConfig::Managed { why3_path, altergo_path, z3, cvc4, cvc5 } => {
-                writeln!(f, "mode: managed")?;
-                writeln!(f, "Path to Why3: {}", why3_path.display())?;
-                writeln!(f, "Path to Alt-Ergo: {}", altergo_path.display())?;
-                writeln!(f, "Z3 version: {z3}")?;
-                writeln!(f, "CVC4 version: {cvc4}")?;
-                writeln!(f, "CVC5 version: {cvc5}")
+            ManagedTool::Builtin { check_version } => {
+                writeln!(f, "- mode: builtin")?;
+                writeln!(f, "- check_version: {check_version}")
             }
-            ToolsConfig::External { why3_path, altergo_path } => {
-                writeln!(f, "mode: external")?;
-                writeln!(f, "Path to Why3: {}", why3_path.display())?;
-                writeln!(f, "Path to Alt-Ergo: {}", altergo_path.display())
+            ManagedTool::External(exttool) => {
+                writeln!(f, "- mode: external")?;
+                write!(f, "{exttool}")
             }
         }
     }
@@ -104,7 +111,7 @@ impl fmt::Display for Error {
             Error::WrongVersion(v) => write!(
                 f,
                 "Existing Creusot configuration found, \
-                           but with a different version than expected ({v}, \
+                           but with a different version than expected (found {v}, \
                            expected {CURRENT_CONFIG_VERSION})."
             ),
         }