setup: slight refactoring of the why3 config file generation

creusot-rs · Mar 9, 2024 · 7cfb75b · 7cfb75b
1 parent 515703d
commit 7cfb75b
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 8 deletions.
diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
@@ -84,7 +84,7 @@ jobs:
         cargo run --bin cargo-creusot creusot setup install
         echo -e "\n>> ~/.config/creusot/Config.toml:\n"
         cat ~/.config/creusot/Config.toml
-        echo -e "\n>> ~/.config/creusot/.why3.conf:\n"
-        cat ~/.config/creusot/.why3.conf
+        echo -e "\n>> ~/.config/creusot/why3.conf:\n"
+        cat ~/.config/creusot/why3.conf
     - run: cargo test --test why3 "" -- --replay=none --diff-from=origin/master
     - run: cargo test --test why3 "" -- --skip-unstable
diff --git a/creusot-setup/src/lib.rs b/creusot-setup/src/lib.rs
@@ -13,9 +13,11 @@ use tools::*;
 use tools_versions_urls::*;
 use ToolsConfig::*;
 
+// CAUTION: on MacOS, [config_dir] and [data_dir] are in fact the same directory
 struct CfgPaths {
     config_dir: PathBuf,
     config_file: PathBuf,
+    why3_config_file: PathBuf,
     data_dir: PathBuf,
     bin_subdir: PathBuf,
     cache_dir: PathBuf,
@@ -32,6 +34,7 @@ fn get_config_paths(custom_config_dir: &Option<PathBuf>) -> anyhow::Result<CfgPa
     Ok(CfgPaths {
         config_dir: PathBuf::from(config_dir),
         config_file: config_dir.join("Config.toml"),
+        why3_config_file: config_dir.join("why3.conf"),
         data_dir: PathBuf::from(dirs.data_dir()),
         bin_subdir: dirs.data_dir().join("bin"),
         cache_dir: PathBuf::from(dirs.cache_dir()),
@@ -183,7 +186,7 @@ pub fn status_for_creusot(custom_config_dir: &Option<PathBuf>) -> anyhow::Result
                     }
                     Ok(CreusotFlags {
                         why3_path: why3_path.to_path_buf(),
-                        why3_config: Some(paths.config_dir.join(".why3.conf")),
+                        why3_config: Some(paths.why3_config_file),
                     })
                 }
             }
@@ -307,7 +310,7 @@ fn managed_download_and_generate_config(
     symlink_file(altergo_path, &paths.bin_subdir.join(ALTERGO.binary_name))?;
 
     // generate the corresponding .why3.conf
-    generate_why3_conf(why3_path, &paths.bin_subdir, &paths.config_dir)?;
+    generate_why3_conf(why3_path, &paths.bin_subdir, &paths.why3_config_file)?;
 
     // write the config file
     let config = Config {

diff --git a/creusot-setup/src/tools.rs b/creusot-setup/src/tools.rs
@@ -173,13 +173,22 @@ fn detect_why3_version(why3: &Path) -> Option<String> {
     })
 }
 
-pub fn generate_why3_conf(why3_path: &Path, bin_dir: &Path, dest_dir: &Path) -> anyhow::Result<()> {
+pub fn generate_why3_conf(
+    why3_path: &Path,
+    bin_dir: &Path,
+    dest_file: &Path,
+) -> anyhow::Result<()> {
     println!("Generating a fresh why3 configuration...");
-    let dest_file = dest_dir.join(".why3.conf");
-    let _ = fs::remove_file(dest_file);
+    // create or empty the destination file to avoid getting a warning from why3
+    // because it doesn't exist
+    {
+        let _ = fs::File::create(&dest_file);
+    }
     let status = Command::new(why3_path)
+        .arg("-C")
+        .arg(&dest_file)
         .args(["config", "detect"])
-        .envs([("PATH", bin_dir), ("HOME", dest_dir)])
+        .envs([("PATH", bin_dir)])
         .status()
         .context("launching 'why3 config detect' on downloaded solvers")?;
     if !status.success() {