Merge branch 'master' into free-pcs-engine

.github/workflows/coverage.yml

@@ -14,12 +14,13 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
 
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: '15'
+          distribution: 'zulu'
 
       - name: Set up the environment
         run: python x.py setup

.github/workflows/crates-io.yml

@@ -20,7 +20,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
       - name: Publish crates.io
         uses: katyo/publish-crates@v2
         with:

.github/workflows/deploy.yml

@@ -14,22 +14,23 @@ jobs:
   build:
     strategy:
       matrix:
-        os: [ubuntu-20.04, ubuntu-22.04, windows-latest, macos-latest]
+        os: [ubuntu-20.04, windows-latest, macos-latest]
       fail-fast: false
     runs-on: ${{ matrix.os }}
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
 
       - name: Set up Python 3
-        uses: actions/setup-python@v2
+        uses: actions/setup-python@v4
         with:
           python-version: '3.x'
 
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: '15'
+          distribution: 'zulu'
 
       - name: Set up the environment
         run: python x.py setup
@@ -61,17 +62,18 @@ jobs:
     if: false
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
 
       - name: Set up Python 3
-        uses: actions/setup-python@v2
+        uses: actions/setup-python@v4
         with:
           python-version: '3.x'
 
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: '15'
+          distribution: 'zulu'
 
       - name: Set up the environment
         run: python x.py setup
@@ -108,7 +110,7 @@ jobs:
       - name: Zip Prusti artifacts
         shell: bash
         run: |
-          for os in ubuntu-20.04 ubuntu-22.04 windows-latest macos-latest
+          for os in ubuntu-20.04 windows-latest macos-latest
           do
             echo "Package Prusti artifact for $os"
             cd prusti-release-$os
@@ -128,9 +130,9 @@ jobs:
         with:
           tag_name: ${{ env.TAG_NAME }}
           release_name: Nightly Release ${{ env.TAG_NAME }}
-          keep_num: 2
+          keep_num: 4
 
-      - name: Upload release asset for Ubuntu 20.04 using a backward compatible asset name
+      - name: Upload release asset for Ubuntu
         uses: actions/upload-release-asset@v1
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
@@ -140,26 +142,6 @@ jobs:
           asset_name: prusti-release-ubuntu.zip
           asset_content_type: application/zip
 
-      - name: Upload release asset for Ubuntu 20.04
-        uses: actions/upload-release-asset@v1
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        with:
-          upload_url: ${{ steps.create_release.outputs.upload_url }}
-          asset_path: ./prusti-release-ubuntu-20.04/prusti.zip
-          asset_name: prusti-release-ubuntu-20.04.zip
-          asset_content_type: application/zip
-
-      - name: Upload release asset for Ubuntu 22.04
-        uses: actions/upload-release-asset@v1
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        with:
-          upload_url: ${{ steps.create_release.outputs.upload_url }}
-          asset_path: ./prusti-release-ubuntu-22.04/prusti.zip
-          asset_name: prusti-release-ubuntu-22.04.zip
-          asset_content_type: application/zip
-
       - name: Upload release asset for Windows
         uses: actions/upload-release-asset@v1
         env:

.github/workflows/pages.yml

@@ -0,0 +1,82 @@
+name: Build GitHub pages
+
+on:
+  workflow_dispatch:
+  push:
+    branches: 'master'
+  pull_request:
+    branches: 'master'
+
+env:
+  RUST_BACKTRACE: 1
+  # Currently broken. See issue #1287
+  # RUSTDOCFLAGS: "--generate-link-to-definition -Zunstable-options"
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v3
+        with:
+          path: "repo"
+
+      - name: Check for broken links
+        uses: lycheeverse/[email protected]
+        with:
+          fail: true
+
+      - name: Prepare output directory
+        run: |
+          mkdir -p output
+          cp -r repo/docs/static/* output/
+
+      - name: Setup mdBook
+        uses: peaceiris/actions-mdbook@v1
+        with:
+          mdbook-version: "latest"
+
+      - name: Build dummy crate to get dependencies
+        run: |
+          cd repo/docs/dummy/
+          cargo build --target-dir ./target
+
+      - name: Build user guide
+        run: |
+          cd repo/docs/user-guide
+          mdbook build -d ../../../output/user-guide
+
+      - name: Build dev guide
+        run: |
+          cd repo/docs/dev-guide
+          mdbook build -d ../../../output/dev-guide
+
+      - name: Doctest user guide
+        run: |
+          cd repo/docs/user-guide
+          mdbook test -L ../dummy/target/debug/deps
+
+      - name: Doctest dev guide
+        run: |
+          cd repo/docs/dev-guide
+          mdbook test -L ../dummy/target/debug/deps
+
+      - name: Set up the environment
+        run: |
+          cd repo
+          python x.py setup
+
+      - name: Generate documentation
+        run: |
+          cd repo
+          python x.py doc --all --no-deps
+          cp -r ./target/doc ../output/doc
+
+      # Only deploy on push to master
+      - name: Publish to GitHub pages
+        uses: peaceiris/actions-gh-pages@v3
+        if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/master' }}
+        with:
+          github_token: ${{ secrets.GITHUB_TOKEN }}
+          publish_dir: ./output
+          force_orphan: true