Install creusot-rustc in a toolchain-dependent location

Problem: creusot-rustc is dynamically linked with rustc_driver, so it can't be run
directly from the command line because it can't find its dependencies alone.

Solution: Putting it in a special directory controlled by Creusot:
1. removes it from $PATH, suppressing the temptation to run it from the command line
2. allows cargo-creusot to detect incomplete upgrades (this prevents
   an obscure dynlink error if one updates the toolchain that creusot depends
   on and only reinstalls one of cargo-creusot or creusot-rustc).

The installation of creusot-rustc is now handled by `cargo creusot setup install`.

.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:
@@ -156,8 +152,9 @@ jobs:
         name: why3-deps
     - name: unpack why3 and why3find
       run: tar -xzf _opam.tar.gz
-    - name: setup creusot
+    - name: Install Creusot
       run: |
+        cargo install --path cargo-creusot
         # 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

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

@@ -114,10 +114,6 @@ fn creusot(
 }
 
 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");
-
     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 +125,16 @@ 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 = 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,12 +177,6 @@ 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)]

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)
 }
@@ -216,7 +220,11 @@ pub struct InstallFlags {
 
 pub fn install(flags: InstallFlags) -> anyhow::Result<()> {
     let paths = get_config_paths()?;
+    install_tools(&paths, flags)?; // install_tools clears the data_dir
+    install_creusot_rustc(&paths)
+}
 
+pub fn install_tools(paths: &CfgPaths, flags: InstallFlags) -> anyhow::Result<()> {
     // helpers to generate the ExternalTool/ManagedTool config sections
 
     let getpath = |bin: Binary| -> anyhow::Result<PathBuf> {
@@ -321,3 +329,40 @@ 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.");
+    }
+    // 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()
+}