Skip to content

add Jans patches to VerCors v1 #1928

add Jans patches to VerCors v1

add Jans patches to VerCors v1 #1928

Workflow file for this run

name: Build and test
# Only run the workflow when pushed to master, dev, or on pull requests.
on:
push:
branches:
- '**'
tags-ignore:
- dev-prerelease
pull_request:
branches:
- '**'
jobs:
pre_build_test:
runs-on: ubuntu-latest
# Map a step output to a job output
outputs:
should_skip: ${{ steps.skip_check.outputs.should_skip }}
steps:
- id: skip_check
uses: fkirc/skip-duplicate-actions@master
with:
# Never allow two runs of this workflow to exist
concurrent_skipping: 'always'
# Except, never skip a PR, scheduled, or manually dispatch run
do_not_skip: '["pull_request", "workflow_dispatch", "schedule"]'
# Skip if we can find a duplicate run with the same everything
skip_after_successful_duplicate: 'true'
# Do not run on changes only to these files
paths_ignore: '["**/README.md", "**/LICENSE*"]'
build-test:
needs: pre_build_test
if: ${{ needs.pre_build_test.outputs.should_skip != 'true' }}
runs-on: ubuntu-latest
environment: Default
steps:
# This should automatically cancel any previous workflows that are still
# running when for example new commits are pushed.
#- uses: technote-space/auto-cancel-redundant-workflow@v1
- uses: actions/checkout@v2
- uses: actions/setup-java@v1
with:
java-version: "11"
# Currently sbt and fakeroot are installed by default
- name: Coursier cache
uses: coursier/cache-action@v5
- name: Build and package
run: sbt debian:packageBin universal:packageBin
- name: Run tests
run: sbt test || true
- name: Clean up intermediate files for caching
# From the sbt manual, clean up any leftover intermediate files
# https://www.scala-sbt.org/1.x/docs/GitHub-Actions-with-sbt.html
run: |
rm -rf "$HOME/.ivy2/local" || true
find $HOME/Library/Caches/Coursier/v1 -name "ivydata-*.properties" -delete || true
find $HOME/.ivy2/cache -name "ivydata-*.properties" -delete || true
find $HOME/.cache/coursier/v1 -name "ivydata-*.properties" -delete || true
find $HOME/.sbt -name "*.lock" -delete || true
- name: Archive VerCors .deb
uses: actions/upload-artifact@v2
with:
name: vercors-debian-package
retention-days: 1
path: |
target/*.deb
- run: mv target/universal/*.zip target/vercors.zip
- name: Archive VerCors .zip
uses: actions/upload-artifact@v2
with:
name: vercors-zip-package
retention-days: 1
path: |
target/vercors.zip
- name: "Zip VerCors class files"
# We skip the parsers subproject because sonar doesn't scan it, it's only generated code anyway
# And we zip them because this speeds up upload massively because only 1 file has to be uploaded instead of 1000
run: "find . -path ./parsers -prune -false -o -name '*.class' | zip -@ classfiles.zip"
- name: Archive VerCors class files
uses: actions/upload-artifact@v2
with:
name: vercors-class-files
retention-days: 1
path: |
classfiles.zip
# If this is the dev branch we also want to build the .txz binary for the release
- name: Build mac binary
if: ${{ github.ref == 'refs/heads/dev' }}
run: sbt universal:packageZipTarball
# If this is the dev branch we update the pre-release tag in the github repo
# We also package the release zip
- name: Set pre-release tag in github repo
if: ${{ github.ref == 'refs/heads/dev' }}
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
run: |
git config --local user.name "Vercors Team"
git config --local user.email "[email protected]"
git tag --force dev-prerelease
git remote set-url origin https://${GITHUB_TOKEN}@github.com/utwente-fmt/vercors.git
git push --force --tags
- name: Create Release
if: ${{ github.ref == 'refs/heads/dev' }}
uses: ncipollo/release-action@v1
with:
allowUpdates: true
artifacts: "target/*.deb,target/universal/*.tgz"
artifactContentType: application/zip
body: This is an alpha build of the vercors development branch. It is updated automatically after each merge. Refer to the commit on the left for the last update.
name: Vercors Dev Build
prerelease: true
tag: dev-prerelease
token: ${{ secrets.GITHUB_TOKEN }}
- name: Publish Test Report
uses: mikepenz/action-junit-report@v2
with:
report_paths: '**/target/test-reports/TEST-*.xml'
integration-test-linux:
needs: build-test
runs-on: ubuntu-latest
strategy:
matrix:
testID: [0, 1, 2, 3, 4]
fail-fast: false
env:
maxTestID: 5
steps:
# Need to check out the repo for the "examples" directory
- uses: actions/checkout@v2
- uses: actions/setup-java@v1
with:
java-version: "11"
java-package: jre
- name: Download VerCors binary
uses: actions/download-artifact@v2
with:
name: vercors-debian-package
- run: "sudo dpkg -i *.deb"
- run: vercors --silicon examples/manual/fibonacci.pvl
- run: SPLIT=${{ matrix.testID }}/${{ env.maxTestID }} vercors --test=examples --test-workers=2 --tool carbon --tool silicon --tool veymont --exclude-suite=slow,medium,problem-fail --progress --actions-test-output --enable-test-coverage --coverage-output-file=jacoco_${{ matrix.testID }}_${{ env.maxTestID }}.xml
- name: Archive Java Code Coverage (jacoco_n_m.xml)
uses: actions/upload-artifact@v2
with:
name: vercors-jacoco-xml
retention-days: 1
path: |
jacoco*.xml
integration-test-windows:
runs-on: windows-latest
needs: build-test
steps:
- uses: actions/checkout@v2
- uses: actions/setup-java@v1
with:
java-version: "11"
- name: Cache LLVM and Clang
id: cache-llvm
uses: actions/cache@v2
with:
path: ${{ runner.temp }}/llvm
key: llvm-10.0
- name: Install LLVM and Clang
uses: KyleMayes/install-llvm-action@v1
with:
version: "10.0"
directory: ${{ runner.temp }}/llvm
cached: ${{ steps.cache-llvm.outputs.cache-hit }}
- name: Download VerCors binary
uses: actions/download-artifact@v2
with:
name: vercors-zip-package
- run: mkdir vercorszip
# --strip-components is needed because the zip contains a directory, which contains bin, examples, etc.
# But the name of this directory changes from time to time, because of the version number
# By stripping the first component of the path when extracting this directory this is not a problem
# --directory extracts to a given directory, ensuring the current directory is not cluttered.
- run: tar --strip-components=1 --directory vercorszip -xf vercors.zip
# Note how arguments with commas are quoted triply:
# - One layer gets peeled of by the .bat script
# - Another layer gets peeled of by powershell
# This prevents the commas from being interpreted as array separators, a marvelous powershell feature.
- run: vercorszip\bin\vercors.bat --test=examples\basic --test-workers=2 --tool carbon --tool silicon """--exclude-suite=slow,medium,problem-fail""" --progress --actions-test-output
integration-test-mac:
runs-on: macos-latest
needs: build-test
steps:
- uses: actions/checkout@v2
- uses: actions/setup-java@v1
with:
java-version: "11"
- name: Install clang
run: brew install llvm
- name: Download VerCors binary
uses: actions/download-artifact@v2
with:
name: vercors-zip-package
- run: mkdir vercorszip
# --strip-components is needed because the zip contains a directory, which contains bin, examples, etc.
# But the name of this directory changes from time to time, because of the version number
# By stripping the first component of the path when extracting this directory this is not a problem
# --directory extracts to a given directory, ensuring the current directory is not cluttered.
- run: tar --strip-components=1 --directory vercorszip -xf vercors.zip
- run: vercorszip/bin/vercors --test=examples/basic --test-workers=2 --tool carbon --tool silicon --exclude-suite=slow,medium,problem-fail --progress --actions-test-output
integration-test-veymont:
needs: build-test
runs-on: ubuntu-latest
steps:
# Need to check out the repo for the "examples" directory and the veymont 2stage testing script
- uses: actions/checkout@v2
- uses: actions/setup-java@v1
with:
java-version: "11"
java-package: jre
- name: Download VerCors binary
uses: actions/download-artifact@v2
with:
name: vercors-debian-package
- run: "sudo dpkg -i *.deb"
- run: ./util/veymontTesting/veymont-2stage-tests.sh
integration-test-wiki:
needs: build-test
runs-on: ubuntu-latest
steps:
# Need to check out the repo for the "examples" directory
- uses: actions/checkout@v2
- uses: actions/setup-java@v1
with:
java-version: "11"
java-package: jre
- name: Install wiki script dependencies
working-directory: util/wiki
run: |
sudo apt install pandoc
pip3 install -r requirements.txt
- name: Extract test cases from wiki
run: "python3 util/wiki/generate_wiki_pdf.py -c wiki_cases"
- name: Download VerCors binary
uses: actions/download-artifact@v2
with:
name: vercors-debian-package
- run: "sudo dpkg -i *.deb"
- run: vercors --silicon examples/manual/fibonacci.pvl
# Be sure to propagate any changes to this line below to the appropriate invocation in wiki-snippet-test.yml
- run: vercors --test=wiki_cases --test-workers=2 --tool carbon --tool silicon --tool veymont --exclude-suite=slow,medium,problem-fail --progress --actions-test-output
sonar:
needs:
- build-test
- integration-test-linux
runs-on: ubuntu-latest
environment: Default
steps:
- uses: actions/checkout@v2
with:
#fetch-depth is needed to checkout the git history otherwise only the last commit is downloaded. The git history is used by analyses of sonar.
fetch-depth: 0
# The target branches are used in a pull request analysis which is why dev and ast are downloaded.
# The command "git checkout -" checkout the previous branch.
- run: git checkout dev
- run: git checkout -
- run: git checkout ast
- run: git checkout -
- uses: actions/setup-java@v1
with:
java-version: "11"
- name: Download VerCors class files
uses: actions/download-artifact@v2
with:
name: vercors-class-files
- name: Unzip VerCors class files
run: "unzip classfiles.zip"
- name: Download Java Code Coverage
uses: actions/download-artifact@v2
with:
name: vercors-jacoco-xml
- name: SonarCloud Scan
uses: sonarsource/sonarcloud-github-action@master
env:
# This is set automatically by github
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
# SONAR_TOKEN is set in the secrets section of the github repo
SONAR_TOKEN: ${{ secrets.SONAR_TOKEN }}
# Avoid "java not found" error (see: https://community.sonarsource.com/t/cannot-run-sonarsource-sonarcloud-github-action-master-java-not-found/14922/3)
JAVA_HOME: ''