Merge remote-tracking branch 'origin/master' into prusti

# Conflicts: # Cargo.lock # creusot-contracts/src/ghost.rs # creusot-contracts/src/ghost_ptr.rs # creusot-contracts/src/lib.rs # creusot-rustc/src/main.rs # creusot/tests/should_fail/bug/869.mlcfg # creusot/tests/should_fail/cycle.stderr # creusot/tests/should_succeed/100doors.mlcfg # creusot/tests/should_succeed/bug/874.mlcfg # creusot/tests/should_succeed/filter_positive.mlcfg # creusot/tests/should_succeed/hashmap.mlcfg # creusot/tests/should_succeed/hillel.mlcfg # creusot/tests/should_succeed/iterators/01_range.mlcfg # creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg # creusot/tests/should_succeed/iterators/04_skip.mlcfg # creusot/tests/should_succeed/iterators/07_fuse.mlcfg # creusot/tests/should_succeed/iterators/08_collect_extend.mlcfg # creusot/tests/should_succeed/iterators/09_empty.mlcfg # creusot/tests/should_succeed/iterators/10_once.mlcfg # creusot/tests/should_succeed/iterators/14_copied.mlcfg # creusot/tests/should_succeed/iterators/15_enumerate.mlcfg # creusot/tests/should_succeed/knapsack.mlcfg # creusot/tests/should_succeed/knapsack_full.mlcfg # creusot/tests/should_succeed/rusthorn/inc_max_repeat.mlcfg # creusot/tests/should_succeed/selection_sort_generic.mlcfg # creusot/tests/should_succeed/sparse_array.mlcfg # creusot/tests/should_succeed/sum.mlcfg # creusot/tests/should_succeed/sum_of_odds.mlcfg # creusot/tests/should_succeed/syntax/13_vec_macro.mlcfg # creusot/tests/should_succeed/vector/01.mlcfg # creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg # creusot/tests/should_succeed/vector/06_knights_tour.mlcfg # creusot/tests/should_succeed/vector/08_haystack.mlcfg
creusot-rs · Mar 14, 2024 · 471dc66 · 471dc66
2 parents aa44a8a + f5731f7
commit 471dc66
Show file tree

Hide file tree

Showing 593 changed files with 23,419 additions and 13,109 deletions.
diff --git a/.creusot-config.sample/Config.toml b/.creusot-config.sample/Config.toml
@@ -0,0 +1,6 @@
+version = 1
+
+[tools]
+mode = "external"
+why3_path = "why3"
+altergo_path = "alt-ergo"
diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
@@ -44,6 +44,8 @@ jobs:
         key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
     - name: Build
       run: cargo build
+    - name: dummy creusot setup
+      run: cp -r .creusot-config.sample .creusot-config
     - name: Run tests
       run: cargo test
   why3:
@@ -55,47 +57,34 @@ jobs:
     - name: Fetch target branch
       if: github.base_ref
       run: git fetch --no-tags --prune --depth=1 origin +refs/heads/${{github.base_ref}}:refs/remotes/origin/${{github.base_ref}}
-    - name: Install CVC4
-      run: sudo apt-get install -y cvc4=1.8-2
-    - name: Install CVC5
-      run: |
-        wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.5/cvc5-Linux
-        sudo cp cvc5-Linux /usr/local/bin/cvc5
-        sudo chmod +x /usr/local/bin/cvc5
-    - name: Install Z3
-      run: |
-        wget https://github.com/Z3Prover/z3/releases/download/z3-4.12.4/z3-4.12.4-x64-glibc-2.35.zip
-        unzip z3-4.12.4-x64-glibc-2.35.zip
-        sudo cp -rn z3-4.12.4-x64-glibc-2.35/bin /usr/local
-        sudo cp -rn z3-4.12.4-x64-glibc-2.35/include /usr/local
-        sudo chmod +x /usr/local/bin/z3
     - uses: actions/cache@v2
       with:
         path: |
           ~/.cargo/registry
           ~/.cargo/git
+          ~/.cache/creusot
           target
-        key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
+        key: ${{ runner.os }}-cargo-creusot-${{ hashFiles('**/Cargo.lock', 'creusot-setup/src/tools_versions_urls.rs') }}
     - uses: dawidd6/action-download-artifact@v2
       with:
         workflow: why3.yml
         name: why3
         path: /home/runner/work/creusot/why3
-    - run: |
+    - name: setup paths for why3 and alt-ergo
+      run: |
         chmod -R +x ~/work/creusot/why3/bin
         chmod -R +x ~/work/creusot/why3/lib/why3/why3server
+        echo ~/work/creusot/why3/bin >> $GITHUB_PATH
 
         mv ~/work/creusot/why3/alt-ergo /usr/local/bin/alt-ergo
         chmod +x /usr/local/bin/alt-ergo
         echo $(/usr/local/bin/alt-ergo --version)
-
-        ~/work/creusot/why3/bin/why3 config detect
-        cat ~/.why3.conf
+    - name: run cargo creusot setup install
+      run: |
+        cargo run --bin cargo-creusot creusot setup install
+        echo -e "\n>> ~/.config/creusot/Config.toml:\n"
+        cat ~/.config/creusot/Config.toml
+        echo -e "\n>> ~/.config/creusot/why3.conf:\n"
+        cat ~/.config/creusot/why3.conf
     - run: cargo test --test why3 "" -- --replay=none --diff-from=origin/master
-      env:
-        WHY3_CONFIG: ${{ github.workspace }}/ci/why.conf
-        WHY3_PATH: ${{ github.workspace }}/../why3/bin/why3
     - run: cargo test --test why3 "" -- --skip-unstable
-      env:
-        WHY3_CONFIG: ${{ github.workspace }}/ci/why.conf
-        WHY3_PATH: ${{ github.workspace }}/../why3/bin/why3
diff --git a/.gitignore b/.gitignore
@@ -2,6 +2,9 @@
 nll-facts/
 mir_dump/
 
+# Creusot local config for development
+/.creusot-config
+
 # Creusot files
 *.creusot
 *.cmeta

diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md
@@ -151,7 +151,7 @@ Instead, we replace the `discriminant` / `switchInt` pair with a match directly
 
 ## Logical functions
 
-Logical functions are created by `#[ghost]`, `#[logic]`, or `#[predicate]`.
+Logical functions are created by `#[logic]` or `#[predicate]`.
 
 ## Specifications