Install why3 and why3find in local switch

.github/workflows/deploy.yml

@@ -40,7 +40,7 @@ jobs:
         key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
     - name: Install Creusot
       run: |
-        ./INSTALL --skip-extra-tools
+        ./INSTALL --external why3-and-why3find --skip-extra-tools
     - name: Dummy creusot setup
       run: |
         mkdir -p ~/.config/creusot

.github/workflows/nightly.yml

@@ -27,13 +27,9 @@ jobs:
       with:
         ocaml-compiler: 5.3.0
         opam-local-packages: ci/creusot-deps-nightly.opam
-    - name: Build opam packages
-      run: |
-        sudo apt update
-        opam install creusot-deps-nightly
-        echo $(opam var bin) >> $GITHUB_PATH
+    - run: sudo apt update
     - name: Install Creusot
       if: steps.cache-creusot-setup.outputs.cache-hit != 'true'
       # Use only 2 parallel provers, because more provers (4) makes replaying proofs unstable
-      run: ./INSTALL --provers-parallelism 2 --no-check-version why3 --no-check-version why3find
+      run: ./INSTALL --provers-parallelism 2
     - run: cargo test --test why3

.github/workflows/rust.yml

@@ -134,7 +134,7 @@ jobs:
       if: steps.cache-creusot-setup.outputs.cache-hit != 'true'
       # Use only 2 parallel provers, because more provers (4) makes replaying proofs unstable
       run: |
-        ./INSTALL --skip-cargo-creusot --skip-creusot-rustc --provers-parallelism 2
+        ./INSTALL --external why3-and-why3find --skip-cargo-creusot --skip-creusot-rustc --provers-parallelism 2
         echo -e "\n>> ~/.config/creusot/Config.toml:\n"
         cat ~/.config/creusot/Config.toml
         echo -e "\n>> ~/.config/creusot/why3.conf:\n"
@@ -162,7 +162,7 @@ jobs:
       # Add /home/runner/work/creusot/creusot/_opam/bin to PATH just for this step
       run: |
         export PATH=/home/runner/work/creusot/creusot/_opam/bin:$PATH
-        ./INSTALL
+        ./INSTALL --external why3-and-why3find
     - name: test cargo creusot new
       run: |
         set -x

HACKING.md

@@ -22,7 +22,7 @@ To avoid first installing the `cargo-creusot` binary before running `cargo
 
 ## Running the testsuite
 
-- Test the output of creusot (coma files) against reference files:
+Test the output of creusot (coma files) against reference files:
 ```
 cargo test --test ui
 ```
@@ -32,16 +32,21 @@ Then, to update an out-of-date reference file:
 cargo test --test ui -- "optional-string" --bless
 ```
 
-(NB: to bless all the tests, you need to pass the empty string `""`)
-
-- Replay proofs:
+Replay proofs:
 ```
 cargo test --test why3
 ```
 
 Additional useful parameters, to avoid replaying *every* proof in development:
 - `--diff-from=GIT_REF`
-- `--replay=<none|obsolete|all>`
+
+Update `proof.json` of selected tests:
+```
+cargo test --test why3 -- "optional-string" --update
+```
+
+Note: the `why3` tests require Creusot to be installed so that the necessary tools can be found
+(Why3, Why3find, and provers).
 
 ## Inspecting/fixing the proof of a test
 

README.md

