Replace the 'dev-why3' binary by 'dev-env' which sets shell environme…

…nt variables

This is strictly more flexible: instead of requiring the use of a
custom why3 wrapper, we provide a way to setup a shell environment
where `why3` resolves to the correct binary, and WHY3CONFIG indicates
the config file.

This will then "just work" for binaries such as why3_tools that link
to the why3 api, since they will pick up WHY3CONFIG.

HACKING.md

@@ -5,9 +5,9 @@ working on the Creusot codebase.
 
 ## Setup
 
-On top of the usual Rust/Cargo workflow, the "Creusot developer setup" requires
-a working Why3 in order to run the testsuite and update tests proofs. You have
-two choices:
+The "Creusot developer setup" sometimes requires more flexibility in how it
+looks up why3 and related solvers, compared to the standard "user" workflow
+provided by `cargo creusot setup install`. You have two options:
 
 - **By default** the testsuite will use the global Creusot configuration managed
   by `cargo creusot setup`. You first need to have successfully run `cargo
@@ -61,17 +61,21 @@ If the proof of a test is broken (e.g.
 ./ide creusot/tests/should_succeed/cell/01
 ```
 
-## Calling why3
+## Calling why3 & why3_tools: shell environment setup
 
-To invoke why3 robustly (manually or in scripts), we provide a wrapper that will
-lookup the why3 path and config according to the logic described in **Setup**
-above.
+To invoke why3 (manually or in scripts) with the same binary/configuration as
+setup by `cargo creusot setup`, one needs to setup a shell environment with the
+correct PATH and environment variables.
 
-To invoke why3 this way, run:
+To do so, we provide the following command:
 ```
-cargo run --bin dev-why3 -- <arguments_to_why3...>
+eval $(cargo run --bin dev-env)
 ```
 
+After that, the `why3` binary in PATH will be the one configured by
+`cargo creusot setup`, using the adequate configuration file (through the
+`WHY3CONFIG` environment variable).
+
 ## Upgrading the revision of Why3 used by Creusot
 
 Edit `creusot-deps.opam` to use the hash of the git commit of the latest commit

creusot-dev-config/Cargo.toml

@@ -6,3 +6,4 @@ edition = "2021"
 [dependencies]
 creusot-setup = { path = "../creusot-setup" }
 anyhow = "1.0"
+which = "6.0"

creusot-dev-config/src/bin/dev-env.rs

@@ -0,0 +1,26 @@
+use anyhow::anyhow;
+use std::{env, path::PathBuf};
+use which::which;
+
+pub fn main() -> anyhow::Result<()> {
+    let paths = creusot_dev_config::paths()?;
+
+    let why3_path = which(&paths.why3)?;
+    eprintln!("Using Why3 at: {}", &why3_path.display());
+    let why3_dir = PathBuf::from(&why3_path.parent().ok_or(anyhow!("finding why3's location"))?);
+    let new_path = match env::var_os("PATH") {
+        Some(path) => {
+            let mut path_elts = env::split_paths(&path).collect::<Vec<_>>();
+            path_elts.insert(0, why3_dir);
+            env::join_paths(path_elts)?
+        }
+        None => env::join_paths([why3_dir].iter())?,
+    };
+    println!("PATH={:?}; export PATH;", &new_path);
+
+    if let Some(config) = &paths.why3_config {
+        eprintln!("Using Why3 config at: {}", config.display());
+        println!("WHY3CONFIG='{}'; export WHY3CONFIG;", &config.display());
+    }
+    Ok(())
+}

creusot-dev-config/src/lib.rs

@@ -10,7 +10,7 @@ use std::{path::PathBuf, process::Command};
 /// - otherwise, in the global config repository used by creusot setup
 
 pub fn custom_config_dir() -> Option<PathBuf> {
-    let local_config = PathBuf::from("../.creusot-config");
+    let local_config = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("../.creusot-config");
     if local_config.is_dir() {
         Some(std::fs::canonicalize(local_config).unwrap())
     } else {

ide

@@ -1,4 +1,5 @@
 #!/usr/bin/env bash
 
 SCRIPTPATH=$(dirname "$BASH_SOURCE")
-cargo run --bin dev-why3 -- --warn-off=unused_variable --warn-off=clone_not_abstract --warn-off=axiom_abstract ide -L $SCRIPTPATH/prelude $@
+eval $(cargo run --bin dev-env)
+why3 --warn-off=unused_variable --warn-off=clone_not_abstract --warn-off=axiom_abstract ide -L $SCRIPTPATH/prelude $@