Refactor handling of why3 paths in cargo-creusot and tests

- Remove library compoenent of creusot-dev-config; test suite depends on creusot-setup instead
- Rename `status_for_creusot` and `CreusotFlags` to `creusot_paths` and `Paths`

cargo-creusot/src/main.rs

@@ -75,11 +75,11 @@ fn creusot(
 
     // Default output_dir to "." if not specified
     let include_dir = Some(options.output_dir.clone().unwrap_or(".".into()));
-    let config_args = setup::status_for_creusot()?;
+    let paths = setup::creusot_paths()?;
     let creusot_args = CreusotArgs {
         options,
-        why3_path: config_args.why3_path.clone(),
-        why3_config_file: config_args.why3_config.clone(),
+        why3_path: paths.why3.clone(),
+        why3_config_file: paths.why3.clone(),
         subcommand: creusot_rustc_subcmd.clone(),
     };
 
@@ -98,8 +98,8 @@ fn creusot(
 
         // why3 configuration
         let why3 = Why3Launcher {
-            why3_path: config_args.why3_path,
-            config_file: config_args.why3_config,
+            why3_path: paths.why3,
+            config_file: paths.why3_config,
             mode,
             include_dir,
             coma_files,

cargo-creusot/src/why3find_wrapper.rs

@@ -1,6 +1,6 @@
 use anyhow::Result;
 use clap::*;
-use creusot_setup::{status_for_creusot, CreusotFlags, PROVERS};
+use creusot_setup::{creusot_paths, Paths, 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>, paths: &CreusotFlags) -> Result<()> {
-    let mut why3find = Command::new(&paths.why3find_path);
+fn raw_config(args: &Vec<String>, paths: &Paths) -> Result<()> {
+    let mut why3find = Command::new(&paths.why3find);
     why3find
         .arg("config")
         .arg("--quiet")
@@ -51,8 +51,8 @@ fn raw_config(args: &Vec<String>, paths: &CreusotFlags) -> Result<()> {
         .map(|_| ())
 }
 
-fn raw_prove(args: ProveArgs, paths: &CreusotFlags) -> Result<()> {
-    let mut why3find = Command::new(&paths.why3find_path);
+fn raw_prove(args: ProveArgs, paths: &Paths) -> Result<()> {
+    let mut why3find = Command::new(&paths.why3find);
     why3find.arg("prove");
     if args.ide {
         why3find.arg("-i");
@@ -63,7 +63,7 @@ fn raw_prove(args: ProveArgs, paths: &CreusotFlags) -> Result<()> {
     for file in files {
         why3find.arg(file);
     }
-    if let Some(why3_path) = paths.why3_path.parent() {
+    if let Some(why3_path) = paths.why3.parent() {
         let mut path = why3_path.to_path_buf().into_os_string();
         path.push(":");
         path.push(std::env::var("PATH").unwrap());
@@ -79,12 +79,12 @@ fn raw_prove(args: ProveArgs, paths: &CreusotFlags) -> Result<()> {
 }
 
 pub fn why3find_config(args: ConfigArgs) -> Result<()> {
-    let paths = status_for_creusot()?;
+    let paths = creusot_paths()?;
     raw_config(&args.args, &paths)
 }
 
 pub fn why3find_prove(args: ProveArgs) -> Result<()> {
-    let paths = status_for_creusot()?;
+    let paths = creusot_paths()?;
     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`."));
     }

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

@@ -3,7 +3,7 @@ use std::{env, path::PathBuf};
 use which::which;
 
 pub fn main() -> anyhow::Result<()> {
-    let paths = creusot_dev_config::paths()?;
+    let paths = creusot_setup::creusot_paths()?;
 
     let why3_path = which(&paths.why3)?;
     eprintln!("Using Why3 at: {}", &why3_path.display());

creusot-setup/src/lib.rs

@@ -156,16 +156,15 @@ pub fn status() -> anyhow::Result<()> {
     Ok(())
 }
 
-pub struct CreusotFlags {
-    pub why3_path: PathBuf,
-    pub why3find_path: PathBuf,
+pub struct Paths {
+    pub why3: PathBuf,
+    pub why3find: PathBuf,
     pub why3_config: PathBuf,
 }
 
-/// compute the flags to pass to creusot-rustc.
-/// fail if the installation is not in an acceptable state, which means we will
-/// stop there and do not attempt launching creusot-rustc.
-pub fn status_for_creusot() -> anyhow::Result<CreusotFlags> {
+/// Get paths to tools from Config.toml.
+/// fail if the installation is not in an acceptable state
+pub fn creusot_paths() -> anyhow::Result<Paths> {
     let paths = get_config_paths()?;
     match Config::read_from_file(&paths.config_file) {
         Err(err) => bail!(
@@ -187,9 +186,9 @@ pub fn status_for_creusot() -> anyhow::Result<CreusotFlags> {
                      to diagnostic and fix the issue(s)"
                 )
             }
-            Ok(CreusotFlags {
-                why3_path: cfg.why3.path.to_path_buf(),
-                why3find_path: cfg.why3find.path.to_path_buf(),
+            Ok(Paths {
+                why3: cfg.why3.path.to_path_buf(),
+                why3find: cfg.why3find.path.to_path_buf(),
                 why3_config: paths.why3_config_file,
             })
         }

creusot/Cargo.toml

@@ -33,7 +33,7 @@ termcolor = "1.1"
 arraydeque = "0.4"
 creusot-contracts = { path = "../creusot-contracts", features = ["typechecker"] }
 escargot = { version = "0.5" }
-creusot-dev-config = { path = "../creusot-dev-config" }
+creusot-setup = { path = "../creusot-setup" }
 
 [[test]]
 name = "ui"

creusot/tests/ui.rs

@@ -81,7 +81,7 @@ fn run_creusot(
     base_path.push("creusot");
     base_path.push("debug");
 
-    let config_paths = creusot_dev_config::paths().unwrap();
+    let config_paths = creusot_setup::creusot_paths().unwrap();
 
     let creusot_contract_path = base_path.join("libcreusot_contracts.rlib");
     let creusot_contract_path =

why3tests/Cargo.toml

@@ -12,7 +12,7 @@ termcolor = "1.1"
 git2 = "0.14.4"
 clap = { version = "4.2", features = ["env", "derive"]}
 roxmltree = "0.18.0"
-creusot-dev-config = { path = "../creusot-dev-config" }
+creusot-setup = { path = "../creusot-setup" }
 
 [[test]]
 test = false
@@ -23,4 +23,3 @@ harness = false
 test = false
 name = "session_stats"
 harness = false
-

why3tests/tests/why3.rs

@@ -5,7 +5,7 @@ use std::{
     fs::File,
     io::{BufRead, BufReader, Write},
     path::PathBuf,
-    process::exit,
+    process::{exit, Command},
 };
 use termcolor::*;
 
@@ -92,7 +92,9 @@ fn main() {
         sessionfile.push("why3session.xml");
 
         let output;
-        let mut command = creusot_dev_config::why3_command().unwrap();
+        let paths = creusot_setup::creusot_paths().unwrap();
+        let mut command = Command::new(paths.why3.clone());
+        command.arg("-C").arg(paths.why3_config);
         command.arg("--warn-off=unused_variable");
         command.arg("--warn-off=clone_not_abstract");
         command.arg("--warn-off=axiom_abstract");