@@ -40,31 +40,26 @@ More examples are found in [creusot/tests/should_succeed](creusot/tests/should_s
 1. [Install `rustup`](https://www.rust-lang.org/tools/install), to get the suitable Rust toolchain
 2. [Get `opam`](https://opam.ocaml.org/doc/Install.html), the package manager for OCaml
 3. Clone the [creusot](https://github.com/creusot-rs/creusot/) repository,
-   then *move into the `creusot` directory* for the rest of the setup.
+   then move into the `creusot` directory.
     ```
     $ git clone https://github.com/creusot-rs/creusot
     $ cd creusot
     ```
-4. Set up **Why3** and **Why3find**. Create a local `opam` switch with why3:
-   ```
-   $ opam switch create -y . ocaml.5.3.0
-   $ eval $(opam env)
-   ```
-   This will build `why3`, `why3find`, and their ocaml dependencies in a local `_opam` directory.
-5. Install **Creusot**:
+4. Install **Creusot**:
    ```
    $ ./INSTALL
    ```
-   The installation consists of:
+   A regular installation consists of:
    - the `cargo-creusot` executable in `~/.cargo/bin/`;
    - the `creusot-rustc` executable in `~/.local/share/creusot/toolchains/$TOOLCHAIN/bin`;
+   - the `why3` and `why3find` executables in `~/.local/share/creusot/_opam/bin` (in a local opam switch);
+   - the Creusot prelude in `~/.local/share/creusot/_opam/lib/why3find/packages/creusot`;
    - SMT solvers (Alt-Ergo, CVC4, CVC5, Z3) in `~/.local/share/creusot/bin`;
    - configuration files in `~/.config/creusot/`.
 
-## Configuring the installation
-
-You can create a text file `INSTALL.opts` to remember command-line options to be passed
-to the installation script. Type `./INSTALL --help` for a list of possible options.
+Installation options can be set in a text file `INSTALL.opts`.
+They are just space-separated command-line arguments.
+Type `./INSTALL --help` for a list of available options.
 For example:
 
 ```

creusot-install/src/main.rs

@@ -5,14 +5,17 @@ use creusot_setup::{
     self as setup,
     config::{Config, ExternalTool, ManagedTool},
     tools_versions_urls::*,
-    Binary,
+    Binary, CfgPaths,
 };
 use indoc::writedoc;
 use reqwest::blocking::Client;
 use std::{
-    env, fs,
+    env,
+    ffi::OsStr,
+    fs,
     fs::{copy, create_dir_all, read_to_string, File},
     io::{self, BufWriter, Write},
+    os::unix::ffi::OsStrExt as _,
     path::{Path, PathBuf},
     process::Command,
 };
@@ -80,6 +83,7 @@ fn default_provers_parallelism() -> usize {
 
 #[derive(Debug, ValueEnum, Clone, PartialEq)]
 enum SetupManagedTool {
+    Why3AndWhy3find, // skips opam setup
     AltErgo,
     Z3,
     CVC4,
@@ -107,6 +111,9 @@ fn main() -> anyhow::Result<()> {
 
 fn install(args: Args) -> anyhow::Result<()> {
     let paths = setup::get_config_paths()?;
+    if !args.external.contains(&SetupManagedTool::Why3AndWhy3find) {
+        install_why3(&paths)?;
+    }
     if !args.skip_cargo_creusot {
         install_cargo_creusot()?;
     }
@@ -119,6 +126,28 @@ fn install(args: Args) -> anyhow::Result<()> {
     Ok(())
 }
 
+fn install_why3(cfg: &CfgPaths) -> anyhow::Result<()> {
+    println! {"Installing Why3 and Why3find..."};
+    if fs::exists(cfg.data_dir.join("_opam"))? {
+        // Upgrade existing switch
+        fs::copy(PathBuf::from("creusot-deps.opam"), &cfg.data_dir.join("creusot-deps.opam"))?;
+        let mut cmd = Command::new("opam");
+        cmd.args(["install", "creusot-deps", "-y", "--switch", &cfg.data_dir.to_string_lossy()]); // use creusot-deps.opam
+        if !cmd.status()?.success() {
+            bail!("Failed to upgrade why3 and why3find")
+        }
+    } else {
+        fs::create_dir_all(&cfg.data_dir)?;
+        fs::copy(PathBuf::from("creusot-deps.opam"), &cfg.data_dir.join("creusot-deps.opam"))?;
+        let mut cmd = Command::new("opam");
+        cmd.args(["switch", "create", "-y", &cfg.data_dir.to_string_lossy()]);
+        if !cmd.status()?.success() {
+            bail!("Failed to create opam switch")
+        }
+    }
+    Ok(())
+}
+
 fn install_cargo_creusot() -> anyhow::Result<()> {
     println! {"Installing cargo-creusot..."};
     let mut cmd = Command::new("cargo");
@@ -151,7 +180,7 @@ fn install_tools(paths: &setup::CfgPaths, args: Args) -> anyhow::Result<()> {
 
     // helpers to generate the ExternalTool/ManagedTool config sections
 
-    let getpath = |bin: Binary| -> anyhow::Result<PathBuf> {
+    let get_path = |bin: Binary| -> anyhow::Result<PathBuf> {
         let path = bin.detect_path().ok_or(anyhow!(
             "{} not found. Please install {} version {}",
             &bin.display_name,
@@ -161,31 +190,40 @@ fn install_tools(paths: &setup::CfgPaths, args: Args) -> anyhow::Result<()> {
         println!("Found {} at path: {}", &bin.display_name, &path.display());
         Ok(path)
     };
-
-    let external_tool = |bin: Binary, name: SetupTool| -> anyhow::Result<ExternalTool> {
-        Ok(ExternalTool {
-            path: getpath(bin)?,
-            check_version: !args.no_check_version.contains(&name),
-        })
+    let get_opam_path = |tool| -> anyhow::Result<PathBuf> {
+        let data_dir = &paths.data_dir.to_string_lossy();
+        let output = Command::new("opam")
+            .args(["exec", "--switch", data_dir, "--", "which", tool])
+            .output()?;
+        Ok(PathBuf::from(OsStr::from_bytes(output.stdout.trim_ascii_end())))
+    };
+    let external_tool = |path: PathBuf, name: SetupTool| -> anyhow::Result<ExternalTool> {
+        Ok(ExternalTool { path, check_version: !args.no_check_version.contains(&name) })
     };
     let managed_tool =
         |bin: Binary, name: SetupTool, mname: SetupManagedTool| -> anyhow::Result<ManagedTool> {
             if args.external.contains(&mname) {
                 Ok(ManagedTool::External(ExternalTool {
-                    path: getpath(bin)?,
+                    path: get_path(bin)?,
                     check_version: !args.no_check_version.contains(&name),
                 }))
             } else {
                 Ok(ManagedTool::Builtin { check_version: !args.no_check_version.contains(&name) })
             }
         };
 
+    let (why3_path, why3find_path) = if args.external.contains(&SetupManagedTool::Why3AndWhy3find) {
+        (get_path(setup::WHY3)?, get_path(setup::WHY3FIND)?)
+    } else {
+        (get_opam_path("why3")?, get_opam_path("why3find")?)
+    };
+
     // build the corresponding configuration
 
     let config = Config {
         provers_parallelism: std::cmp::max(1, args.provers_parallelism),
-        why3: external_tool(setup::WHY3, SetupTool::Why3)?,
-        why3find: external_tool(setup::WHY3FIND, SetupTool::Why3find)?,
+        why3: external_tool(why3_path, SetupTool::Why3)?,
+        why3find: external_tool(why3find_path, SetupTool::Why3find)?,
         altergo: managed_tool(ALTERGO.bin, SetupTool::AltErgo, SetupManagedTool::AltErgo)?,
         z3: managed_tool(Z3.bin, SetupTool::Z3, SetupManagedTool::Z3)?,
         cvc4: managed_tool(CVC4.bin, SetupTool::CVC4, SetupManagedTool::CVC4)?,

why3tests/tests/why3.rs

@@ -55,6 +55,10 @@ fn main() {
 
     std::env::set_current_dir("..").unwrap();
 
+    /// Use the Creusot installation for Why3, Why3find, and solvers (because they're a pain to keep track of if we allow them to come from anywhere)
+    let creusot_setup::Paths { why3, why3find, why3_config } =
+        creusot_setup::creusot_paths().unwrap();
+    /// Use the local prelude, so that it's easy to test quick changes.
     let build_prelude_success = Command::new("cargo")
         .args(["run", "-p", "creusot-install", "--", "--only-build-prelude"])
         .status()
@@ -116,9 +120,8 @@ fn main() {
         sessiondir.set_file_name(file.file_stem().unwrap());
 
         let output;
-        let paths = creusot_setup::creusot_paths().unwrap();
-        let mut why3 = Command::new(paths.why3.clone());
-        why3.arg("-C").arg(&paths.why3_config);
+        let mut why3 = Command::new(&why3);
+        why3.arg("-C").arg(&why3_config);
         why3.arg("--warn-off=unused_variable");
         why3.arg("--warn-off=clone_not_abstract");
         why3.arg("--warn-off=axiom_abstract");
@@ -222,8 +225,8 @@ fn main() {
                 }
             }
         } else {
-            let mut why3find = Command::new(paths.why3find);
-            why3find.env("WHY3CONFIG", &paths.why3_config);
+            let mut why3find = Command::new(&why3find);
+            why3find.env("WHY3CONFIG", &why3_config);
             why3find.arg("prove").arg(file.canonicalize().unwrap());
             why3find.arg("--root");
             why3find.arg("target");