Merge branch 'main' into alethe-fix-alpha-equiv

.github/actions/add-jar/action.yml

@@ -0,0 +1,97 @@
+name: Add self-contained JAR with the cvc5 Java bindings
+description: |
+  Creates a JAR that includes the cvc5 Java bindings
+  along with the necessary native libraries.
+inputs:
+  install-path:
+    description: path to the directory with installed artifacts
+  jar-libs-dir:
+    description: name of the directory that will contain the libraries within the JAR
+  jar-name:
+    description: target name of the JAR
+  github-token-latest:
+    description: token to upload JAR to latest
+  github-token-release:
+    description: token to upload JAR to release
+  shell:
+    default: bash
+runs:
+  using: composite
+  steps:
+    - name: Create JAR contents (Linux)
+      if: runner.os == 'Linux'
+      shell: ${{ inputs.shell }}
+      run: |
+        echo "::group::Create JAR contents (Linux)"
+        mkdir ${{ inputs.jar-libs-dir }}
+        cd ${{ inputs.jar-libs-dir }}
+        cat > filenames.txt <<EOF
+        libgmp.so.10
+        libpoly.so.0
+        libpolyxx.so.0
+        libcvc5.so.1
+        libcvc5parser.so.1
+        libcvc5jni.so
+        EOF
+        cat filenames.txt | xargs -I {} cp ${{ inputs.install-path }}/lib/{} .
+        echo "::endgroup::"
+
+    - name: Create JAR contents (macOS)
+      if: runner.os == 'macOS'
+      shell: ${{ inputs.shell }}
+      run: |
+        echo "::group::Create JAR contents (macOS)"
+        mkdir ${{ inputs.jar-libs-dir }}
+        cd ${{ inputs.jar-libs-dir }}
+        cat > filenames.txt <<EOF
+        libgmp.10.dylib
+        libpoly.0.dylib
+        libpolyxx.0.dylib
+        libcvc5.1.dylib
+        libcvc5parser.1.dylib
+        libcvc5jni.dylib
+        EOF
+        cat filenames.txt | xargs -I {} cp ${{ inputs.install-path }}/lib/{} .
+        echo "::endgroup::"
+
+    - name: Create JAR contents (Windows)
+      if: runner.os == 'Windows'
+      shell: ${{ inputs.shell }}
+      run: |
+        echo "::group::Create JAR contents (Windows)"
+        mkdir ${{ inputs.jar-libs-dir }}
+        cd ${{ inputs.jar-libs-dir }}
+        cat > filenames.txt <<EOF
+        libwinpthread-1.dll
+        libgcc_s_seh-1.dll
+        libstdc++-6.dll
+        libpoly.dll
+        libpolyxx.dll
+        libcvc5.dll
+        libcvc5parser.dll
+        cvc5jni.dll
+        EOF
+        cat filenames.txt | xargs -I {} cp ${{ inputs.install-path }}/bin/{} .
+        echo "::endgroup::"
+
+    - name: Create JAR
+      shell: ${{ inputs.shell }}
+      run: |
+        echo "::group::Create JAR"
+        unzip ${{ inputs.install-path }}/share/java/cvc5.jar
+        jar cf ${{ inputs.jar-name }}.jar AUTHORS COPYING licenses io ${{ inputs.jar-libs-dir }}
+        echo "::endgroup::"
+
+    - name: Store to latest
+      if: github.ref == 'refs/heads/main'
+      uses: ./.github/actions/store-to-latest
+      with:
+        asset-filename: ${{ inputs.jar-name }}.jar
+        github-token: ${{ inputs.github-token-latest }}
+
+    - name: Store to release
+      if: startsWith(github.ref, 'refs/tags/')
+      uses: ./.github/actions/store-to-release
+      with:
+        asset-filename: ${{ inputs.jar-name }}.jar
+        github-token: ${{ inputs.github-token-release }}

.github/actions/add-package/action.yml

@@ -11,10 +11,15 @@ inputs:
     description: token to upload package to release
   shell:
     default: bash
+outputs:
+  install-path:
+    description: path to the installation directory
+    value: ${{ steps.create-zip.outputs.install-path }}
 runs:
   using: composite
   steps:
     - name: Create ZIP file
+      id: create-zip
       shell: ${{ inputs.shell }}
       run: |
         echo "::group::Create ZIP file"
@@ -39,21 +44,22 @@ runs:
           fi
         fi
 
-        # Copy COPYING file and licenses directory to install directory
-        cp COPYING ${{ inputs.build-dir }}/install/
+        # Copy AUTHORS and COPYING files and licenses directory to install directory
+        cp AUTHORS COPYING ${{ inputs.build-dir }}/install/
         cp -r licenses ${{ inputs.build-dir }}/install/
 
         # Create ZIP file
         pushd ${{ inputs.build-dir }}
         mv install ${{ inputs.package-name }}
