Install creusot-rustc in a toolchain-dependent location

.github/workflows/rust.yml

@@ -138,10 +138,6 @@ jobs:
           ~/.cargo/git
           target
         key: ${{ runner.os }}-cargo-install-${{ hashFiles('**/Cargo.lock') }}
-    - name: Install
-      run: |
-        cargo install --path cargo-creusot
-        cargo install --path creusot-rustc
     - uses: actions/cache@v4
       id: cache-creusot-setup
       with:
@@ -150,17 +146,21 @@ jobs:
           ~/.local/share/creusot
           _opam/lib/why3find/packages
         key: ${{ runner.os }}-cargo-creusot-setup-${{ hashFiles('creusot-deps.opam', 'creusot-setup/src/tools_versions_urls.rs', 'creusot-setup/src/config.rs') }}
+    - name: Install
+      run: |
+        cargo install --path cargo-creusot
+        cargo creusot setup install --only-creusot-rustc
     - name: download why3 and why3find
       uses: actions/download-artifact@v4
       with:
         name: why3-deps
     - name: unpack why3 and why3find
       run: tar -xzf _opam.tar.gz
-    - name: setup creusot
+    - name: Setup
       run: |
         # Add /home/runner/work/creusot/creusot/_opam/bin to PATH just for this step
         export PATH=/home/runner/work/creusot/creusot/_opam/bin:$PATH
-        cargo creusot setup install
+        cargo creusot setup install --skip-creusot-rustc
       if: steps.cache-creusot-setup.outputs.cache-hit != 'true'
     - name: test cargo creusot new
       run: |

README.md

