diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index c65283f41..bd4358fda 100644 --- a/.github/workflows/rust.yml +++ b/.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: | diff --git a/README.md b/README.md index 235492a68..1441e00c7 100644 --- a/README.md +++ b/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 diff --git a/cargo-creusot/src/main.rs b/cargo-creusot/src/main.rs index e0fa417bd..c2939d336 100644 --- a/cargo-creusot/src/main.rs +++ b/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, options: CommonOptions, + creusot_rustc: Option, cargo_flags: Vec, ) -> 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) { - 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, cargo_flags: Vec) { 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) { } } }; - 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) { } } -fn toolchain_channel() -> Option { - 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, /// Subcommand: why3, setup #[command(subcommand)] pub subcommand: Option, @@ -228,6 +245,12 @@ pub enum SetupSubCommand { /// Do not error if 's version does not match the one expected by creusot #[arg(long, value_name = "TOOL")] no_check_version: Vec, + /// 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, }, } diff --git a/creusot-setup/src/lib.rs b/creusot-setup/src/lib.rs index 7e95b8adc..4d9bb767c 100644 --- a/creusot-setup/src/lib.rs +++ b/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 { }) } +pub fn get_data_dir() -> anyhow::Result { + get_config_paths().map(|config| config.data_dir) +} + pub fn get_why3_config_file() -> anyhow::Result { 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 { @@ -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() +} diff --git a/creusot/tests/creusot-contracts.rs b/creusot/tests/creusot-contracts.rs index b1302f59a..cf944d8ff 100644 --- a/creusot/tests/creusot-contracts.rs +++ b/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", diff --git a/creusot/tests/ui.rs b/creusot/tests/ui.rs index c623d2675..be78668c3 100644 --- a/creusot/tests/ui.rs +++ b/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(),