Merge branch 'main' into romac/driver-proposals

.github/dependabot.yml

@@ -0,0 +1,8 @@
+# https://docs.github.com/github/administering-a-repository/configuration-options-for-dependency-updates
+
+version: 2
+updates:
+  - package-ecosystem: "cargo"
+    directory: "/Code"
+    schedule:
+      interval: "weekly"

.github/workflows/coverage.yml

@@ -15,6 +15,7 @@ on:
 
 jobs:
   coverage:
+    name: Integration
     runs-on: ubuntu-latest
     defaults:
       run:
@@ -38,12 +39,49 @@ jobs:
       - name: Install cargo-llvm-cov
         uses: taiki-e/install-action@cargo-llvm-cov
       - name: Generate code coverage
-        run: cargo llvm-cov nextest --all-features --workspace --lcov --output-path lcov.info
+        run: cargo llvm-cov nextest --workspace --exclude malachite-itf --all-features --lcov --output-path lcov.info
       - name: Generate text report
         run: cargo llvm-cov report
       - name: Upload coverage to Codecov
         uses: codecov/codecov-action@v3
         with:
           token: ${{ secrets.CODECOV_TOKEN }}
           files: Code/lcov.info
+          flags: integration
+          fail_ci_if_error: true
+
+  mbt-coverage:
+    name: MBT
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: Code
+    env:
+      CARGO_TERM_COLOR: always
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+      - uses: actions/setup-node@v3
+        with:
+          node-version: "18"
+      - run: npm install -g @informalsystems/quint
+      - name: Setup Rust toolchain
+        uses: actions-rust-lang/setup-rust-toolchain@v1
+        with:
+          toolchain: nightly
+          components: llvm-tools-preview
+      - name: Install cargo-nextest
+        uses: taiki-e/install-action@cargo-nextest
+      - name: Install cargo-llvm-cov
+        uses: taiki-e/install-action@cargo-llvm-cov
+      - name: Generate code coverage
+        run: cargo llvm-cov nextest -p malachite-itf --all-features --lcov --output-path lcov.info
+      - name: Generate text report
+        run: cargo llvm-cov report
+      - name: Upload coverage to Codecov
+        uses: codecov/codecov-action@v3
+        with:
+          token: ${{ secrets.CODECOV_TOKEN }}
+          files: Code/lcov.info
+          flags: mbt
           fail_ci_if_error: true

.github/workflows/mbt.yml

@@ -42,4 +42,4 @@ jobs:
         run: echo "QUINT_SEED=$(date +%s)" >> $GITHUB_ENV
       - name: Run tests from traces (with random seed)
         working-directory: Code/itf
-        run: cargo nextest run --workspace --all-features test_itf
+        run: cargo nextest run -p malachite-itf --all-features

.github/workflows/quint.yml

@@ -26,10 +26,12 @@ jobs:
   quint-test:
     name: Test
     runs-on: ubuntu-latest
+    env:
+      MAX_SAMPLES: 100
     steps:
       - uses: actions/checkout@v4
       - uses: actions/setup-node@v3
         with:
           node-version: "18"
       - run: npm install -g @informalsystems/quint
-      - run: bash Scripts/quint-forall.sh test Specs/Quint/*Test.qnt
+      - run: bash Scripts/quint-forall.sh "test --max-samples $MAX_SAMPLES" Specs/Quint/*Test.qnt

Code/.cargo/config.toml

@@ -0,0 +1,3 @@
+[alias]
+mbt         = "nextest run -p malachite-itf --all-features"
+integration = "nextest run --workspace --exclude malachite-itf"