+        echo "install-path=${{ inputs.build-dir }}/${{ inputs.package-name }}" >> $GITHUB_OUTPUT
         zip -r ${{ inputs.package-name }} ${{ inputs.package-name }}
         popd
 
         # Move package to root directory
         mv ${{ inputs.build-dir }}/${{ inputs.package-name }}.zip .
         echo "::endgroup::"
 
-    - name: install pyGithub
+    - name: Install pyGithub
       shell: ${{ inputs.shell }}
       run: |
         # Upgrading pyopenssl resolves the following error:
@@ -64,82 +70,14 @@ runs:
 
     - name: Store to latest
       if: github.ref == 'refs/heads/main'
-      shell: 'python3 {0}'
-      env:
-        GITHUB_TOKEN: ${{ inputs.github-token-latest }}
-        PACKAGE: ${{ inputs.package-name }}.zip
-      run: |
-        import datetime
-        import os
-        from github import Github
-
-        sha = os.getenv('GITHUB_SHA')
-
-        gh = Github(os.getenv('GITHUB_TOKEN'))
-        repo = gh.get_repo(os.getenv('GITHUB_REPOSITORY'))
-
-        try:
-          ref = repo.get_git_ref('tags/latest')
-          # update "latest" to current commit if sha changed
-          if ref.object.sha != sha:
-            ref.edit(sha)
-        except:
-          print('tag `latest` does not exist.')
-          exit
-
-        try:
-          rel = repo.get_release('latest')
-        except:
-          print('New `latest` release')
-          rel = repo.create_git_release('latest', 'latest', 'Latest builds')
-
-        # generate new filename
-        package = os.getenv('PACKAGE')
-        name,ext = os.path.splitext(package)
-        curtime = repo.get_git_commit(sha).committer.date.strftime('%Y-%m-%d')
-        samedayprefix = '{}-{}-'.format(name, curtime)
-        filename = '{}-{}-{}{}'.format(name, curtime, sha[:7], ext)
-
-        # prune old commits
-        assets = list(rel.get_assets())
-        assets.sort(key=lambda x: x.created_at, reverse=True)
-
-        for cnt,asset in enumerate(assets):
-          delete = False
-          # We generate 10 artifacts per build:
-          # {Linux-x86_64, Linux-arm64, macOS-x86_64, macOS-arm64, Win64-x86_64} * {static, shared}
-          if cnt >= 20: # Keep at most 2 builds
-            delete = True
-          if asset.name.startswith(samedayprefix):
-            delete = True
-          # convert to timezone-aware datetime
-          age = datetime.datetime.now().replace(tzinfo=datetime.timezone.utc) - asset.created_at
-          if age.days > 7:
-            delete = True
-          if delete:
-            asset.delete_asset()
-
-        # upload as asset with proper name
-        rel.upload_asset(package, name=filename)
+      uses: ./.github/actions/store-to-latest
+      with:
+        asset-filename: ${{ inputs.package-name }}.zip
+        github-token: ${{ inputs.github-token-latest }}
 
     - name: Store to release
       if: startsWith(github.ref, 'refs/tags/')
-      shell: 'python3 {0}'
-      env:
-        GITHUB_TOKEN: ${{ inputs.github-token-release }}
-        PACKAGE: ${{ inputs.package-name }}.zip
-      run: |
-        import os
-        from github import Github
-
-        refname = os.getenv('GITHUB_REF_NAME')
-        gh = Github(os.getenv('GITHUB_TOKEN'))
-        repo = gh.get_repo(os.getenv('GITHUB_REPOSITORY'))
-        try:
-          rel = repo.get_release(refname)
-        except:
-          print("New release from " + refname)
-          ref = repo.get_git_ref('tags/' + refname)
-          commit = repo.get_git_commit(ref.object.sha)
-          rel = repo.create_git_release(refname, refname, commit.message)
-        rel.upload_asset(os.getenv('PACKAGE'))
+      uses: ./.github/actions/store-to-release
+      with:
+        asset-filename: ${{ inputs.package-name }}.zip
+        github-token: ${{ inputs.github-token-release }}

.github/actions/run-tests/action.yml

@@ -64,6 +64,8 @@ runs:
           export PATH="${{ inputs.build-dir }}/install/bin:$PATH"
           export CMAKE_GENERATOR="MSYS Makefiles"
         fi
+        export CFLAGS=-Werror
+        export CXXFLAGS=-Werror
         cmake .. -DCMAKE_PREFIX_PATH=${{ inputs.build-dir }}/install/lib/cmake \
           -DPython_EXECUTABLE=$(command -v python3)
         make -j${{ env.num_proc }}

