Merge pull request #1270 from creusot-rs/missing-tool

creusot-setup: Clarify error about whether a tool is missing or has the wrong version

creusot-setup/src/lib.rs

@@ -52,20 +52,20 @@ pub fn get_why3_config_file() -> anyhow::Result<PathBuf> {
 struct Issue {
     error: bool,
     tool: String,
-    cur_version: Option<String>,
+    cur_version: anyhow::Result<String>,
     expected_version: String,
     builtin_tool: bool,
 }
 
 impl fmt::Display for Issue {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         let Issue { error, tool, cur_version, expected_version, builtin_tool: _ } = self;
-        write!(
-            f,
-            "{}: {tool} has version {}, but version {expected_version} is expected",
-            (if *error { "Error" } else { "Warning" }),
-            cur_version.as_deref().unwrap_or("(not detected)")
-        )
+        let header = if *error { "Error" } else { "Warning" };
+        match cur_version {
+            Ok(cur_version) => write!(f,
+                "{header}: {tool} has version {cur_version}, expected version is {expected_version}"),
+            Err(err) => write!(f, "{header}: {err}"),
+        }
     }
 }
 
@@ -101,14 +101,15 @@ fn diagnostic_config(paths: &CfgPaths, config: &Config, check_builtins: bool) ->
 
     // check versions of binaries (passing --version) vs expected version
     for (bin, check_version, path, builtin_tool) in bins {
-        if let DetectedVersion::Bad(ver) = bin.detect_version(&path) {
-            issues.push(Issue {
+        match bin.detect_version(&path) {
+            Ok(version) if version == bin.version => continue,
+            bad_version => issues.push(Issue {
                 error: check_version,
                 tool: bin.display_name.to_owned(),
-                cur_version: ver,
+                cur_version: bad_version,
                 expected_version: bin.version.to_owned(),
                 builtin_tool,
-            })
+            }),
         }
     }
 

creusot-setup/src/tools.rs

@@ -87,7 +87,7 @@ pub struct Binary {
     pub display_name: &'static str,
     pub binary_name: &'static str,
     pub version: &'static str,
-    detect_version: fn(&Path) -> Option<String>,
+    detect_version: fn(&Path) -> anyhow::Result<String>,
 }
 
 // download a list [ManagedBinary]s
@@ -168,37 +168,31 @@ fn download_from_url_with_cache(
 
 // helpers: external binaries
 
-pub enum DetectedVersion {
-    Good,
-    Bad(Option<String>),
-}
-
 impl Binary {
     pub fn detect_path(&self) -> Option<PathBuf> {
         use which::which;
         which(self.binary_name).ok()
     }
 
-    pub fn detect_version(&self, path: &Path) -> DetectedVersion {
-        let detect_version = self.detect_version;
-        match detect_version(&path) {
-            None => DetectedVersion::Bad(None),
-            Some(ver) if ver != self.version => DetectedVersion::Bad(Some(ver)),
-            Some(_) => DetectedVersion::Good,
-        }
+    pub fn detect_version(&self, path: &Path) -> anyhow::Result<String> {
+        (self.detect_version)(path)
     }
 }
 
 // helpers: why3
 
-fn detect_why3_version(why3: &Path) -> Option<String> {
-    let output = Command::new(&why3).arg("--version").output().ok()?;
-    let version_full = String::from_utf8(output.stdout).ok()?;
-    let version = version_full.strip_prefix("Why3 platform, version ");
-    version.map(|ver| {
-        let parts: Vec<_> = ver.trim_end().split(|c| c == '.' || c == '+').collect();
-        String::from(&parts[..3].join("."))
-    })
+fn detect_why3_version(why3: &Path) -> anyhow::Result<String> {
+    let output = run(Command::new(&why3).arg("--version"))?;
+    let version_full = String::from_utf8(output.stdout)?;
+    match version_full.strip_prefix("Why3 platform, version ") {
+        Some(version) => {
+            let parts: Vec<_> = version.trim_end().split(|c| c == '.' || c == '+').collect();
+            Ok(String::from(&parts[..3].join(".")))
+        }
+        None => {
+            bail!("bad Why3 version: {}", version_full)
+        }
+    }
 }
 
 pub fn generate_why3_conf(
@@ -267,32 +261,37 @@ fn generate_strategy(f: &mut dyn Write) -> anyhow::Result<()> {
 
 // helpers: why3find
 
-pub fn detect_why3find_version(why3find: &Path) -> Option<String> {
-    let output = Command::new(&why3find).arg("--version").output().ok()?;
-    let version_full = String::from_utf8(output.stdout).ok()?;
-    let version = version_full.strip_prefix("why3find v");
-    version.map(|ver| {
-        let parts: Vec<_> = ver.trim_end().split(|c| c == '.' || c == '+').collect();
-        String::from(&parts[..3].join("."))
-    })
+pub fn detect_why3find_version(why3find: &Path) -> anyhow::Result<String> {
+    let output = run(Command::new(&why3find).arg("--version"))?;
+    let version_full = String::from_utf8(output.stdout)?;
+    match version_full.strip_prefix("why3find v") {
+        Some(version) => {
+            let parts: Vec<_> = version.trim_end().split(|c| c == '.' || c == '+').collect();
+            Ok(String::from(&parts[..3].join(".")))
+        }
+        None => bail!("bad Why3find version: {}", version_full),
+    }
 }
 
 // helpers: alt-ergo
 
-fn detect_altergo_version(altergo: &Path) -> Option<String> {
-    let output = Command::new(&altergo).arg("--version").output().ok()?;
-    let out_s = String::from_utf8(output.stdout).ok()?;
-    out_s.trim_end().strip_prefix("v").map(String::from)
+fn detect_altergo_version(altergo: &Path) -> anyhow::Result<String> {
+    let output = run(Command::new(&altergo).arg("--version"))?;
+    let version_full = String::from_utf8(output.stdout)?;
+    let version = version_full.trim_end().strip_prefix("v").map(String::from);
+    version.ok_or(anyhow!("bad Altergo version: {}", version_full))
 }
 
 // helpers: Z3
 
 // assumes a version string of the form: "Z3 version 4.12.4 - 64 bit"
-fn detect_z3_version(z3: &Path) -> Option<String> {
-    let output = Command::new(&z3).arg("--version").output().ok()?;
-    let out_s = String::from_utf8(output.stdout).ok()?;
-    let out_s = out_s.strip_prefix("Z3 version ")?;
-    out_s.split_ascii_whitespace().next().map(String::from)
+fn detect_z3_version(z3: &Path) -> anyhow::Result<String> {
+    let output = run(Command::new(&z3).arg("--version"))?;
+    let version_full = String::from_utf8(output.stdout)?;
+    let version = version_full
+        .strip_prefix("Z3 version ")
+        .and_then(|version| version.split_ascii_whitespace().next().map(String::from));
+    version.ok_or(anyhow!("bad Z3 version: {}", version_full))
 }
 
 // Z3 releases come as a .zip archive that includes many things. We are only
@@ -329,21 +328,25 @@ fn download_z3_from_url(
 // cvc4
 
 // assumes a version of the form: "This is CVC4 version 1.8 [git HEAD 52479010]\n....."
-fn detect_cvc4_version(cvc4: &Path) -> Option<String> {
-    let output = Command::new(&cvc4).arg("--version").output().ok()?;
-    let out_s = String::from_utf8(output.stdout).ok()?;
-    let out_s = out_s.strip_prefix("This is CVC4 version ")?;
-    out_s.split_ascii_whitespace().next().map(String::from)
+fn detect_cvc4_version(cvc4: &Path) -> anyhow::Result<String> {
+    let output = run(Command::new(&cvc4).arg("--version"))?;
+    let version_full = String::from_utf8(output.stdout)?;
+    let version = version_full
+        .strip_prefix("This is CVC4 version ")
+        .and_then(|version| version.split_ascii_whitespace().next().map(String::from));
+    version.ok_or(anyhow!("bad CVC4 version: {}", version_full))
 }
 
 // cvc5
 
 // assumes a version of the form: "This is cvc5 version 1.0.5 [git ...]\n....."
-fn detect_cvc5_version(cvc5: &Path) -> Option<String> {
-    let output = Command::new(&cvc5).arg("--version").output().ok()?;
-    let out_s = String::from_utf8(output.stdout).ok()?;
-    let out_s = out_s.strip_prefix("This is cvc5 version ")?;
-    out_s.split_ascii_whitespace().next().map(String::from)
+fn detect_cvc5_version(cvc5: &Path) -> anyhow::Result<String> {
+    let output = run(Command::new(&cvc5).arg("--version"))?;
+    let version_full = String::from_utf8(output.stdout)?;
+    let version = version_full
+        .strip_prefix("This is cvc5 version ")
+        .and_then(|version| version.split_ascii_whitespace().next().map(String::from));
+    version.ok_or(anyhow!("bad CVC5 version: {}", version_full))
 }
 
 // cross-platform wrappers
@@ -371,6 +374,17 @@ pub fn symlink_file<P: AsRef<Path>, Q: AsRef<Path>>(original: P, link: Q) -> std
     }
 }
 
+// Wrapper for Command::output(), error is wrapped in anyhow::Error
+fn run(cmd: &mut Command) -> anyhow::Result<std::process::Output> {
+    cmd.output().map_err(|e| {
+        if e.kind() == std::io::ErrorKind::NotFound {
+            anyhow!("{:?} not found", cmd.get_program())
+        } else {
+            anyhow!("{:?}: {}", cmd, e)
+        }
+    })
+}
+
 pub fn why3find_install() {
     Command::new("why3find").arg("install").arg("prelude").status().unwrap();
 }