From 7012b44e0d36e1e8f07025fc76a20dc7bc01a009 Mon Sep 17 00:00:00 2001 From: Florian Schanda Date: Sat, 17 Aug 2024 22:53:44 +0200 Subject: [PATCH] Update to PyVCG 1.0.7 and CVC 1.2.0 (#95) This add CVC5 API support on Windows, making the external binary unnecessary. Because CVC5 packaging changed we now need a special script to fetch it. We can now also support Python 3.12. --- .github/workflows/ci.yml | 16 +++---- .github/workflows/docs.yml | 12 +++--- .gitignore | 4 ++ CHANGELOG.md | 4 ++ MODULE.bazel | 18 ++++---- Makefile | 1 - documentation/TUTORIAL-INSTALL.md | 4 +- documentation/TUTORIAL-LINT.md | 8 ++-- requirements.txt | 4 +- setup.py | 12 +----- util/fetch_cvc5.py | 71 +++++++++++++++++++++++++++++++ 11 files changed, 111 insertions(+), 43 deletions(-) create mode 100755 util/fetch_cvc5.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d781a8da..36e772be 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -33,22 +33,16 @@ jobs: py-version: ["3.8", "3.9", "3.10", "3.11", "3.12"] include: - os: ubuntu-latest - cvc5: "Linux" + cvc5-plat: "linux" - os: macos-13 brew: "/usr/local" - cvc5: "macOS" + cvc5-plat: "osx13" - os: macos-14 brew: "/opt/homebrew" - cvc5: "macOS-arm64" + cvc5-plat: "osx14" runs-on: ${{ matrix.os }} steps: - 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-${{ matrix.cvc5 }}' - name: 'cvc5' - version: '1.0.8' - name: Install python version if: matrix.os != 'macos-14' || matrix.py-version == '3.11' || matrix.py-version == '3.12' uses: actions/setup-python@v5 @@ -69,6 +63,10 @@ jobs: run: | brew install make echo "${{ matrix.brew }}/opt/make/libexec/gnubin" >> $GITHUB_PATH + - name: Fetch CVC5 + run: | + util/fetch_cvc5.py 1.2.0 ${{ matrix.cvc5-plat }} + echo "$GITHUB_WORKSPACE" >> $GITHUB_PATH - name: Executing unit tests run: | make unit-tests diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index d0a4b5eb..0a73264b 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -32,11 +32,6 @@ jobs: uses: actions/checkout@v4 with: fetch-depth: 0 - - 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@v5 with: @@ -48,6 +43,13 @@ jobs: pip install bmw-lobster-core bmw-lobster-tool-python pip install --no-deps bmw-lobster-tool-trlc sudo apt-get install -y graphviz + - name: Fetch CVC5 + run: | + util/fetch_cvc5.py 1.2.0 linux + echo "$GITHUB_WORKSPACE" >> $GITHUB_PATH + - name: Test CVC5 + run: | + cvc5 --version - name: Generate docs run: | make docs diff --git a/.gitignore b/.gitignore index d90d539c..56e6ac6b 100644 --- a/.gitignore +++ b/.gitignore @@ -19,3 +19,7 @@ dist # Build-System ignores bazel-* + +# Special ignores for CI +cvc5 +cvc5.exe diff --git a/CHANGELOG.md b/CHANGELOG.md index 32dbb5ec..ae09fbcb 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -52,6 +52,10 @@ changes. These have been tagged in the changelog. backwards incompatible change as it may invalidate some previously valid `.trlc` or `.rsl` files. +* [TRLC] The `--verify` command is now supported on Windows without + the use of an external `cvc5` install, now that the Python package + for CVC5 is also available on Windows. + * [TRLC, LRM] New builtin function `oneof`. This can be used to test if precisely one of a number of parameters is true. For example: diff --git a/MODULE.bazel b/MODULE.bazel index fb4a054b..30d06461 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -33,23 +33,23 @@ http_archive = use_repo_rule("@bazel_tools//tools/build_defs/repo:http.bzl", "ht http_archive( name = "cvc5_linux", build_file = "@trlc//:cvc5.BUILD", - sha256 = "cf291aef67da8eaa8d425a51f67f3f72f36db8b1040655dc799b64e3d69e6086", - strip_prefix = "cvc5-Linux-static", - url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-Linux-static.zip", + sha256 = "ab9344e2dddda794669c888a3afcd99f25f2627e1d426bd7d08ecb267361b331", + strip_prefix = "cvc5-Linux-x86_64-static-gpl", + url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Linux-x86_64-static-gpl.zip", ) http_archive( name = "cvc5_mac", build_file = "@trlc//:cvc5.BUILD", - sha256 = "561a5ee82416441fa616c6f416ecaae2fa2dfc06dc81c2c6cc8dcfb31936e326", - strip_prefix = "cvc5-macOS-static", - url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-macOS-static.zip", + sha256 = "2b983ca743ef1327b51408bf8ba6c08c97beaadde2c3968da701ca16bb1e3740", + strip_prefix = "cvc5-macOS-arm64-static-gpl", + url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-macOS-arm64-static-gpl.zip", ) http_archive( name = "cvc5_windows", build_file = "@trlc//:cvc5.BUILD", - sha256 = "f06715b796020c810b2713e6df3969dae99d38c24d2a6eac225a029fc70fe1ee", - strip_prefix = "cvc5-Win64-static", - url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-Win64-static.zip", + sha256 = "256f4af3f4181e770801df436852cb3c76c86dbf9b69a47064d7f8d5bc0ee1d2", + strip_prefix = "cvc5-Win64-x86_64-static", + url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Win64-x86_64-static.zip", ) diff --git a/Makefile b/Makefile index 14b752cb..812c641e 100644 --- a/Makefile +++ b/Makefile @@ -57,7 +57,6 @@ docs: package: @git clean -xdf @python3 setup.py sdist bdist_wheel - @python3 setup.py bdist_wheel -p manylinux2014_x86_64 upload-main: package python3 -m twine upload --repository pypi dist/* diff --git a/documentation/TUTORIAL-INSTALL.md b/documentation/TUTORIAL-INSTALL.md index ad7c2734..2b4f5596 100644 --- a/documentation/TUTORIAL-INSTALL.md +++ b/documentation/TUTORIAL-INSTALL.md @@ -10,9 +10,9 @@ The easiest way to install the tools is through PyPI: $ pip3 install --user trlc ``` -There are currently one required dependencies (PyVCG which should be +There is currently only one required dependency (PyVCG which should be installed automatically), all you need is a moderatly recent Python -3.8 / 3.9 / 3.10 / 3.11. +3.8 / 3.9 / 3.10 / 3.11 / 3.12. Don't forget to adjust your `PATH` so that `.local/bin` (or the equivalent on Windows) is on it; so that the `trlc` executable can be diff --git a/documentation/TUTORIAL-LINT.md b/documentation/TUTORIAL-LINT.md index ed1a602e..86c55931 100644 --- a/documentation/TUTORIAL-LINT.md +++ b/documentation/TUTORIAL-LINT.md @@ -10,16 +10,14 @@ deployed and used. This is enabled by default, but you can turn these off with the `--no-lint` option. To enable more detailed checks you can also use the `--verify` -feature, but please note that this is only available on Linux, and -requires you to have installed the optional dependency -[CVC5](https://pypi.org/project/cvc5). +feature. ```bash $ trlc --verify DIRECTORIES_OR_FILES ``` -If you are on Windows or Linux, you can also download the CVC5 -executables and ask TRLC to use them directly: +If the API for CVC5 isn't avialable on your platform, then you can +also download the CVC5 executables and ask TRLC to use them directly: ```bash $ trlc --verify --use-cvc5-binary=path/to/cvc5.exe DIRECTORIES_OR_FILES diff --git a/requirements.txt b/requirements.txt index b4b45cef..036eb7fc 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1,2 +1,2 @@ -pyvcg==1.0.6 -cvc5>=1.1.1; sys.platform == "linux" or sys.platform == "darwin" +pyvcg==1.0.7 +cvc5>=1.2.0 diff --git a/setup.py b/setup.py index 66f604e1..5b843df3 100644 --- a/setup.py +++ b/setup.py @@ -30,14 +30,6 @@ "Source Code" : version.CODE_URL, } -required_packages = [] -python_required = ">=3.8, <4" -if "--plat-name" in sys.argv or "-p" in sys.argv: - required_packages.append("PyVCG[api]==1.0.6") - python_required = ">=3.8, <3.12" -else: - required_packages.append("PyVCG==1.0.6") - setuptools.setup( name="trlc", version=version.TRLC_VERSION, @@ -50,8 +42,8 @@ project_urls=project_urls, license="GNU General Public License v3", packages=setuptools.find_packages(), - install_requires=required_packages, - python_requires=python_required, + install_requires="PyVCG[api]==1.0.7", + python_requires=">=3.8, <3.13", classifiers=[ "Development Status :: 5 - Production/Stable", "Environment :: Console", diff --git a/util/fetch_cvc5.py b/util/fetch_cvc5.py new file mode 100755 index 00000000..1f4973e8 --- /dev/null +++ b/util/fetch_cvc5.py @@ -0,0 +1,71 @@ +#!/usr/bin/env python3 +# +# TRLC - Treat Requirements Like Code +# Copyright (C) 2024 Florian Schanda +# +# This file is part of the TRLC Python Reference Implementation. +# +# TRLC is free software: you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation, either version 3 of the License, or +# (at your option) any later version. +# +# TRLC is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with TRLC. If not, see . + +# This utility script fetches and unpacks CVC5 binaries for use in CI. + +import os +import urllib.request +import io +import zipfile +import argparse +import stat + +CVC5_RELEASES = "http://github.com/cvc5/cvc5/releases/download" +CVC5_BINARY = "cvc5" +CVC5_EXECUTABLE = True + +ap = argparse.ArgumentParser() +ap.add_argument("version") +ap.add_argument("platform") + +options = ap.parse_args() + +CVC5_VERSION = options.version + +if options.platform == "linux": + CVC5_PLATFORM = "Linux-x86_64-static" +elif options.platform == "osx13": + CVC5_PLATFORM = "macOS-x86_64-static" +elif options.platform == "osx14": + CVC5_PLATFORM = "macOS-arm64-static" +elif options.platform == "windows": + CVC5_PLATFORM = "Win64-x86_64-static" + CVC5_BINARY = "cvc5.exe" + CVC5_EXECUTABLE = False +else: + ap.error("unknown platform") + +print ("Downloading CVC5 archive (%s, %s)" % (CVC5_VERSION, CVC5_PLATFORM)) +with urllib.request.urlopen("%s/cvc5-%s/cvc5-%s.zip" % + (CVC5_RELEASES, + CVC5_VERSION, + CVC5_PLATFORM)) as fd: + content = fd.read() + +print ("Extracting %s" % CVC5_BINARY) +with zipfile.ZipFile(io.BytesIO(content)) as zf: + with zf.open("cvc5-%s/bin/%s" % (CVC5_PLATFORM, + CVC5_BINARY)) as fd: + with open(CVC5_BINARY, "wb") as fd_out: + fd_out.write(fd.read()) + +if CVC5_EXECUTABLE: + print("Setting executable bit") + os.chmod(CVC5_BINARY, stat.S_IRUSR | stat.S_IWUSR | stat.S_IXUSR)