@@ -51,17 +51,15 @@ More examples are found in [creusot/tests/should_succeed](creusot/tests/should_s
    $ eval $(opam env)
    ```
    This will build `why3`, `why3find`, and their ocaml dependencies in a local `_opam` directory.
-5. Build **Creusot**:
+5. Install **Creusot**:
     ```
-    $ cargo install --path creusot-rustc
     $ cargo install --path cargo-creusot
+    $ cargo creusot setup install
     ```
-    this will build the `cargo-creusot` and `creusot-rustc` executables and place them in `~/.cargo/bin`.
-6. Set up **Creusot**:
-   ```
-   $ cargo creusot setup install
-   ```
-   this will download additional solvers (Alt-Ergo, Z3, CVC4, CVC5) and configure Why3 to use them.
+    The first command will build the `cargo-creusot` executable and place it in `~/.cargo/bin/`.
+    The second command will download solvers (Alt-Ergo, Z3, CVC4, CVC5), configure Why3 to use them,
+    then it will install the `creusot-rustc` executable; configuration files are stored in
+    `~/.config/creusot/` and executables are stored in `~/.local/share/creusot/`.
 
 # Upgrading Creusot 
 

cargo-creusot/src/main.rs

@@ -3,6 +3,7 @@ use creusot_args::{options::*, CREUSOT_RUSTC_ARGS};
 use creusot_setup as setup;
 use std::{
     env,
+    path::PathBuf,
     process::{exit, Command},
 };
 use tempdir::TempDir;
@@ -20,11 +21,20 @@ fn main() -> Result<()> {
     let cargs = CargoCreusotArgs::parse_from(std::env::args().skip(1));
 
     match cargs.subcommand {
-        None => creusot(None, cargs.options, cargs.cargo_flags),
-        Some(Creusot(subcmd)) => creusot(Some(subcmd), cargs.options, cargs.cargo_flags),
+        None => creusot(None, cargs.options, cargs.creusot_rustc, cargs.cargo_flags),
+        Some(Creusot(subcmd)) => {
+            creusot(Some(subcmd), cargs.options, cargs.creusot_rustc, cargs.cargo_flags)
+        }
         Some(Setup { command: SetupSubCommand::Status }) => setup::status(),
         Some(Setup {
-            command: SetupSubCommand::Install { provers_parallelism, external, no_check_version },
+            command:
+                SetupSubCommand::Install {
+                    provers_parallelism,
+                    external,
+                    no_check_version,
+                    only_creusot_rustc,
+                    skip_creusot_rustc,
+                },
         }) => {
             let extflag =
                 |name| setup::ExternalFlag { check_version: !no_check_version.contains(&name) };
@@ -40,6 +50,8 @@ fn main() -> Result<()> {
                 z3: managedflag(SetupTool::Z3, SetupManagedTool::Z3),
                 cvc4: managedflag(SetupTool::CVC4, SetupManagedTool::CVC4),
                 cvc5: managedflag(SetupTool::CVC5, SetupManagedTool::CVC5),
+                only_creusot_rustc,
+                skip_creusot_rustc,
             };
             setup::install(flags)
         }
@@ -53,6 +65,7 @@ fn main() -> Result<()> {
 fn creusot(
     subcmd: Option<CreusotSubCommand>,
     options: CommonOptions,
+    creusot_rustc: Option<PathBuf>,
     cargo_flags: Vec<String>,
 ) -> Result<()> {
     let (coma_src, coma_glob) = get_coma(&options);
@@ -83,7 +96,7 @@ fn creusot(
         subcommand: creusot_rustc_subcmd.clone(),
     };
 
-    invoke_cargo(&creusot_args, cargo_flags);
+    invoke_cargo(&creusot_args, creusot_rustc, cargo_flags);
 
     if let Some((mode, coma_src, args)) = launch_why3 {
         let mut coma_files = vec![coma_src];
@@ -113,11 +126,7 @@ fn creusot(
     Ok(())
 }
 
-fn invoke_cargo(args: &CreusotArgs, cargo_flags: Vec<String>) {
-    let creusot_rustc_path = std::env::current_exe()
-        .expect("current executable path invalid")
-        .with_file_name("creusot-rustc");
-
+fn invoke_cargo(args: &CreusotArgs, creusot_rustc: Option<PathBuf>, cargo_flags: Vec<String>) {
     let cargo_path = env::var("CARGO_PATH").unwrap_or_else(|_| "cargo".to_string());
     let cargo_cmd = match &args.subcommand {
         Some(CreusotSubCommand::Doc { .. }) => "doc",
@@ -129,8 +138,19 @@ fn invoke_cargo(args: &CreusotArgs, cargo_flags: Vec<String>) {
             }
         }
     };
-    let toolchain = toolchain_channel()
-        .expect("Expected `cargo-creusot` to be built with a valid toolchain file");
+    let toolchain = setup::toolchain_channel();
+    let creusot_rustc_path = match creusot_rustc {
+        Some(path) => path,
+        None => setup::toolchain_dir(&setup::get_data_dir().unwrap(), &toolchain)
+            .join("bin")
+            .join("creusot-rustc"),
+    };
+    // creusot_rustc binary exists
+    if !creusot_rustc_path.exists() {
+        eprintln!("creusot-rustc not found (expected at {creusot_rustc_path:?})");
+        eprintln!("Run 'cargo creusot setup install' in the source directory of Creusot to install creusot-rustc");
+        exit(1);
+    }
     let mut cmd = Command::new(cargo_path);
     cmd.arg(format!("+{toolchain}"))
         .arg(cargo_cmd)
@@ -173,16 +193,13 @@ fn invoke_cargo(args: &CreusotArgs, cargo_flags: Vec<String>) {
     }
 }
 
-fn toolchain_channel() -> Option<String> {
-    let toolchain: toml::Value = toml::from_str(include_str!("../../rust-toolchain")).ok()?;
-    let channel = toolchain["toolchain"]["channel"].as_str()?;
-    Some(channel.into())
-}
-
 #[derive(Debug, Parser)]
 pub struct CargoCreusotArgs {
     #[clap(flatten)]
     pub options: CommonOptions,
+    /// Path to creusot-rustc (for testing)
+    #[clap(long, value_name = "PATH")]
+    pub creusot_rustc: Option<PathBuf>,
     /// Subcommand: why3, setup
     #[command(subcommand)]
     pub subcommand: Option<CargoCreusotSubCommand>,
@@ -228,6 +245,12 @@ pub enum SetupSubCommand {
         /// 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>,
+        /// Only install creusot-rustc
+        #[arg(long)]
+        only_creusot_rustc: bool,
+        /// Skip installing creusot-rustc
+        #[arg(long, conflicts_with = "only_creusot_rustc")]
+        skip_creusot_rustc: bool,
     },
 }
 

creusot-setup/src/lib.rs

@@ -1,6 +1,6 @@
 use anyhow::{anyhow, bail, Context};
 use directories::ProjectDirs;
-use std::{fmt, fs, path::PathBuf};
+use std::{fmt, fs, path::PathBuf, process::Command};
 
 mod config;
 mod tools;
@@ -43,6 +43,10 @@ fn get_config_paths() -> anyhow::Result<CfgPaths> {
     })
 }
 
+pub fn get_data_dir() -> anyhow::Result<PathBuf> {
+    get_config_paths().map(|config| config.data_dir)
+}
+
 pub fn get_why3_config_file() -> anyhow::Result<PathBuf> {
     get_config_paths().map(|config| config.why3_config_file)
 }
@@ -212,11 +216,22 @@ pub struct InstallFlags {
     pub z3: ManagedFlag,
     pub cvc4: ManagedFlag,
     pub cvc5: ManagedFlag,
+    pub only_creusot_rustc: bool,
+    pub skip_creusot_rustc: bool,
 }
 
 pub fn install(flags: InstallFlags) -> anyhow::Result<()> {
     let paths = get_config_paths()?;
+    if !flags.skip_creusot_rustc {
+        install_creusot_rustc(&paths)?;
+    }
+    if !flags.only_creusot_rustc {
+        install_tools(&paths, flags)?;
+    }
+    Ok(())
+}
 
+fn install_tools(paths: &CfgPaths, flags: InstallFlags) -> anyhow::Result<()> {
     // helpers to generate the ExternalTool/ManagedTool config sections
 
     let getpath = |bin: Binary| -> anyhow::Result<PathBuf> {
@@ -276,7 +291,7 @@ pub fn install(flags: InstallFlags) -> anyhow::Result<()> {
 fn apply_config(paths: &CfgPaths, cfg: &Config) -> anyhow::Result<()> {
     // erase any previous existing config (but not the cache)
     let _ = fs::remove_dir_all(&paths.config_dir);
-    let _ = fs::remove_dir_all(&paths.data_dir);
+    let _ = fs::remove_dir_all(&paths.data_dir.join("bin"));
 
     // create directories
     fs::create_dir_all(&paths.config_dir)?;
@@ -321,3 +336,41 @@ fn apply_config(paths: &CfgPaths, cfg: &Config) -> anyhow::Result<()> {
     why3find_install(&cfg.why3find.path)?;
     Ok(())
 }
+
+fn install_creusot_rustc(cfg: &CfgPaths) -> anyhow::Result<()> {
+    println! {"Installing creusot-rustc..."};
+    let toolchain = toolchain_channel();
+    // The `toolchain` hard-coded in toolchain_channel must match the active toolchain
+    let active_toolchain = active_toolchain();
+    if !active_toolchain.starts_with(&toolchain) {
+        // Ignore the target triple in the full toolchain identifier
+        panic!("Active toolchain: {active_toolchain}; expected: {toolchain}; cargo-creusot is probably out of date.");
+    }
+    let _ = fs::remove_dir_all(&cfg.data_dir.join("toolchains"));
+    // Usually ~/.local/share/creusot/toolchains/nightly-YYYY-MM-DD/
+    let toolchain_dir =
+        &toolchain_dir(&cfg.data_dir, &toolchain).into_os_string().into_string().unwrap();
+    let mut cmd = Command::new("cargo");
+    cmd.args(["install", "--path", "creusot-rustc", "--root", toolchain_dir, "--quiet"]);
+    if !cmd.status()?.success() {
+        bail!("Failed to install creusot-rustc")
+    }
+    Ok(())
+}
+
+fn active_toolchain() -> String {
+    let output = Command::new("rustup").args(&["show", "active-toolchain"]).output().unwrap();
+    let output = String::from_utf8(output.stdout).unwrap();
+    let toolchain = output.split(" ").next().unwrap();
+    toolchain.to_string()
+}
+
+pub fn toolchain_dir(data_dir: &PathBuf, toolchain: &str) -> PathBuf {
+    data_dir.join("toolchains").join(toolchain)
+}
+
+pub fn toolchain_channel() -> String {
+    let toolchain: toml::Value = toml::from_str(include_str!("../../rust-toolchain"))
+        .expect("Expected `cargo-creusot` to be built with a valid toolchain file");
+    toolchain["toolchain"]["channel"].as_str().unwrap().to_string()
+}

creusot/tests/creusot-contracts.rs

@@ -27,7 +27,7 @@ fn main() {
         args.force_color = true;
     }
     // Build creusot-rustc to make it available to cargo-creusot
-    let _ = escargot::CargoBuild::new()
+    let creusot_rustc = escargot::CargoBuild::new()
         .bin("creusot-rustc")
         .current_release()
         .manifest_path("../creusot-rustc/Cargo.toml")
@@ -52,6 +52,8 @@ fn main() {
         .unwrap();
     cargo_creusot.current_dir(&base_path).args([
         "creusot",
+        "--creusot-rustc",
+        creusot_rustc.path().to_str().unwrap(),
         "--stdout",
         "--export-metadata=false",
         "--span-mode=relative",

creusot/tests/ui.rs

@@ -58,6 +58,8 @@ fn main() {
     let mut metadata_file = cargo_creusot;
     metadata_file.current_dir(base_path);
     metadata_file.arg("creusot").args(&[
+        "--creusot-rustc".as_ref(),
+        creusot_rustc.path().as_os_str(),
         "--metadata-path".as_ref(),
         temp_file.as_os_str(),
         "--output-file=/dev/null".as_ref(),