diff --git a/Cargo.lock b/Cargo.lock index 3e51db1938..dce82d7f31 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -421,8 +421,8 @@ dependencies = [ "assert_cmd", "clap", "creusot-contracts", - "creusot-dev-config", "creusot-metadata", + "creusot-setup", "escargot", "glob", "include_dir", @@ -478,15 +478,6 @@ dependencies = [ "uuid", ] -[[package]] -name = "creusot-dev-config" -version = "0.3.0" -dependencies = [ - "anyhow", - "creusot-setup", - "which", -] - [[package]] name = "creusot-metadata" version = "0.3.0" @@ -2425,7 +2416,7 @@ version = "0.3.0" dependencies = [ "assert_cmd", "clap", - "creusot-dev-config", + "creusot-setup", "git2", "glob", "roxmltree", diff --git a/cargo-creusot/src/main.rs b/cargo-creusot/src/main.rs index 9a9790e39d..0f024ebae3 100644 --- a/cargo-creusot/src/main.rs +++ b/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, diff --git a/cargo-creusot/src/why3find_wrapper.rs b/cargo-creusot/src/why3find_wrapper.rs index 2826f9fd61..ded24ba065 100644 --- a/cargo-creusot/src/why3find_wrapper.rs +++ b/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, paths: &CreusotFlags) -> Result<()> { - let mut why3find = Command::new(&paths.why3find_path); +fn raw_config(args: &Vec, paths: &Paths) -> Result<()> { + let mut why3find = Command::new(&paths.why3find); why3find .arg("config") .arg("--quiet") @@ -51,8 +51,8 @@ fn raw_config(args: &Vec, 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`.")); } diff --git a/creusot-dev-config/src/bin/dev-env.rs b/creusot-dev-config/src/bin/dev-env.rs index 5131b2a4c8..20adcecd94 100644 --- a/creusot-dev-config/src/bin/dev-env.rs +++ b/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()); diff --git a/creusot-dev-config/src/lib.rs b/creusot-dev-config/src/lib.rs deleted file mode 100644 index 896a8c70cf..0000000000 --- a/creusot-dev-config/src/lib.rs +++ /dev/null @@ -1,26 +0,0 @@ -use std::{path::PathBuf, process::Command}; - -/// Helper library encapsulating the logic for looking up creusot's config and -/// calling why3 in development workflows. This is used in particular by the -/// testsuite. - -pub struct Paths { - pub why3: PathBuf, - pub why3_config: PathBuf, -} - -/// Fails if the config could not be loaded -pub fn paths() -> anyhow::Result { - let paths = creusot_setup::status_for_creusot()?; - Ok(Paths { why3: paths.why3_path, why3_config: paths.why3_config }) -} - -/// Returns a command to invoke why3 (passing it the path to its configuration -/// file if needed). -/// Fails if the config could not be loaded -pub fn why3_command() -> anyhow::Result { - let p = paths()?; - let mut cmd = Command::new(p.why3.clone()); - cmd.arg("-C").arg(p.why3_config); - Ok(cmd) -} diff --git a/creusot-setup/src/lib.rs b/creusot-setup/src/lib.rs index 9aaa95d279..7e95b8adc7 100644 --- a/creusot-setup/src/lib.rs +++ b/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 { +/// Get paths to tools from Config.toml. +/// fail if the installation is not in an acceptable state +pub fn creusot_paths() -> anyhow::Result { 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 { 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, }) } diff --git a/creusot/Cargo.toml b/creusot/Cargo.toml index 4fa256f18d..3a8afcba33 100644 --- a/creusot/Cargo.toml +++ b/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" diff --git a/creusot/tests/ui.rs b/creusot/tests/ui.rs index 67019e08c9..434963f561 100644 --- a/creusot/tests/ui.rs +++ b/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 = diff --git a/why3tests/Cargo.toml b/why3tests/Cargo.toml index 88181e9243..aeb554dcd8 100644 --- a/why3tests/Cargo.toml +++ b/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 - diff --git a/why3tests/tests/why3.rs b/why3tests/tests/why3.rs index c61e5ebafe..5bb8d7f2ac 100644 --- a/why3tests/tests/why3.rs +++ b/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");