.github/actions/setup-cache/action.yml

@@ -3,6 +3,10 @@ description: Setup caches (ccache, contribs and dependencies)
 inputs:
   cache-key:
     default: "none"
+  install-ethos:
+    default: false
+  install-carcara:
+    default: false
   shell:
     default: bash
 
@@ -61,8 +65,13 @@ runs:
       if: steps.contrib-cache.outputs.cache-hit != 'true'
       shell: ${{ inputs.shell }}
       run: |
-        ./contrib/get-carcara-checker
-        ./contrib/get-ethos-checker
+        mkdir -p ./deps/bin
+        if [ "${{ inputs.install-carcara }}" = "true" ]; then
+          ./contrib/get-carcara-checker
+        fi
+        if [ "${{ inputs.install-ethos }}" = "true" ]; then
+          ./contrib/get-ethos-checker
+        fi
 
     - name: Setup dependencies cache
       uses: actions/cache@v4

.github/actions/store-to-latest/action.yml

@@ -0,0 +1,70 @@
+name: Store to latest
+description: Store an asset on the release page associated to the latest tag
+inputs:
+  asset-filename:
+    description: filename of the asset
+  github-token:
+    description: token to upload asset to latest
+
+runs:
+  using: composite
+  steps:
+    - name: Store to latest
+      shell: 'python3 {0}'
+      env:
+        GITHUB_TOKEN: ${{ inputs.github-token }}
+        PACKAGE: ${{ inputs.asset-filename }}
+      run: |
+        import datetime
+        import os
+        from github import Github
+
+        sha = os.getenv('GITHUB_SHA')
+
+        gh = Github(os.getenv('GITHUB_TOKEN'))
+        repo = gh.get_repo(os.getenv('GITHUB_REPOSITORY'))
+
+        try:
+          ref = repo.get_git_ref('tags/latest')
+          # update "latest" to current commit if sha changed
+          if ref.object.sha != sha:
+            ref.edit(sha)
+        except:
+          print('tag `latest` does not exist.')
+          exit
+
+        try:
+          rel = repo.get_release('latest')
+        except:
+          print('New `latest` release')
+          rel = repo.create_git_release('latest', 'latest', 'Latest builds')
+
+        # generate new filename
+        package = os.getenv('PACKAGE')
+        name,ext = os.path.splitext(package)
+        curtime = repo.get_git_commit(sha).committer.date.strftime('%Y-%m-%d')
+        samedayprefix = '{}-{}-'.format(name, curtime)
+        filename = '{}-{}-{}{}'.format(name, curtime, sha[:7], ext)
+
+        # prune old commits
+        assets = list(rel.get_assets())
+        assets.sort(key=lambda x: x.created_at, reverse=True)
+
+        for cnt,asset in enumerate(assets):
+          delete = False
+          # We generate 10 packages per build:
+          # {Linux-x86_64, Linux-arm64, macOS-x86_64, macOS-arm64, Win64-x86_64} * {static, shared}
+          # and 4 JARS {Linux-x86_64, macOS-x86_64, macOS-arm64, Win64-x86_64}
+          if cnt >= 28: # Keep at most 2 builds
+            delete = True
+          if asset.name.startswith(samedayprefix):
+            delete = True
+          # convert to timezone-aware datetime
+          age = datetime.datetime.now().replace(tzinfo=datetime.timezone.utc) - asset.created_at
+          if age.days > 7:
+            delete = True
+          if delete:
+            asset.delete_asset()
+
+        # upload as asset with proper name
+        rel.upload_asset(package, name=filename)

.github/actions/store-to-release/action.yml

@@ -0,0 +1,31 @@
+name: Store to release
+description: Store an asset on the release page associated to current release
+inputs:
+  asset-filename:
+    description: filename of the asset
+  github-token:
+    description: token to upload asset to current release
+
+runs:
+  using: composite
+  steps:
+    - name: Store to release
+      shell: 'python3 {0}'
+      env:
+        GITHUB_TOKEN: ${{ inputs.github-token }}
+        PACKAGE: ${{ inputs.asset-filename }}
+      run: |
+        import os
+        from github import Github
+
+        refname = os.getenv('GITHUB_REF_NAME')
+        gh = Github(os.getenv('GITHUB_TOKEN'))
+        repo = gh.get_repo(os.getenv('GITHUB_REPOSITORY'))
+        try:
+          rel = repo.get_release(refname)
+        except:
+          print("New release from " + refname)
+          ref = repo.get_git_ref('tags/' + refname)
+          commit = repo.get_git_commit(ref.object.sha)
+          rel = repo.create_git_release(refname, refname, commit.message)
+        rel.upload_asset(os.getenv('PACKAGE'))