diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 3b57b46c9a..367969f06b 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -150,16 +150,18 @@ 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') }} - - run: cargo creusot setup install - if: steps.cache-creusot-setup.outputs.cache-hit != 'true' - name: download why3 and why3find uses: actions/download-artifact@v4 with: name: why3-deps - - name: setup opam PATH + - name: unpack why3 and why3find + run: tar -xzf _opam.tar.gz + - name: setup creusot run: | - tar -xzf _opam.tar.gz - echo /home/runner/work/creusot/creusot/_opam/bin >> $GITHUB_PATH + # 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 + if: steps.cache-creusot-setup.outputs.cache-hit != 'true' - name: test cargo creusot new run: | set -x diff --git a/cargo-creusot/src/why3find_wrapper.rs b/cargo-creusot/src/why3find_wrapper.rs index 688aebe007..2826f9fd61 100644 --- a/cargo-creusot/src/why3find_wrapper.rs +++ b/cargo-creusot/src/why3find_wrapper.rs @@ -1,6 +1,6 @@ use anyhow::Result; use clap::*; -use creusot_setup::{get_why3_config_file, PROVERS}; +use creusot_setup::{status_for_creusot, CreusotFlags, PROVERS}; use std::{ path::{Path, PathBuf}, process::{Command, Stdio}, @@ -27,8 +27,8 @@ fn why3find_json_exists() -> bool { Path::new("why3find.json").exists() } -fn raw_config(args: &Vec, why3_config_file: &PathBuf) -> Result<()> { - let mut why3find = Command::new("why3find"); +fn raw_config(args: &Vec, paths: &CreusotFlags) -> Result<()> { + let mut why3find = Command::new(&paths.why3find_path); why3find .arg("config") .arg("--quiet") @@ -43,7 +43,7 @@ fn raw_config(args: &Vec, why3_config_file: &PathBuf) -> Result<()> { why3find.arg(arg); } why3find - .env("WHY3CONFIG", &why3_config_file) + .env("WHY3CONFIG", &paths.why3_config) .stdout(Stdio::inherit()) .stderr(Stdio::inherit()) .status() @@ -51,8 +51,8 @@ fn raw_config(args: &Vec, why3_config_file: &PathBuf) -> Result<()> { .map(|_| ()) } -fn raw_prove(args: ProveArgs, why3_config_file: &PathBuf) -> Result<()> { - let mut why3find = Command::new("why3find"); +fn raw_prove(args: ProveArgs, paths: &CreusotFlags) -> Result<()> { + let mut why3find = Command::new(&paths.why3find_path); why3find.arg("prove"); if args.ide { why3find.arg("-i"); @@ -63,8 +63,14 @@ fn raw_prove(args: ProveArgs, why3_config_file: &PathBuf) -> Result<()> { for file in files { why3find.arg(file); } + if let Some(why3_path) = paths.why3_path.parent() { + let mut path = why3_path.to_path_buf().into_os_string(); + path.push(":"); + path.push(std::env::var("PATH").unwrap()); + why3find.env("PATH", path); + } why3find - .env("WHY3CONFIG", &why3_config_file) + .env("WHY3CONFIG", &paths.why3_config) .stdout(Stdio::inherit()) .stderr(Stdio::inherit()) .status() @@ -73,12 +79,12 @@ fn raw_prove(args: ProveArgs, why3_config_file: &PathBuf) -> Result<()> { } pub fn why3find_config(args: ConfigArgs) -> Result<()> { - let paths = get_why3_config_file()?; + let paths = status_for_creusot()?; raw_config(&args.args, &paths) } pub fn why3find_prove(args: ProveArgs) -> Result<()> { - let paths = get_why3_config_file()?; + let paths = status_for_creusot()?; if !why3find_json_exists() { return Err(anyhow::anyhow!("why3find.json not found. Perhaps you are in the wrong directory, or you need to run `cargo creusot config`.")); } diff --git a/ci/creusot-config-dummy.toml b/ci/creusot-config-dummy.toml index 94e8a84fb4..7ed2afde4e 100644 --- a/ci/creusot-config-dummy.toml +++ b/ci/creusot-config-dummy.toml @@ -1,4 +1,4 @@ -version = 5 +version = 6 provers_parallelism = 1 [why3] diff --git a/creusot-setup/src/config.rs b/creusot-setup/src/config.rs index ae91444a4d..4e21f7a5c4 100644 --- a/creusot-setup/src/config.rs +++ b/creusot-setup/src/config.rs @@ -8,7 +8,7 @@ use std::{ // the goal is to avoid silently mis-interpreting a past or future version of // the config file whenever its format changes. // NOTE: update ci/creusot-config-dummy.toml whenever you change this. -pub const CURRENT_CONFIG_VERSION: i64 = 5; +pub const CURRENT_CONFIG_VERSION: i64 = 6; // bump CURRENT_CONFIG_VERSION if you change this definition #[derive(Serialize, Deserialize)] diff --git a/creusot-setup/src/lib.rs b/creusot-setup/src/lib.rs index 423d67f9ac..9aaa95d279 100644 --- a/creusot-setup/src/lib.rs +++ b/creusot-setup/src/lib.rs @@ -158,6 +158,7 @@ pub fn status() -> anyhow::Result<()> { pub struct CreusotFlags { pub why3_path: PathBuf, + pub why3find_path: PathBuf, pub why3_config: PathBuf, } @@ -188,6 +189,7 @@ pub fn status_for_creusot() -> anyhow::Result { } Ok(CreusotFlags { why3_path: cfg.why3.path.to_path_buf(), + why3find_path: cfg.why3find.path.to_path_buf(), why3_config: paths.why3_config_file, }) } @@ -317,6 +319,6 @@ fn apply_config(paths: &CfgPaths, cfg: &Config) -> anyhow::Result<()> { cfg.write_to_file(&paths.config_file)?; // install the why3find package - why3find_install(); + why3find_install(&cfg.why3find.path)?; Ok(()) } diff --git a/creusot-setup/src/tools.rs b/creusot-setup/src/tools.rs index bf65e52753..365dd7d1e2 100644 --- a/creusot-setup/src/tools.rs +++ b/creusot-setup/src/tools.rs @@ -385,6 +385,7 @@ fn run(cmd: &mut Command) -> anyhow::Result { }) } -pub fn why3find_install() { - Command::new("why3find").args(["install", "--global", "prelude"]).status().unwrap(); +pub fn why3find_install(why3find: &PathBuf) -> anyhow::Result<()> { + Command::new(why3find).args(["install", "--global", "prelude"]).status()?; + Ok(()) }