diff --git a/creusot-setup/src/lib.rs b/creusot-setup/src/lib.rs index a9fc43d4a..423d67f9a 100644 --- a/creusot-setup/src/lib.rs +++ b/creusot-setup/src/lib.rs @@ -52,7 +52,7 @@ pub fn get_why3_config_file() -> anyhow::Result { struct Issue { error: bool, tool: String, - cur_version: Option, + cur_version: anyhow::Result, expected_version: String, builtin_tool: bool, } @@ -60,12 +60,12 @@ struct Issue { 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, - }) + }), } } diff --git a/creusot-setup/src/tools.rs b/creusot-setup/src/tools.rs index 2aca745b5..7c8953789 100644 --- a/creusot-setup/src/tools.rs +++ b/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, + detect_version: fn(&Path) -> anyhow::Result, } // download a list [ManagedBinary]s @@ -168,37 +168,31 @@ fn download_from_url_with_cache( // helpers: external binaries -pub enum DetectedVersion { - Good, - Bad(Option), -} - impl Binary { pub fn detect_path(&self) -> Option { 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 { + (self.detect_version)(path) } } // helpers: why3 -fn detect_why3_version(why3: &Path) -> Option { - 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 { + 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 { - 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 { + 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 { - 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 { + 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 { - 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 { + 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 { - 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 { + 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 { - 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 { + 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, Q: AsRef>(original: P, link: Q) -> std } } +// Wrapper for Command::output(), error is wrapped in anyhow::Error +fn run(cmd: &mut Command) -> anyhow::Result { + 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(); }