From ff1da0af52a2707765668297590f992c5179f5e2 Mon Sep 17 00:00:00 2001 From: "Curt J. Sampson" Date: Tue, 23 Jul 2024 22:41:52 +0900 Subject: [PATCH 1/3] install-build-deps script (#4505) Add an `install-build-deps` script to replace the manual commands in the README. See commit message(s) for details. __WARNING:__ This commit is based on the commit in #4054; if you merge this it will merge that one too. (The script includes the `libunwind-dev` package added in that commit.) You'll probably want to do a quick check that this works on MacOS and update the commit message appropriately. --- README.md | 77 ++++++++--------------------------------- install-build-deps | 85 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 99 insertions(+), 63 deletions(-) create mode 100755 install-build-deps diff --git a/README.md b/README.md index 87b0fe2e016..9ecd37bcb1b 100644 --- a/README.md +++ b/README.md @@ -56,7 +56,7 @@ for details about supported configurations and system setup. ## Contents 1. [Prerequisite Install Guide](#prerequisite-install-guide) -2. [Build and Install Guide](#build-and-install-guide) +2. [Build and Install Guide] 3. [IDE Setup](#ide-setup) 4. [Running the Test Suite](#running-the-test-suite) 5. [Changing the KORE Data Structures](#changing-the-kore-data-structures) @@ -72,69 +72,13 @@ must first be installed. ## The Short Version -On Ubuntu Linux 22.04 (Jammy): +Regardless of system, unless you cloned with `--recusrive` you will first +have to run `git submodule update --init --recursive`. -```shell -git submodule update --init --recursive -sudo apt-get install \ - bison \ - build-essential \ - clang-15 \ - cmake \ - curl \ - flex \ - g++ \ - gcc \ - libboost-test-dev \ - libfmt-dev \ - libgmp-dev \ - libjemalloc-dev \ - libmpfr-dev \ - libsecp256k1-dev \ - libunwind-dev \ - libyaml-dev \ - libz3-dev \ - lld-15 \ - llvm-15-tools \ - m4 \ - maven \ - openjdk-17-jdk \ - pkg-config \ - python3 \ - python3-dev \ - z3 \ - zlib1g-dev -curl -sSL https://get.haskellstack.org/ | sh -``` - -If you install this list of dependencies, continue directly to the [Build and Install Guide](#build-and-install-guide). - -On macOS using [Homebrew](https://brew.sh/): - -```shell -git submodule update --init --recursive -brew install \ - bison \ - boost \ - cmake \ - flex \ - fmt \ - gcc \ - gmp \ - openjdk \ - jemalloc \ - libyaml \ - llvm \ - make \ - maven \ - mpfr \ - pkg-config \ - python \ - secp256k1 \ - stack \ - zlib \ - z3 -``` +You then need the build and runtime dependencies. If you are on a +Debian-based system (including Ubuntu) or MacOS with [Homebrew] installed, +you can run `./install-build-deps` and continue directly to the +[Build and Install Guide]. ## The Long Version @@ -451,3 +395,10 @@ of artifacts, you can run `mvn dependency:purge-local-repository`. If tests fail but you want to run the build anyway to see what happens, you can use `mvn package -DskipTests`. If you still cannot build, please contact a K developer. + + + + +[Build and Install Guide]: #build-and-install-guide + +[Homebrew]: https://brew.sh/ diff --git a/install-build-deps b/install-build-deps new file mode 100755 index 00000000000..ee741eca574 --- /dev/null +++ b/install-build-deps @@ -0,0 +1,85 @@ +#!/usr/bin/env bash +# +# Install OS packages containing dependencies required to build K. +# +set -Eeuo pipefail + +die() { local ec="$1"; shift; echo "ERROR: $@"; exit $ec; } + +inst_Debian() { + echo '===== Debian packages:' + sudo apt-get install -q \ + bison \ + build-essential \ + clang-15 \ + cmake \ + curl \ + flex \ + g++ \ + gcc \ + libboost-test-dev \ + libfmt-dev \ + libgmp-dev \ + libjemalloc-dev \ + libmpfr-dev \ + libsecp256k1-dev \ + libunwind-dev \ + libyaml-dev \ + libz3-dev \ + lld-15 \ + llvm-15-tools \ + m4 \ + maven \ + openjdk-17-jdk \ + pkg-config \ + python3 \ + python3-dev \ + z3 \ + zlib1g-dev + + if stack --version >/dev/null 2>&1; then + echo 'Using existing Haskell Stack installation.' + else + echo '===== Haskell Stack:' + curl -sSL https://get.haskellstack.org/ | sh + fi +} + +inst_MacOS() { + echo '===== Brew packages' + brew install \ + bison \ + boost \ + cmake \ + flex \ + fmt \ + gcc \ + gmp \ + openjdk \ + jemalloc \ + libyaml \ + llvm \ + make \ + maven \ + mpfr \ + pkg-config \ + python \ + secp256k1 \ + stack \ + zlib \ + z3 +} + +try() { + local command="$1"; shift + local platform="$1"; shift + + echo "===== Checking for $command for platform $platform" + $command --version >/dev/null 2>&1 || return 1 + echo "----- Found platform $platform" + inst_$platform +} + +try apt-get Debian && exit 0 +try brew MacOS && exit 0 +die 1 'Cannot find known platform. Your system appears to be unsupported.' From 353900c69bf2d5601a2683535acb93b47ed5fe9f Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Tue, 23 Jul 2024 15:42:05 -0600 Subject: [PATCH 2/3] Update dependency: deps/llvm-backend_release (#4547) Co-authored-by: devops --- deps/llvm-backend_release | 2 +- flake.lock | 8 ++++---- flake.nix | 2 +- llvm-backend/src/main/native/llvm-backend | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index a2d633db704..fbde3d5aeca 100644 --- a/deps/llvm-backend_release +++ b/deps/llvm-backend_release @@ -1 +1 @@ -0.1.61 +0.1.62 diff --git a/flake.lock b/flake.lock index 4051802a0a8..c374cf23c70 100644 --- a/flake.lock +++ b/flake.lock @@ -112,16 +112,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1721723305, - "narHash": "sha256-o2fmSDY7quhyUPieiMotHVAeIdfbh0IPTD+YSzb1EjM=", + "lastModified": 1721760167, + "narHash": "sha256-WLW4i4vsdAMVjUZBXH2y0tsIlpKV8hH/ejk7HQq5anI=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "a77c3ece39529bf3e5364719154ac60b80d17db6", + "rev": "9b505eafb2b47848f3b7ca16dc88f011651f5e2c", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.61", + "ref": "v0.1.62", "repo": "llvm-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index 43877cc2f15..57f51f1d0b1 100644 --- a/flake.nix +++ b/flake.nix @@ -1,7 +1,7 @@ { description = "K Framework"; inputs = { - llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.61"; + llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.62"; haskell-backend = { url = "github:runtimeverification/haskell-backend/v0.1.46"; inputs.rv-utils.follows = "llvm-backend/rv-utils"; diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index a77c3ece395..9b505eafb2b 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit a77c3ece39529bf3e5364719154ac60b80d17db6 +Subproject commit 9b505eafb2b47848f3b7ca16dc88f011651f5e2c From ae6d41980a2fdb6e98db5479ebf56a1595b1ed75 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 24 Jul 2024 18:27:35 +0200 Subject: [PATCH 3/3] Use `gnu` tar format for the bug reports (#4548) This change enforces the GNU format of tar files instead of the default POSIX.1-2001 pax format. This is necessary because: - the filenames in the bug reports are often longer than the format-portable restriction of 256 characters - the Haskell [library](https://hackage.haskell.org/package/tar-0.6.3.0/changelog) we use to work with tar does not support the pax format. However, it does support the GNU format which also allows long names. --- pyk/src/pyk/utils.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/utils.py b/pyk/src/pyk/utils.py index 04c650482e2..243acda6280 100644 --- a/pyk/src/pyk/utils.py +++ b/pyk/src/pyk/utils.py @@ -681,7 +681,7 @@ def __init__(self, bug_report: Path) -> None: def add_file(self, finput: Path, arcname: Path) -> None: if str(finput) not in self._file_remap: self._file_remap[str(finput)] = str(arcname) - with tarfile.open(self._bug_report, 'a') as tar: + with tarfile.open(self._bug_report, 'a', format=tarfile.GNU_FORMAT) as tar: tar.add(finput, arcname=arcname) _LOGGER.info(f'Added file to bug report {self._bug_report}:{arcname}: {finput}')