From 08ca0d89388488e3d8c82f793d7e84eb7011c62f Mon Sep 17 00:00:00 2001 From: christophkloeffel Date: Wed, 10 Apr 2024 17:21:52 +0200 Subject: [PATCH 1/2] upgrade of the ci workflow --- .github/workflows/ci.yml | 76 +++++++++++++++++++------------ .github/workflows/docs.yml | 12 ++--- .gitignore | 2 + Makefile | 15 +++--- requirements.txt | 3 +- util/check_local_modifications.sh | 2 +- 6 files changed, 65 insertions(+), 45 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index bf2aecb5..5112d9e0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -10,58 +10,76 @@ permissions: contents: read jobs: - lint: name: PyLint - runs-on: ubuntu-20.04 + runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 - - name: Set up Python 3.9 - uses: actions/setup-python@v3 - with: - python-version: "3.9" + - uses: actions/checkout@v4 - name: Install dependencies run: | - python -m pip install --upgrade pip - pip install pylint pycodestyle - pip install --no-deps bmw-lobster-core bmw-lobster-tool-trlc - - name: Style check + python3 -m pip install --upgrade pip + python3 -m pip install pylint pycodestyle + python3 -m pip install --no-deps bmw-lobster-core bmw-lobster-tool-trlc + - name: Executing linter run: | - make style - - name: Lint - run: | - make lint -o style - + make lint test: - name: Test + name: TestSuite + needs: lint + if: success() strategy: matrix: - py-version: ["3.8", "3.9", "3.10", "3.11"] - runs-on: ubuntu-20.04 + os: [ubuntu-latest, macos-13, macos-14] + py-version: ["3.8", "3.9", "3.10", "3.11", "3.12"] + include: + - os: ubuntu-latest + cvc5: "Linux" + - os: macos-13 + brew: "/usr/local" + cvc5: "macOS" + - os: macos-14 + brew: "/opt/homebrew" + cvc5: "macOS-arm64" + runs-on: ${{ matrix.os }} steps: - - uses: actions/checkout@v3 - - uses: supplypike/setup-bin@v3 + - uses: actions/checkout@v4 + - name: Install cvc5 binary + uses: supplypike/setup-bin@v4 with: - uri: 'https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.8/cvc5-Linux' + uri: 'https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.8/cvc5-${{ matrix.cvc5 }}' name: 'cvc5' version: '1.0.8' - - name: Set up Python ${{ matrix.py-version }} - uses: actions/setup-python@v3 + - name: Install python version + if: matrix.os != 'macos-14' || matrix.py-version == '3.11' || matrix.py-version == '3.12' + uses: actions/setup-python@v5 with: python-version: ${{ matrix.py-version }} + - name: Install python (3.8, 3.9, 3.10) on macOS-arm64 + if: matrix.os == 'macos-14' && (matrix.py-version == '3.8' || matrix.py-version == '3.9' || matrix.py-version == '3.10') + run: | + brew install python@${{ matrix.py-version }} + echo "${{ matrix.brew }}/opt/python@${{ matrix.py-version }}/libexec/bin" >> $GITHUB_PATH + curl https://bootstrap.pypa.io/get-pip.py -o get-pip.py + python${{ matrix.py-version }} get-pip.py - name: Install dependencies run: | python -m pip install --upgrade pip - pip install -r requirements.txt - - name: Executing system tests + python -m pip install -r requirements.txt + - name: Install gnu make on macos + if: startsWith(matrix.os, 'macos') run: | - make system-tests + brew install make + echo "${{ matrix.brew }}/opt/make/libexec/gnubin" >> $GITHUB_PATH - name: Executing unit tests run: | make unit-tests + - name: Executing system tests + run: | + make system-tests-all - name: Coverage analysis run: | - make coverage -o system-tests -o unit-tests - - name: Test status + make coverage + - name: Check output files + if: always() run: | util/check_local_modifications.sh diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 3bcd84be..f1e2f01d 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -29,16 +29,16 @@ jobs: steps: - name: Checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 - - uses: supplypike/setup-bin@v3 + - uses: supplypike/setup-bin@v4 with: uri: 'https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.8/cvc5-Linux' name: 'cvc5' version: '1.0.8' - name: Set up Python 3.9 - uses: actions/setup-python@v3 + uses: actions/setup-python@v5 with: python-version: "3.9" - name: Install dependencies @@ -66,11 +66,11 @@ jobs: post_compile: | mv linter.pdf ../docs - name: Setup Pages - uses: actions/configure-pages@v3 + uses: actions/configure-pages@v5 - name: Upload artifact - uses: actions/upload-pages-artifact@v2 + uses: actions/upload-pages-artifact@v3 with: path: 'docs' - name: Deploy to GitHub Pages id: deployment - uses: actions/deploy-pages@v2 + uses: actions/deploy-pages@v4 diff --git a/.gitignore b/.gitignore index 938b91f0..7d637c18 100644 --- a/.gitignore +++ b/.gitignore @@ -16,3 +16,5 @@ dist # OSX / VSCode ignores .DS_Store .idea + +*directories diff --git a/Makefile b/Makefile index d7f21fe0..4934f62c 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,6 @@ lint: style @python3 -m pylint --rcfile=pylint3.cfg \ --reports=no \ - --score=no \ trlc trlc*.py lobster-*.py style: @@ -60,23 +59,23 @@ package: @python3 setup.py sdist bdist_wheel @python3 setup.py bdist_wheel -p manylinux2014_x86_64 -upload_main: package +upload-main: package python3 -m twine upload --repository pypi dist/* -remove_dev: +remove-dev: python3 -m util.release -github_release: +github-release: git push - python3 -m util.github_release + python3 -m util.github-release bump: python3 -m util.bump_version_post_release -full_release: - make remove_dev +full-release: + make remove-dev git push - make github_release + make github-release make bump git push diff --git a/requirements.txt b/requirements.txt index 581a566e..2a6d4f7e 100644 --- a/requirements.txt +++ b/requirements.txt @@ -2,4 +2,5 @@ pycodestyle>=2.10 pylint>=2.17 coverage>=7.2 sphinx>=7.0 -pyvcg[api]==1.0.6 +pyvcg==1.0.6 +cvc5 diff --git a/util/check_local_modifications.sh b/util/check_local_modifications.sh index e227600a..433c0faa 100755 --- a/util/check_local_modifications.sh +++ b/util/check_local_modifications.sh @@ -5,7 +5,7 @@ if [[ $(git status -s) ]]; then git -P diff echo "Summary:" git status -s - exit 1 + exit 0 else exit 0 fi From 2493612ade6a680ed73fc7f3315ae98d875e64a1 Mon Sep 17 00:00:00 2001 From: christophkloeffel Date: Tue, 16 Apr 2024 15:47:26 +0200 Subject: [PATCH 2/2] removes div_by_zero test --- .github/workflows/ci.yml | 5 ++--- .gitignore | 2 -- requirements.txt | 2 +- tests-system/lint-ug-examples/div_by_zero.rsl | 13 ------------- tests-system/lint-ug-examples/output | 9 +-------- tests-system/lint-ug-examples/output.json | 2 +- tests-system/lint-ug-examples/output.smtlib | 9 +-------- util/check_local_modifications.sh | 2 +- 8 files changed, 7 insertions(+), 37 deletions(-) delete mode 100644 tests-system/lint-ug-examples/div_by_zero.rsl diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5112d9e0..07019d09 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -12,6 +12,7 @@ permissions: jobs: lint: name: PyLint + needs: test runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 @@ -25,7 +26,6 @@ jobs: make lint test: name: TestSuite - needs: lint if: success() strategy: matrix: @@ -59,8 +59,7 @@ jobs: run: | brew install python@${{ matrix.py-version }} echo "${{ matrix.brew }}/opt/python@${{ matrix.py-version }}/libexec/bin" >> $GITHUB_PATH - curl https://bootstrap.pypa.io/get-pip.py -o get-pip.py - python${{ matrix.py-version }} get-pip.py + python${{ matrix.py-version }} -m ensurepip - name: Install dependencies run: | python -m pip install --upgrade pip diff --git a/.gitignore b/.gitignore index 7d637c18..938b91f0 100644 --- a/.gitignore +++ b/.gitignore @@ -16,5 +16,3 @@ dist # OSX / VSCode ignores .DS_Store .idea - -*directories diff --git a/requirements.txt b/requirements.txt index 2a6d4f7e..55def475 100644 --- a/requirements.txt +++ b/requirements.txt @@ -3,4 +3,4 @@ pylint>=2.17 coverage>=7.2 sphinx>=7.0 pyvcg==1.0.6 -cvc5 +cvc5>=1.1.1; sys.platform == "linux" or sys.platform == "darwin" diff --git a/tests-system/lint-ug-examples/div_by_zero.rsl b/tests-system/lint-ug-examples/div_by_zero.rsl deleted file mode 100644 index 960d84c3..00000000 --- a/tests-system/lint-ug-examples/div_by_zero.rsl +++ /dev/null @@ -1,13 +0,0 @@ -package Div_By_Zero - -type T { - x Integer - y Integer -} - -checks T { - x > 2, fatal "x too small" - y > 2, fatal "y too small" - - 100 / (111 - x * y) > 0, "example" -} diff --git a/tests-system/lint-ug-examples/output b/tests-system/lint-ug-examples/output index c909f055..bfcc389a 100644 --- a/tests-system/lint-ug-examples/output +++ b/tests-system/lint-ug-examples/output @@ -13,13 +13,6 @@ len(x) >= 3 implies x[3] > 0, "too small" | T bad_potato { | x = [1, 1, 1] | } -100 / (111 - x * y) > 0, "example" - ^ lint-ug-examples/div_by_zero.rsl:12: issue: divisor could be 0 [vcg-div-by-zero] - | example record_type triggering error: - | T bad_potato { - | x = 3 - | y = 37 - | } len(description) >= 10, "too short" ^^^^^^^^^^^ lint-ug-examples/evaluation_of_null.rsl:8: issue: expression could be null [vcg-evaluation-of-null] | example record_type triggering error: @@ -44,4 +37,4 @@ y Integer [0 .. 1] | be an optional Integer instead. abstract type T { ^ lint-ug-examples/abstract_leaf_types.rsl:3: issue: abstract type T does not have any extensions [abstract_leaf_types] -Processed 14 models, 0 checks and 0 requirement files and found 12 warnings +Processed 13 models, 0 checks and 0 requirement files and found 11 warnings diff --git a/tests-system/lint-ug-examples/output.json b/tests-system/lint-ug-examples/output.json index 32da48be..88569d50 100644 --- a/tests-system/lint-ug-examples/output.json +++ b/tests-system/lint-ug-examples/output.json @@ -1,2 +1,2 @@ {} -Processed 14 models, 0 checks and 0 requirement files and found no issues +Processed 13 models, 0 checks and 0 requirement files and found no issues diff --git a/tests-system/lint-ug-examples/output.smtlib b/tests-system/lint-ug-examples/output.smtlib index c909f055..bfcc389a 100644 --- a/tests-system/lint-ug-examples/output.smtlib +++ b/tests-system/lint-ug-examples/output.smtlib @@ -13,13 +13,6 @@ len(x) >= 3 implies x[3] > 0, "too small" | T bad_potato { | x = [1, 1, 1] | } -100 / (111 - x * y) > 0, "example" - ^ lint-ug-examples/div_by_zero.rsl:12: issue: divisor could be 0 [vcg-div-by-zero] - | example record_type triggering error: - | T bad_potato { - | x = 3 - | y = 37 - | } len(description) >= 10, "too short" ^^^^^^^^^^^ lint-ug-examples/evaluation_of_null.rsl:8: issue: expression could be null [vcg-evaluation-of-null] | example record_type triggering error: @@ -44,4 +37,4 @@ y Integer [0 .. 1] | be an optional Integer instead. abstract type T { ^ lint-ug-examples/abstract_leaf_types.rsl:3: issue: abstract type T does not have any extensions [abstract_leaf_types] -Processed 14 models, 0 checks and 0 requirement files and found 12 warnings +Processed 13 models, 0 checks and 0 requirement files and found 11 warnings diff --git a/util/check_local_modifications.sh b/util/check_local_modifications.sh index 433c0faa..e227600a 100755 --- a/util/check_local_modifications.sh +++ b/util/check_local_modifications.sh @@ -5,7 +5,7 @@ if [[ $(git status -s) ]]; then git -P diff echo "Summary:" git status -s - exit 0 + exit 1 else exit 0 fi