upgrade of the CI workflow

.github/workflows/ci.yml

@@ -10,58 +10,75 @@ permissions:
   contents: read
 
 jobs:
-
   lint:
     name: PyLint
-    runs-on: ubuntu-20.04
+    needs: test
+    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
+    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
+          python${{ matrix.py-version }} -m ensurepip
       - 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

.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

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
 

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>=1.1.1; sys.platform == "linux" or sys.platform == "darwin"

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

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

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