Merge pull request #1019 from Armael/ncores

setup: allow configuring the number of cores used by why3

cargo-creusot/src/main.rs

@@ -90,14 +90,15 @@ fn main() -> Result<()> {
             Ok(())
         }
         Setup(SetupSubCommand::Status) => setup::status(),
-        Setup(SetupSubCommand::Install { external, no_check_version }) => {
+        Setup(SetupSubCommand::Install { provers_parallelism, external, no_check_version }) => {
             let extflag =
                 |name| setup::ExternalFlag { check_version: !no_check_version.contains(&name) };
             let managedflag = |name, mname| setup::ManagedFlag {
                 check_version: !no_check_version.contains(&name),
                 external: external.contains(&mname),
             };
             let flags = setup::InstallFlags {
+                provers_parallelism,
                 why3: extflag(SetupTool::Why3),
                 altergo: extflag(SetupTool::AltErgo),
                 z3: managedflag(SetupTool::Z3, SetupManagedTool::Z3),

ci/creusot-config-dummy.toml

@@ -1,4 +1,5 @@
-version = 2
+version = 3
+provers_parallelism = 1
 
 [why3]
 path = "why3"

creusot-args/src/options.rs

@@ -114,12 +114,22 @@ pub enum SetupTool {
     CVC5,
 }
 
+fn default_provers_parallelism() -> usize {
+    match std::thread::available_parallelism() {
+        Ok(n) => n.get(),
+        Err(_) => 1,
+    }
+}
+
 #[derive(Debug, Parser, Clone)]
 pub enum SetupSubCommand {
     /// Show the current status of the Creusot installation
     Status,
     /// Setup Creusot or update an existing installation
     Install {
+        /// Maximum number of provers to run in parallel
+        #[arg(long, default_value_t = default_provers_parallelism())]
+        provers_parallelism: usize,
         /// Look-up <TOOL> from PATH instead of using the built-in version
         #[arg(long, value_name = "TOOL")]
         external: Vec<SetupManagedTool>,

creusot-setup/src/config.rs

@@ -7,7 +7,8 @@ use std::{
 // identifies a version of the config file.
 // the goal is to avoid silently mis-interpreting a past or future version of
 // the config file whenever its format changes.
-pub const CURRENT_CONFIG_VERSION: i64 = 2;
+// NOTE: update ci/creusot-config-dummy.toml whenever you change this.
+pub const CURRENT_CONFIG_VERSION: i64 = 3;
 
 // bump CURRENT_CONFIG_VERSION if you change this definition
 #[derive(Serialize, Deserialize)]
@@ -29,6 +30,7 @@ pub enum ManagedTool {
 // bump CURRENT_CONFIG_VERSION if you change this definition
 #[derive(Serialize, Deserialize)]
 pub struct Config {
+    pub provers_parallelism: usize,
     pub why3: ExternalTool,
     pub altergo: ExternalTool,
     pub z3: ManagedTool,

creusot-setup/src/lib.rs

@@ -193,6 +193,7 @@ pub struct ManagedFlag {
 }
 
 pub struct InstallFlags {
+    pub provers_parallelism: usize,
     pub why3: ExternalFlag,
     pub altergo: ExternalFlag,
     pub z3: ManagedFlag,
@@ -234,6 +235,7 @@ pub fn install(flags: InstallFlags) -> anyhow::Result<()> {
     // build the corresponding configuration
 
     let config = Config {
+        provers_parallelism: std::cmp::max(1, flags.provers_parallelism),
         why3: external_tool(WHY3, flags.why3)?,
         altergo: external_tool(ALTERGO, flags.altergo)?,
         z3: managed_tool(Z3.bin, flags.z3)?,
@@ -290,7 +292,12 @@ fn apply_config(paths: &CfgPaths, cfg: &Config) -> anyhow::Result<()> {
     }
 
     // generate the corresponding .why3.conf
-    generate_why3_conf(&cfg.why3.path, &paths.bin_subdir, &paths.why3_config_file)?;
+    generate_why3_conf(
+        cfg.provers_parallelism,
+        &cfg.why3.path,
+        &paths.bin_subdir,
+        &paths.why3_config_file,
+    )?;
 
     // write the config file to disk
     cfg.write_to_file(&paths.config_file)

creusot-setup/src/tools.rs

@@ -187,15 +187,18 @@ fn detect_why3_version(why3: &Path) -> Option<String> {
 }
 
 pub fn generate_why3_conf(
+    provers_parallelism: usize,
     why3_path: &Path,
     bin_dir: &Path,
     dest_file: &Path,
 ) -> anyhow::Result<()> {
     println!("Generating a fresh why3 configuration...");
-    // create or empty the destination file to avoid getting a warning from why3
-    // because it doesn't exist
     {
-        let _ = fs::File::create(&dest_file);
+        use std::io::Write;
+        let mut f = fs::File::create(&dest_file)?;
+        writeln!(&mut f, "[main]")?;
+        writeln!(&mut f, "magic = {WHY3_CONFIG_MAGIC_NUMBER}")?;
+        writeln!(&mut f, "running_provers_max = {provers_parallelism}")?;
     }
     let status = Command::new(why3_path)
         .arg("-C")

creusot-setup/src/tools_versions_urls.rs

@@ -7,6 +7,7 @@
 
 // tools without binary releases
 pub const WHY3_VERSION: &'static str = "1.7.2";
+pub const WHY3_CONFIG_MAGIC_NUMBER: &'static str = "14";
 pub const ALTERGO_VERSION: &'static str = "2.5.3";
 // tools with binary releases
 pub const Z3_VERSION: &'static str = "4.12.4";