From 09009d77698578e274758de8ad9ee8c93236db69 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 28 Aug 2024 15:02:07 -0600 Subject: [PATCH 1/8] Cleanup CI steps (#4611) This is some changes I noticed we can make to CI: - We remove the job "post performance numbers", which hasn't worked for at least 6 months: https://github.com/runtimeverification/k/actions/runs/8081624497 - Update some actions that were giving deprecated Node.js warnings. --- .github/workflows/develop.yml | 56 ----------------------------------- .github/workflows/release.yml | 2 +- 2 files changed, 1 insertion(+), 57 deletions(-) diff --git a/.github/workflows/develop.yml b/.github/workflows/develop.yml index c3623290323..745a9c7ade9 100644 --- a/.github/workflows/develop.yml +++ b/.github/workflows/develop.yml @@ -37,59 +37,3 @@ jobs: if git add --update && git commit --no-edit --allow-empty --message "Set Version: $(cat package/version)"; then git push origin master fi - - post-performance-tests: - name: 'Performance Tests' - runs-on: [self-hosted, linux, normal] - continue-on-error: true - steps: - - uses: actions/checkout@v4 - - name: 'Set up Docker Test Image' - env: - BASE_OS: ubuntu - BASE_DISTRO: jammy - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - BENCHER_API_TOKEN: ${{ secrets.BENCHER_API_TOKEN }} - BENCHER_PROJECT: k-framework - BENCHER_ADAPTER: json - run: | - set -euxo pipefail - workspace=$(pwd) - docker run --name "k-posting-profiling-tests-${GITHUB_SHA}" \ - --rm -it --detach \ - -e BENCHER_API_TOKEN="$BENCHER_API_TOKEN" \ - -e BENCHER_PROJECT="$BENCHER_PROJECT" \ - -e BENCHER_ADAPTER="$BENCHER_ADAPTER" \ - -e GITHUB_HEAD_REF="$GITHUB_HEAD_REF" \ - -e GITHUB_BASE_REF="$GITHUB_BASE_REF" \ - -e GITHUB_TOKEN="$GITHUB_TOKEN" \ - -e GITHUB_ACTIONS=true \ - -e GITHUB_EVENT_NAME="$GITHUB_EVENT_NAME" \ - -e GITHUB_EVENT_PATH="$GITHUB_EVENT_PATH" \ - -e GITHUB_REPOSITORY="$GITHUB_REPOSITORY" \ - -e GITHUB_REF="$GITHUB_REF" \ - -e GITHUB_SHA="$GITHUB_SHA" \ - --workdir /opt/workspace \ - -v "${workspace}:/opt/workspace" \ - -v "${GITHUB_EVENT_PATH}:${GITHUB_EVENT_PATH}" \ - "${BASE_OS}:${BASE_DISTRO}" - - name: 'Setting up dependencies' - run: | - set -euxo pipefail - docker exec -t "k-posting-profiling-tests-${GITHUB_SHA}" /bin/bash -c './k-distribution/tests/profiling/setup_profiling.sh SKIP_K_BUILD' - - name: 'Getting Performance Tests Results' - run: | - set -euxo pipefail - docker exec -t "k-posting-profiling-tests-${GITHUB_SHA}" /bin/bash -c './k-distribution/tests/profiling/post_results_to_develop.py "${GITHUB_SHA}"' - - name: 'Posting Performance Tests Results' - run: | - set -euxo pipefail - docker exec -t "k-posting-profiling-tests-${GITHUB_SHA}" /bin/bash -c 'bencher run \ - --if-branch "develop" --else-if-branch "master" \ - --file .profiling-results.json --err --ci-only-on-alert \ - --github-actions "${GITHUB_TOKEN}" "echo Exporting report"' - - name: 'Tear down Docker' - if: always() - run: | - docker stop --time=0 "k-posting-profiling-tests-${GITHUB_SHA}" - docker container rm --force "k-posting-profiling-tests-${GITHUB_SHA}" || true diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 43aa7207fb2..3ed90fe2f00 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -76,7 +76,7 @@ jobs: name: k-framework-binary - name: 'Publish K to k-framework-binary cache' - uses: workflow/nix-shell-action@v3.3.0 + uses: workflow/nix-shell-action@v3.3.2 env: CACHIX_AUTH_TOKEN: '${{ secrets.CACHIX_PRIVATE_KFB_TOKEN }}' GC_DONT_GC: '1' From 07685d9137e896a21643ceab2a60c19ff150444f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Thu, 29 Aug 2024 18:02:27 +0200 Subject: [PATCH 2/8] Move bug report handling from `Transport` to `JsonRpcClient` (#4529) Blocked on: * ~#4524~ Since transport-specific files are no longer added to the bug report (e.g. commands for sending a request), bug report handling can be performed in the client. --- pyk/src/pyk/kore/rpc.py | 110 +++++++-------------- pyk/src/tests/unit/kore/test_rpc_client.py | 2 +- 2 files changed, 39 insertions(+), 73 deletions(-) diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 3ce2031e643..ecd5ca94ed2 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -57,45 +57,16 @@ def __init__(self, message: str, code: int, data: Any = None): class Transport(ContextManager['Transport'], ABC): - _bug_report: BugReport | None - _bug_report_id: str | None - - def __init__(self, bug_report_id: str | None = None, bug_report: BugReport | None = None) -> None: - if (bug_report_id is None and bug_report is not None) or (bug_report_id is not None and bug_report is None): - raise ValueError('bug_report and bug_report_id must be passed together.') - self._bug_report_id = bug_report_id - self._bug_report = bug_report def request(self, req: str, request_id: str, method_name: str) -> str: - base_name = self._bug_report_id if self._bug_report_id is not None else 'kore_rpc' - req_name = f'{base_name}/{id(self)}/{request_id}' - if self._bug_report: - bug_report_request = f'{req_name}_request.json' - self._bug_report.add_file_contents(req, Path(bug_report_request)) - self._bug_report.add_request(f'{req_name}_request.json') - server_addr = self._description() _LOGGER.info(f'Sending request to {server_addr}: {request_id} - {method_name}') _LOGGER.debug(f'Sending request to {server_addr}: {req}') resp = self._request(req) _LOGGER.info(f'Received response from {server_addr}: {request_id} - {method_name}') _LOGGER.debug(f'Received response from {server_addr}: {resp}') - - if self._bug_report: - bug_report_response = f'{req_name}_response.json' - self._bug_report.add_file_contents(resp, Path(bug_report_response)) - self._bug_report.add_request(f'{req_name}_response.json') return resp - @abstractmethod - def _command(self, req_name: str, bug_report_request: str) -> list[str]: ... - - @abstractmethod - def _request(self, req: str) -> str: ... - - @abstractmethod - def _description(self) -> str: ... - def __enter__(self) -> Transport: return self @@ -105,6 +76,12 @@ def __exit__(self, *args: Any) -> None: @abstractmethod def close(self) -> None: ... + @abstractmethod + def _request(self, req: str) -> str: ... + + @abstractmethod + def _description(self) -> str: ... + class TransportType(Enum): SINGLE_SOCKET = auto() @@ -124,10 +101,7 @@ def __init__( port: int, *, timeout: int | None = None, - bug_report_id: str | None = None, - bug_report: BugReport | None = None, ): - super().__init__(bug_report_id, bug_report) self._host = host self._port = port self._sock = self._create_connection(host, port, timeout) @@ -157,19 +131,6 @@ def close(self) -> None: self._file.close() self._sock.close() - def _command(self, req_name: str, bug_report_request: str) -> list[str]: - return [ - 'cat', - bug_report_request, - '|', - 'nc', - '-Nv', - self._host, - str(self._port), - '>', - f'{req_name}_actual.json', - ] - def _request(self, req: str) -> str: self._sock.sendall(req.encode()) server_addr = self._description() @@ -192,10 +153,7 @@ def __init__( port: int, *, timeout: int | None = None, - bug_report_id: str | None = None, - bug_report: BugReport | None = None, ): - super().__init__(bug_report_id, bug_report) self._host = host self._port = port self._timeout = timeout @@ -203,20 +161,6 @@ def __init__( def close(self) -> None: pass - def _command(self, req_name: str, bug_report_request: str) -> list[str]: - return [ - 'curl', - '-X', - 'POST', - '-H', - 'Content-Type: application/json', - '-d', - '@' + bug_report_request, - 'http://' + self._host + ':' + str(self._port), - '>', - f'{req_name}_actual.json', - ] - def _request(self, req: str) -> str: connection = http.client.HTTPConnection(self._host, self._port, timeout=self._timeout) connection.request('POST', '/', body=req, headers={'Content-Type': 'application/json'}) @@ -308,6 +252,9 @@ class JsonRpcClient(ContextManager['JsonRpcClient']): _transport: Transport _req_id: int + _bug_report: BugReport | None + _bug_report_id: str | None + def __init__( self, host: str, @@ -318,17 +265,23 @@ def __init__( bug_report_id: str | None = None, transport: TransportType = TransportType.SINGLE_SOCKET, ): - if transport is TransportType.SINGLE_SOCKET: - self._transport = SingleSocketTransport( - host, port, timeout=timeout, bug_report=bug_report, bug_report_id=bug_report_id - ) - elif transport is TransportType.HTTP: - self._transport = HttpTransport( - host, port, timeout=timeout, bug_report=bug_report, bug_report_id=bug_report_id - ) - else: - raise AssertionError() + if (bug_report is None) != (bug_report_id is None): + raise ValueError('bug_report and bug_report_id must be passed together.') + + self._transport = self._create_transport(transport, host=host, port=port, timeout=timeout) self._req_id = 1 + self._bug_report_id = bug_report_id + self._bug_report = bug_report + + @staticmethod + def _create_transport(transport: TransportType, *, host: str, port: int, timeout: int | None) -> Transport: + match transport: + case TransportType.SINGLE_SOCKET: + return SingleSocketTransport(host, port, timeout=timeout) + case TransportType.HTTP: + return HttpTransport(host, port, timeout=timeout) + case _: + raise AssertionError() def __enter__(self) -> JsonRpcClient: return self @@ -351,10 +304,23 @@ def request(self, method: str, **params: Any) -> dict[str, Any]: } req = json.dumps(payload) + + base_name = self._bug_report_id if self._bug_report_id is not None else 'kore_rpc' + req_name = f'{base_name}/{id(self)}/{req_id}' + if self._bug_report: + bug_report_request = f'{req_name}_request.json' + self._bug_report.add_file_contents(req, Path(bug_report_request)) + self._bug_report.add_request(f'{req_name}_request.json') + resp = self._transport.request(req, req_id, method) if not resp: raise RuntimeError('Empty response received') + if self._bug_report: + bug_report_response = f'{req_name}_response.json' + self._bug_report.add_file_contents(resp, Path(bug_report_response)) + self._bug_report.add_request(f'{req_name}_response.json') + data = json.loads(resp) self._check(data) assert data['id'] == req_id diff --git a/pyk/src/tests/unit/kore/test_rpc_client.py b/pyk/src/tests/unit/kore/test_rpc_client.py index cf69f1c5bf7..bb054849e3a 100644 --- a/pyk/src/tests/unit/kore/test_rpc_client.py +++ b/pyk/src/tests/unit/kore/test_rpc_client.py @@ -50,7 +50,7 @@ def transport(mock: Mock) -> MockTransport: @pytest.fixture def kore_client(mock: Mock, mock_class: Mock) -> Iterator[KoreClient]: # noqa: N803 client = KoreClient('localhost', 3000) - mock_class.assert_called_with('localhost', 3000, timeout=None, bug_report=None, bug_report_id=None) + mock_class.assert_called_with('localhost', 3000, timeout=None) assert client._client._default_client._transport == mock yield client client.close() From c6ea4fa46353effa98e7fd293e6a3da7acb1e1dd Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Mon, 2 Sep 2024 00:24:36 -0700 Subject: [PATCH 3/8] Set pyk version with `importlib.metadata.version` (#4615) Closes #4614 Uses `importlib.metadata.version` to read the version from `pyproject.toml` rather than manually `sed`ding. --- package/version.sh | 1 - pyk/src/pyk/__init__.py | 3 ++- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version.sh b/package/version.sh index afbcc381d46..d116348e1a0 100755 --- a/package/version.sh +++ b/package/version.sh @@ -27,7 +27,6 @@ version_sub() { sed --in-place 's/^version = ".*"$/version = "'${version}'"/' pyk/pyproject.toml sed --in-place "s/^version = '.*'$/version = '${version}'/" pyk/docs/conf.py sed --in-place "s/^release = '.*'$/release = '${version}'/" pyk/docs/conf.py - sed --in-place "s/^__version__: Final = '.*'/__version__: Final = '${version}'/" pyk/src/pyk/__init__.py } version_command="$1" ; shift diff --git a/pyk/src/pyk/__init__.py b/pyk/src/pyk/__init__.py index de9e67e7176..4f4439e92e3 100644 --- a/pyk/src/pyk/__init__.py +++ b/pyk/src/pyk/__init__.py @@ -1,9 +1,10 @@ from __future__ import annotations +from importlib.metadata import version from typing import TYPE_CHECKING if TYPE_CHECKING: from typing import Final -__version__: Final = '7.1.0' +__version__: Final = version('kframework') From 96584223bd0c0ec952b370e1714fad5135d59270 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Mon, 2 Sep 2024 04:02:38 -0600 Subject: [PATCH 4/8] Update dependency: web/k-web-theme (#4619) Co-authored-by: devops --- web/k-web-theme | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/web/k-web-theme b/web/k-web-theme index 2721031a0d2..f022ffcbbb2 160000 --- a/web/k-web-theme +++ b/web/k-web-theme @@ -1 +1 @@ -Subproject commit 2721031a0d266510193b05091e0d3291823f456e +Subproject commit f022ffcbbb2c110ddfe13e6f5a7e9cd3f584ce7c From dc4e8d99f044bad2430a1f0be7397bce5ef0edea Mon Sep 17 00:00:00 2001 From: Samuel Balco Date: Tue, 3 Sep 2024 08:52:46 +0100 Subject: [PATCH 5/8] Update poetry2nix (#4620) Update poetry2nix as it was pinned to a version that's almost 1 year old. This gets rid of the annoying warning ``` trace: warning: `pythonForBuild` (from `python*`) has been renamed to `pythonOnBuildForHost` ``` Also remove the pyk flake, remnant of the merger of pyk back into k --- flake.lock | 8 +-- flake.nix | 21 ++++--- pyk/flake.lock | 168 ------------------------------------------------- pyk/flake.nix | 34 ---------- 4 files changed, 16 insertions(+), 215 deletions(-) delete mode 100644 pyk/flake.lock delete mode 100644 pyk/flake.nix diff --git a/flake.lock b/flake.lock index a015a126835..c13a7aab56b 100644 --- a/flake.lock +++ b/flake.lock @@ -175,17 +175,17 @@ "treefmt-nix": "treefmt-nix" }, "locked": { - "lastModified": 1698640399, - "narHash": "sha256-mXzyx79/iFLZ0UDuSkqgFfejYRcSJfsCnJ9WlMusaI0=", + "lastModified": 1725253878, + "narHash": "sha256-HwXut4WbOUAjmybhui2eNSE6+Wb0nigYgDzBBOZaPG4=", "owner": "nix-community", "repo": "poetry2nix", - "rev": "626111646fe236cb1ddc8191a48c75e072a82b7c", + "rev": "0d3fad5740d892487805cd2d60d8e4ed828486e9", "type": "github" }, "original": { "owner": "nix-community", + "ref": "2024.9.219347", "repo": "poetry2nix", - "rev": "626111646fe236cb1ddc8191a48c75e072a82b7c", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 5498172f7c0..4b00526f6a6 100644 --- a/flake.nix +++ b/flake.nix @@ -9,8 +9,7 @@ }; poetry2nix = { - url = - "github:nix-community/poetry2nix/626111646fe236cb1ddc8191a48c75e072a82b7c"; + url = "github:nix-community/poetry2nix/2024.9.219347"; inputs.nixpkgs.follows = "llvm-backend/nixpkgs"; }; @@ -94,9 +93,8 @@ "org.checkerframework:checker-qual:3.33.0" "com.google.errorprone:error_prone_annotations:2.18.0" ]; - manualMvnSourceArtifacts = [ - "org.scala-sbt:compiler-bridge_2.13:1.8.0" - ]; + manualMvnSourceArtifacts = + [ "org.scala-sbt:compiler-bridge_2.13:1.8.0" ]; inherit (final) maven; inherit (prev) llvm-backend; clang = prev."clang_${toString final.llvm-version}"; @@ -210,13 +208,18 @@ }; }; defaultPackage = packages.k; - devShells.kore-integration-tests = pkgs.kore-tests (pkgs.mk-k-framework { - inherit (pkgs) haskell-backend-bins; - llvm-kompile-libs = { }; - }); + devShells.kore-integration-tests = pkgs.kore-tests + (pkgs.mk-k-framework { + inherit (pkgs) haskell-backend-bins; + llvm-kompile-libs = { }; + }); }) // { overlays.llvm-backend = llvm-backend.overlays.default; overlays.z3 = haskell-backend.overlays.z3; + overlays.pyk = (import ./nix/pyk-overlay.nix { + inherit poetry2nix; + projectDir = ./pyk; + }); overlay = nixpkgs.lib.composeManyExtensions allOverlays; }; diff --git a/pyk/flake.lock b/pyk/flake.lock deleted file mode 100644 index 9dc8c707f7a..00000000000 --- a/pyk/flake.lock +++ /dev/null @@ -1,168 +0,0 @@ -{ - "nodes": { - "flake-utils": { - "inputs": { - "systems": "systems" - }, - "locked": { - "lastModified": 1694529238, - "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=", - "owner": "numtide", - "repo": "flake-utils", - "rev": "ff7b65b44d01cf9ba6a71320833626af21126384", - "type": "github" - }, - "original": { - "owner": "numtide", - "repo": "flake-utils", - "type": "github" - } - }, - "nix-github-actions": { - "inputs": { - "nixpkgs": [ - "poetry2nix", - "nixpkgs" - ] - }, - "locked": { - "lastModified": 1693660503, - "narHash": "sha256-B/g2V4v6gjirFmy+I5mwB2bCYc0l3j5scVfwgl6WOl8=", - "owner": "nix-community", - "repo": "nix-github-actions", - "rev": "bd5bdbb52350e145c526108f4ef192eb8e554fa0", - "type": "github" - }, - "original": { - "owner": "nix-community", - "repo": "nix-github-actions", - "type": "github" - } - }, - "nixpkgs": { - "locked": { - "lastModified": 1716457947, - "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", - "owner": "nixos", - "repo": "nixpkgs", - "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", - "type": "github" - }, - "original": { - "owner": "nixos", - "repo": "nixpkgs", - "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", - "type": "github" - } - }, - "poetry2nix": { - "inputs": { - "flake-utils": "flake-utils", - "nix-github-actions": "nix-github-actions", - "nixpkgs": [ - "nixpkgs" - ], - "systems": "systems_2", - "treefmt-nix": "treefmt-nix" - }, - "locked": { - "lastModified": 1698640399, - "narHash": "sha256-mXzyx79/iFLZ0UDuSkqgFfejYRcSJfsCnJ9WlMusaI0=", - "owner": "nix-community", - "repo": "poetry2nix", - "rev": "626111646fe236cb1ddc8191a48c75e072a82b7c", - "type": "github" - }, - "original": { - "owner": "nix-community", - "repo": "poetry2nix", - "rev": "626111646fe236cb1ddc8191a48c75e072a82b7c", - "type": "github" - } - }, - "root": { - "inputs": { - "flake-utils": [ - "poetry2nix", - "flake-utils" - ], - "nixpkgs": [ - "rv-utils", - "nixpkgs" - ], - "poetry2nix": "poetry2nix", - "rv-utils": "rv-utils" - } - }, - "rv-utils": { - "inputs": { - "nixpkgs": "nixpkgs" - }, - "locked": { - "lastModified": 1716459074, - "narHash": "sha256-IpahO+EkWdGl9QP7B2YXfJWpSfghjxgpz4ab47nRJY4=", - "owner": "runtimeverification", - "repo": "rv-nix-tools", - "rev": "a65058865cda201de504f5546271b8e997a0be9c", - "type": "github" - }, - "original": { - "owner": "runtimeverification", - "repo": "rv-nix-tools", - "type": "github" - } - }, - "systems": { - "locked": { - "lastModified": 1681028828, - "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", - "owner": "nix-systems", - "repo": "default", - "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", - "type": "github" - }, - "original": { - "owner": "nix-systems", - "repo": "default", - "type": "github" - } - }, - "systems_2": { - "locked": { - "lastModified": 1681028828, - "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", - "owner": "nix-systems", - "repo": "default", - "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", - "type": "github" - }, - "original": { - "id": "systems", - "type": "indirect" - } - }, - "treefmt-nix": { - "inputs": { - "nixpkgs": [ - "poetry2nix", - "nixpkgs" - ] - }, - "locked": { - "lastModified": 1697388351, - "narHash": "sha256-63N2eBpKaziIy4R44vjpUu8Nz5fCJY7okKrkixvDQmY=", - "owner": "numtide", - "repo": "treefmt-nix", - "rev": "aae39f64f5ecbe89792d05eacea5cb241891292a", - "type": "github" - }, - "original": { - "owner": "numtide", - "repo": "treefmt-nix", - "type": "github" - } - } - }, - "root": "root", - "version": 7 -} diff --git a/pyk/flake.nix b/pyk/flake.nix deleted file mode 100644 index 4063dda846f..00000000000 --- a/pyk/flake.nix +++ /dev/null @@ -1,34 +0,0 @@ -{ - description = "Application packaged using poetry2nix"; - - inputs = { - rv-utils.url = "github:runtimeverification/rv-nix-tools"; - nixpkgs.follows = "rv-utils/nixpkgs"; - poetry2nix = { - url = - "github:nix-community/poetry2nix/626111646fe236cb1ddc8191a48c75e072a82b7c"; - inputs.nixpkgs.follows = "nixpkgs"; - }; - flake-utils.follows = "poetry2nix/flake-utils"; - }; - - outputs = { self, nixpkgs, flake-utils, rv-utils, poetry2nix }: - { - # Nixpkgs overlay providing the application - overlay = (import ../nix/pyk-overlay.nix { - inherit poetry2nix; - projectDir = ./.; - }); - } // (flake-utils.lib.eachDefaultSystem (system: - let - pkgs = import nixpkgs { - inherit system; - overlays = [ self.overlay ]; - }; - in { - packages = { - inherit (pkgs) pyk pyk-python310 pyk-python311; - default = pkgs.pyk; - }; - })); -} From f5e2adc80000ed58877c94bdb65a7811129c8d2a Mon Sep 17 00:00:00 2001 From: Samuel Balco Date: Tue, 3 Sep 2024 16:35:56 +0100 Subject: [PATCH 6/8] Fix MacOS brew release (#4622) It looks like the semantics of `brew tap` have changed from `brew` version `4.3.16` to `4.3.18` (a recent change to the public github macos runners). `brew tap` now no longer takes an arbitrary `file://...` path... the path must be a git repo. The fix seems to be to `git init` the folder before calling `brew tap` --- .github/workflows/release.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 3ed90fe2f00..18771602a9d 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -301,6 +301,8 @@ jobs: # test suite, so the PL-tutorial is disabled for now. # - https://github.com/runtimeverification/k/issues/3705 cd homebrew-k-old + # brew tap expects a git repository, so we initialise the current folder as a dummy repo + git init brew tap runtimeverification/k "file:///$(pwd)" brew install ${{ needs.macos-build.outputs.bottle_path }} -v # cp -R /usr/local/share/kframework/pl-tutorial ~ From b4f86f2cc00e5fe50a9afb4fb5313cd2edabf2ef Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 3 Sep 2024 12:11:48 -0500 Subject: [PATCH 7/8] add ubuntu noble release (#4608) This PR adds a release docker image and ubuntu package for Ubuntu Noble. --- .github/workflows/Dockerfile | 1 - .github/workflows/release.yml | 63 ++++++++++++++++++- .../debian/kframework-frontend/control.jammy | 2 +- package/debian/kframework/compat.noble | 1 + package/debian/kframework/control.jammy | 2 +- package/debian/kframework/control.noble | 18 ++++++ package/debian/kframework/rules.noble | 43 +++++++++++++ package/docker/Dockerfile.ubuntu-jammy | 7 ++- package/docker/Dockerfile.ubuntu-noble | 29 +++++++++ pyk/poetry.lock | 2 +- pyk/pyproject.toml | 2 +- 11 files changed, 162 insertions(+), 8 deletions(-) create mode 100644 package/debian/kframework/compat.noble create mode 100644 package/debian/kframework/control.noble create mode 100755 package/debian/kframework/rules.noble create mode 100644 package/docker/Dockerfile.ubuntu-noble diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile index 422333bb4e6..d8444685e6b 100644 --- a/.github/workflows/Dockerfile +++ b/.github/workflows/Dockerfile @@ -63,7 +63,6 @@ RUN apt-get update \ pkg-config \ python3 \ python3-dev \ - python3-distutils \ python3-pip \ xxd \ zlib1g-dev diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 18771602a9d..d7bdae44813 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -87,6 +87,67 @@ jobs: kup publish k-framework-binary .#k --keep-days 180 kup publish k-framework-binary .#k.openssl.procps.secp256k1 --keep-days 180 + ubuntu-noble: + name: 'K Ubuntu Noble Package' + runs-on: [self-hosted, linux, normal] + timeout-minutes: 90 + steps: + - uses: actions/checkout@v4 + - name: 'Build and Test Package' + uses: ./.github/actions/test-package + with: + os: ubuntu + distro: noble + llvm: 16 + jdk: 21 + pkg-name: kframework_amd64_ubuntu_noble.deb + build-package: package/debian/build-package noble kframework + test-package: package/debian/test-package + - name: 'Upload the package built to the Summary Page' + uses: actions/upload-artifact@v4 + with: + name: kframework_amd64_ubuntu_noble.deb + path: kframework_amd64_ubuntu_noble.deb + if-no-files-found: error + retention-days: 1 + - name: 'Upload Package to Release' + env: + GITHUB_TOKEN: ${{ secrets.JENKINS_GITHUB_PAT }} + run: | + set -x + version=$(cat package/version) + cp kframework_amd64_ubuntu_noble.deb "kframework_${version}_amd64_ubuntu_noble.deb" + gh release upload --repo runtimeverification/k --clobber "v${version}" "kframework_${version}_amd64_ubuntu_noble.deb" + - name: 'Build, Test, and Push Dockerhub Image' + shell: bash {0} + env: + DOCKERHUB_PASSWORD: ${{ secrets.DOCKERHUB_PASSWORD }} + DOCKERHUB_REPO: runtimeverificationinc/kframework-k + run: | + set -euxo pipefail + version=$(cat package/version) + version_tag=ubuntu-noble-${version} + docker login --username rvdockerhub --password "${DOCKERHUB_PASSWORD}" + docker image build . --file package/docker/Dockerfile.ubuntu-noble --tag "${DOCKERHUB_REPO}:${version_tag}" + docker run --name "k-package-docker-test-noble-${GITHUB_SHA}" --rm -it --detach "${DOCKERHUB_REPO}:${version_tag}" + docker exec -t "k-package-docker-test-noble-${GITHUB_SHA}" bash -c 'cd ~ && echo "module TEST imports BOOL endmodule" > test.k' + docker exec -t "k-package-docker-test-noble-${GITHUB_SHA}" bash -c 'cd ~ && kompile test.k --backend llvm' + docker exec -t "k-package-docker-test-noble-${GITHUB_SHA}" bash -c 'cd ~ && kompile test.k --backend haskell' + docker exec -t "k-package-docker-test-noble-${GITHUB_SHA}" bash -c 'cd ~ && pyk kompile test.k --backend llvm' + docker exec -t "k-package-docker-test-noble-${GITHUB_SHA}" bash -c 'cd ~ && pyk kompile test.k --backend haskell' + docker image push "${DOCKERHUB_REPO}:${version_tag}" + - name: 'Clean up Docker Container' + if: always() + run: | + docker stop --time=0 "k-package-docker-test-noble-${GITHUB_SHA}" + - name: On Failure, Upload the kore-exec.tar.gz file to the Summary Page + if: failure() + uses: actions/upload-artifact@v4 + with: + name: kore-exec.tar.gz + path: | + **/kore-exec.tar.gz + ubuntu-jammy: name: 'K Ubuntu Jammy Package' runs-on: [self-hosted, linux, normal] @@ -359,7 +420,7 @@ jobs: name: 'Publish Release' runs-on: [self-hosted, linux, normal] environment: production - needs: [cachix-release, macos-test, source-tarball, ubuntu-jammy, set-release-id] + needs: [cachix-release, macos-test, source-tarball, ubuntu-jammy, ubuntu-noble, set-release-id] steps: - name: 'Check out code' uses: actions/checkout@v4 diff --git a/package/debian/kframework-frontend/control.jammy b/package/debian/kframework-frontend/control.jammy index f885518c546..b16e23ba4da 100644 --- a/package/debian/kframework-frontend/control.jammy +++ b/package/debian/kframework-frontend/control.jammy @@ -2,7 +2,7 @@ Source: kframework-frontend Section: devel Priority: optional Maintainer: Tamas Toth -Build-Depends: debhelper (>=10) , flex , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , zlib1g-dev +Build-Depends: debhelper (>=10) , flex , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-pip , zlib1g-dev Standards-Version: 3.9.6 Homepage: https://github.com/runtimeverification/k diff --git a/package/debian/kframework/compat.noble b/package/debian/kframework/compat.noble new file mode 100644 index 00000000000..f599e28b8ab --- /dev/null +++ b/package/debian/kframework/compat.noble @@ -0,0 +1 @@ +10 diff --git a/package/debian/kframework/control.jammy b/package/debian/kframework/control.jammy index b8b3a5acdbf..6fcfc5e3f4a 100644 --- a/package/debian/kframework/control.jammy +++ b/package/debian/kframework/control.jammy @@ -2,7 +2,7 @@ Source: kframework Section: devel Priority: optional Maintainer: Dwight Guth -Build-Depends: clang-15 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libunwind-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , xxd , zlib1g-dev +Build-Depends: clang-15 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libunwind-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-pip , xxd , zlib1g-dev Standards-Version: 3.9.6 Homepage: https://github.com/runtimeverification/k diff --git a/package/debian/kframework/control.noble b/package/debian/kframework/control.noble new file mode 100644 index 00000000000..24f47adbf10 --- /dev/null +++ b/package/debian/kframework/control.noble @@ -0,0 +1,18 @@ +Source: kframework +Section: devel +Priority: optional +Maintainer: Dwight Guth +Build-Depends: clang-16 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libunwind-dev , libyaml-dev , maven , openjdk-21-jdk , pkg-config , python3 , python3-dev , python3-pip , xxd , zlib1g-dev +Standards-Version: 3.9.6 +Homepage: https://github.com/runtimeverification/k + +Package: kframework +Architecture: any +Section: devel +Priority: optional +Depends: bison , clang-16 , openjdk-21-jre-headless , flex , gcc , g++ , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-1 , libtinfo-dev , libunwind-dev , libyaml-0-2 , libz3-4 , lld-16 , llvm-16 , pkg-config +Recommends: z3 +Description: K framework toolchain + Includes K Framework compiler for K language definitions, and K interpreter + and prover for programs written in languages defined in K. +Homepage: https://github.com/runtimeverification/k diff --git a/package/debian/kframework/rules.noble b/package/debian/kframework/rules.noble new file mode 100755 index 00000000000..f6c8af748f7 --- /dev/null +++ b/package/debian/kframework/rules.noble @@ -0,0 +1,43 @@ +#!/usr/bin/make -f +# See debhelper(7) (uncomment to enable) +# output every command that modifies files on the build system. +#export DH_VERBOSE = 1 + + +# see FEATURE AREAS in dpkg-buildflags(1) + +# The LLVM backend is built using Clang, which is incompatible with LTO flags +# added by default in newer versions of dpkg. +# https://wiki.debian.org/ToolChain/LTO +export DEB_BUILD_MAINT_OPTIONS=hardening=-stackprotector optimize=-lto + +# see ENVIRONMENT in dpkg-buildflags(1) +# package maintainers to append CFLAGS +#export DEB_CFLAGS_MAINT_APPEND = -Wall -pedantic +# package maintainers to append LDFLAGS +#export DEB_LDFLAGS_MAINT_APPEND = -Wl,--as-needed + +DESTDIR=$(shell pwd)/debian/kframework +PREFIX=/usr +PYTHON_VERSION=python3.10 +PYTHON_DEB_VERSION=python3 +export DESTDIR +export PREFIX + +%: + dh $@ + +override_dh_auto_build: + mvn --batch-mode package -DskipTests -Dllvm.backend.prefix=$(PREFIX) -Dllvm.backend.destdir=$(DESTDIR) + +override_dh_auto_install: + package/package + +override_dh_strip: + dh_strip -Xliballoc.a -Xlibarithmetic.a -XlibAST.a -Xlibutil.a -XlibParser.a -Xlibcollect.a -Xlibcollections.a -Xlibjson.a -Xlibstrings.a -Xlibmeta.a -Xlibio.a + +# dh_make generated override targets +# This is example for Cmake (See https://bugs.debian.org/641051 ) +#override_dh_auto_configure: +# dh_auto_configure -- # -DCMAKE_LIBRARY_PATH=$(DEB_HOST_MULTIARCH) + diff --git a/package/docker/Dockerfile.ubuntu-jammy b/package/docker/Dockerfile.ubuntu-jammy index 7d8b63fe984..60b3eee5ee1 100644 --- a/package/docker/Dockerfile.ubuntu-jammy +++ b/package/docker/Dockerfile.ubuntu-jammy @@ -9,7 +9,8 @@ RUN apt-get update \ build-essential \ git \ python3 \ - python3-pip + python3-pip \ + pipx COPY kframework_amd64_ubuntu_jammy.deb /kframework_amd64_ubuntu_jammy.deb RUN apt-get update \ @@ -17,7 +18,9 @@ RUN apt-get update && apt-get install --yes --no-install-recommends /kframework_amd64_ubuntu_jammy.deb COPY pyk /pyk -RUN pip install poetry \ +RUN pipx install poetry \ + && pipx ensurepath \ + && . /root/.profile \ && cd /pyk \ && make build \ && pip install dist/*.whl \ diff --git a/package/docker/Dockerfile.ubuntu-noble b/package/docker/Dockerfile.ubuntu-noble new file mode 100644 index 00000000000..acd3882b7d4 --- /dev/null +++ b/package/docker/Dockerfile.ubuntu-noble @@ -0,0 +1,29 @@ +FROM runtimeverificationinc/z3:ubuntu-noble-4.13.0 + +ENV TZ=America/Chicago +RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone + +RUN apt-get update \ + && apt-get upgrade --yes \ + && apt-get install --yes \ + build-essential \ + git \ + python3 \ + python3-pip \ + pipx + +COPY kframework_amd64_ubuntu_noble.deb /kframework_amd64_ubuntu_noble.deb +RUN apt-get update \ + && apt-get upgrade --yes \ + && apt-get install --yes --no-install-recommends /kframework_amd64_ubuntu_noble.deb + +COPY pyk /pyk +RUN pipx install poetry \ + && pipx ensurepath \ + && . /root/.profile \ + && cd /pyk \ + && make build \ + && pip install dist/*.whl --break-system-packages \ + && rm -rf /pyk + +RUN rm -rf /kframework_amd64_ubuntu_noble.deb diff --git a/pyk/poetry.lock b/pyk/poetry.lock index 9de7d3ec3b6..81d40e2ee1b 100644 --- a/pyk/poetry.lock +++ b/pyk/poetry.lock @@ -1054,4 +1054,4 @@ test = ["big-O", "importlib-resources", "jaraco.functools", "jaraco.itertools", [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "7888201fe916d5896a73a6bedf4367e437bd8807dad0ef19175db10165d07404" +content-hash = "ceee3227b60208193d4f1cdbbb5fd52ea428e31f521d3e9226234827615fc732" diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml index 3be1e5f6207..a56b90d220f 100644 --- a/pyk/pyproject.toml +++ b/pyk/pyproject.toml @@ -22,7 +22,7 @@ coloredlogs = "^15.0.1" filelock = "^3.9.0" graphviz = "^0.20.1" hypothesis = "^6.103.1" -psutil = "5.9.5" +psutil = "^5.9.5" pybind11 = "^2.10.3" pytest = "*" textual = "^0.27.0" From 4e44f2dbe3fa7fd164711bf5bc20a4045224b437 Mon Sep 17 00:00:00 2001 From: Freeman <105403280+F-WRunTime@users.noreply.github.com> Date: Tue, 3 Sep 2024 14:26:18 -0600 Subject: [PATCH 8/8] release.yml: On failure run publish with verbose option enabled (#4623) On failure we need more informaiton why the upload to cachix failed. More information is always needed. --- .github/workflows/release.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index d7bdae44813..a89d1cef418 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -84,9 +84,9 @@ jobs: packages: jq script: | export PATH="$(nix build github:runtimeverification/kup --no-link --json | jq -r '.[].outputs | to_entries[].value')/bin:$PATH" - kup publish k-framework-binary .#k --keep-days 180 - kup publish k-framework-binary .#k.openssl.procps.secp256k1 --keep-days 180 - + kup publish --verbose k-framework-binary .#k --keep-days 180 + kup publish --verbose k-framework-binary .#k.openssl.procps.secp256k1 --keep-days 180 + ubuntu-noble: name: 'K Ubuntu Noble Package' runs-on: [self-hosted, linux, normal]