Merge pull request #1276 from creusot-rs/why3find-path

Use path to why3find stored in Creusot configuration

.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

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<String>, why3_config_file: &PathBuf) -> Result<()> {
-    let mut why3find = Command::new("why3find");
+fn raw_config(args: &Vec<String>, paths: &CreusotFlags) -> Result<()> {
+    let mut why3find = Command::new(&paths.why3find_path);
     why3find
         .arg("config")
         .arg("--quiet")
@@ -43,16 +43,16 @@ fn raw_config(args: &Vec<String>, 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()
         .map_err(|e| anyhow::Error::new(e).context("why3find config failed"))
         .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`."));
     }

ci/creusot-config-dummy.toml

@@ -1,4 +1,4 @@
-version = 5
+version = 6
 provers_parallelism = 1
 
 [why3]

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)]

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<CreusotFlags> {
             }
             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(())
 }

creusot-setup/src/tools.rs

@@ -385,6 +385,7 @@ fn run(cmd: &mut Command) -> anyhow::Result<std::process::Output> {
     })
 }
 
-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(())
 }