Merge branch 'dev' into rasi_generator

.github/pull_request_template.md

@@ -1,7 +1,7 @@
-Before merging this PR, please check the following:
+Checklist: <!-- Please first submit your pull request, you can check the checkboxes later. Feel free to ask for help if you don't know how/where to make changes. -->
 
-- [ ] I made sure the wiki is updated in accordance with the changes in this PR. For example, syntax changes, semantics changes, VerCors flags changes, etc.
+- [ ] The wiki is updated in accordance with the changes in this PR. For example: syntax changes, semantics changes, VerCors flags changes, etc.
 
 # PR description
 
-_Describe the motivation of the PR and the changes it introduces. Why is it needed, and what does it change?_
+<!-- Describe the motivation of the PR and the changes it introduces. Why is it needed, and what does it change? -->

.github/workflows/release.yml

@@ -0,0 +1,51 @@
+name: '(Pre)-Release'
+on:
+  push:
+    branches:
+      - 'master'
+      - 'dev'
+    tags:
+      - 'v[0-9]*'
+
+jobs:
+  Release:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout VerCors
+        uses: actions/checkout@v2
+      - name: Set Pre-release Tag
+        if: github.ref_name == 'dev'
+        run: |
+          git tag -f dev-prerelease
+          git push origin --tags --force
+      - name: Install Java
+        uses: actions/setup-java@v1
+        with:
+          java-version: 17
+      - name: Build Release
+        run: ./mill -j 0 vercors.main.release
+      - name: Set Properties
+        id: props
+        run: ./mill vercors.main.githubReleaseOutputs >> "$GITHUB_OUTPUT"
+      - name: Delete Previous Pre-release
+        uses: liudonghua123/delete-release-action@v1
+        if: github.ref_name == 'dev'
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        with:
+          suppress_errors: true
+          release_name: 'VerCors Nightly'
+      - name: Create Release
+        id: release
+        uses: softprops/action-gh-release@v1
+        with:
+          name: ${{ steps.props.outputs.RELEASE_NAME }}
+          tag_name: ${{ steps.props.outputs.TAG_NAME }}
+          body: ${{ steps.props.outputs.BODY }}
+          draft: false
+          prerelease: ${{ steps.props.output.PRERELEASE }}
+          files: |
+            out/vercors/main/unixTar.dest/*.tar.xz
+            out/vercors/main/macosTar.dest/*.tar.xz
+            out/vercors/main/winZip.dest/*.zip
+            out/vercors/main/deb.dest/*.deb

.github/workflows/scalatest.yml

@@ -5,13 +5,17 @@ on:
       - '**'
     tags-ignore:
       - dev-prerelease
+  pull_request:
+    branches:
+      - '**'
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
   Compile:
+    if: (github.event_name != 'pull_request' || github.event.pull_request.head.repo.fork)
     runs-on: ubuntu-latest
     steps:
       - name: Checkout VerCors

README.md

@@ -74,7 +74,7 @@ When building VerCors, you additionally need these dependencies:
 - Git (on Windows you need Git Bash, see <https://git-scm.com/downloads>)
 
 1. Clone the VerCors repository using `git clone https://github.com/utwente-fmt/vercors.git` and move into the cloned directory, `cd vercors`.
-2. Run `./mill vercors.compile` to compile VerCors.
+2. Run `./mill vercors.main.compile` to compile VerCors.
 3. Test whether the build was successful by running `./bin/vct examples/concepts/basic/induction-lemma.pvl`.
 
 # Running VerCors

bin/bashComplete

@@ -1,4 +1,5 @@
-#!/bin/sh
+#!/bin/bash
+set -e
 ROOT=$(dirname $(dirname $(readlink -f $0)))
-(cd $ROOT; ./mill vercors.main.runScript)
-$ROOT/out/vercors/main/runScript.dest/bashOptions "$@"
+(cd $ROOT; ./mill -j 0 vercors.main.runScript)
+$ROOT/out/vercors/main/runScript.dest/bashOptions "$@"

bin/carbon

@@ -1,6 +1,7 @@
-#!/bin/sh
+#!/bin/bash
+set -e
 ROOT=$(dirname $(dirname $(readlink -f $0)))
-(cd $ROOT; ./mill vercors.main.runScript)
+(cd $ROOT; ./mill -j 0 vercors.main.runScript)
 
 
 if [[ "$OSTYPE" == "darwin" ]]; then
@@ -11,4 +12,4 @@ else
   BOOGIE_EXE="$ROOT/res/universal/deps/unix/boogie/Boogie"
 fi
 
-BOOGIE_EXE=$BOOGIE_EXE $ROOT/out/vercors/main/runScript.dest/carbon --z3Exe $Z3 "$@"
+BOOGIE_EXE=$BOOGIE_EXE $ROOT/out/vercors/main/runScript.dest/carbon --z3Exe $Z3 "$@"

bin/silicon

@@ -1,6 +1,7 @@
-#!/bin/sh
+#!/bin/bash
+set -e
 ROOT=$(dirname $(dirname $(readlink -f $0)))
-(cd $ROOT; ./mill vercors.main.runScript)
+(cd $ROOT; ./mill -j 0 vercors.main.runScript)
 
 if [[ "$OSTYPE" == "darwin" ]]; then
   Z3="$ROOT/res/universal/deps/darwin/z3/bin/z3"

bin/vct

@@ -1,4 +1,5 @@
-#!/bin/sh
+#!/bin/bash
+set -e
 ROOT=$(dirname $(dirname $(readlink -f $0)))
-(cd $ROOT; ./mill vercors.main.runScript)
-$ROOT/out/vercors/main/runScript.dest/vercors "$@"
+(cd $ROOT; ./mill -j 0 vercors.main.runScript)
+$ROOT/out/vercors/main/runScript.dest/vercors "$@"