diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile index 9d550930a5c..26b22baa0de 100644 --- a/.github/workflows/Dockerfile +++ b/.github/workflows/Dockerfile @@ -47,6 +47,7 @@ RUN apt-get update \ libncurses5-dev \ libnss3-dev \ libreadline-dev \ + libsecp256k1-dev \ libsqlite3-dev \ libssl-dev \ libyaml-dev \ diff --git a/.github/workflows/Dockerfile.stack-deps b/.github/workflows/Dockerfile.stack-deps index 6e4b9b72328..0bb07c8cfd1 100644 --- a/.github/workflows/Dockerfile.stack-deps +++ b/.github/workflows/Dockerfile.stack-deps @@ -9,7 +9,9 @@ RUN apt-get update \ && apt-get upgrade --yes \ && apt-get install --yes \ curl \ - libtinfo-dev + libsecp256k1-dev \ + libtinfo-dev \ + pkg-config RUN curl -sSL https://get.haskellstack.org/ | sh @@ -31,4 +33,4 @@ RUN cd /home/$USER/.tmp-haskell && stack build --only-snapshot ENV LC_ALL=C.UTF-8 ADD --chown=$USER:$GROUP hs-backend-booster/src/main/native/hs-backend-booster/stack.yaml /home/$USER/.tmp-booster/ ADD --chown=$USER:$GROUP hs-backend-booster/src/main/native/hs-backend-booster/package.yaml /home/$USER/.tmp-booster/ -RUN cd /home/$USER/.tmp-booster && stack build --only-snapshot \ No newline at end of file +RUN cd /home/$USER/.tmp-booster && stack build --only-snapshot diff --git a/deps/hs-backend-booster_release b/deps/hs-backend-booster_release index bc188d4565e..70e31b8f616 100644 --- a/deps/hs-backend-booster_release +++ b/deps/hs-backend-booster_release @@ -1 +1 @@ -6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566 +5a283f7c85c5b4f66ff477b494c5d138c54706e6 diff --git a/flake.lock b/flake.lock index eb116e388aa..88ee862d917 100644 --- a/flake.lock +++ b/flake.lock @@ -47,17 +47,17 @@ ] }, "locked": { - "lastModified": 1695839205, - "narHash": "sha256-9USUlWcL4YOseMJdQ1h4XvihR4/FG5zykykI7eY/13A=", + "lastModified": 1696961955, + "narHash": "sha256-HvYHO0Jo7NeV0u2Qi883rsuMyergBCcnbh/lbCGiFug=", "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566", + "rev": "5a283f7c85c5b4f66ff477b494c5d138c54706e6", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566", + "rev": "5a283f7c85c5b4f66ff477b494c5d138c54706e6", "type": "github" } }, @@ -247,11 +247,11 @@ "flake-compat_4": { "flake": false, "locked": { - "lastModified": 1696267196, - "narHash": "sha256-AAQ/2sD+0D18bb8hKuEEVpHUYD1GmO2Uh/taFamn6XQ=", + "lastModified": 1696426674, + "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", "owner": "edolstra", "repo": "flake-compat", - "rev": "4f910c9827911b1ec2bf26b5a062cd09f8d89f85", + "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", "type": "github" }, "original": { @@ -439,17 +439,17 @@ "z3-src": "z3-src" }, "locked": { - "lastModified": 1695129967, - "narHash": "sha256-wLMrn/a10zH3Zvl+ln2Z37b8n4c013i+udkKfFf61Eg=", + "lastModified": 1696881510, + "narHash": "sha256-NBYDOHpFy0/EGQtg1VeJWn7c8ciAZkhoflf0ZOTsVQs=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "63397c713d21322434d572281c1407d929a1189e", + "rev": "cdc83446c302961cd6abd2bca8c3e73dde8f6eab", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "85b5d086840a0f1e89499f086b50d7258598fc8b", + "rev": "cdc83446c302961cd6abd2bca8c3e73dde8f6eab", "type": "github" } }, @@ -465,17 +465,17 @@ "z3-src": "z3-src_2" }, "locked": { - "lastModified": 1695129967, - "narHash": "sha256-wLMrn/a10zH3Zvl+ln2Z37b8n4c013i+udkKfFf61Eg=", + "lastModified": 1696881510, + "narHash": "sha256-NBYDOHpFy0/EGQtg1VeJWn7c8ciAZkhoflf0ZOTsVQs=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "63397c713d21322434d572281c1407d929a1189e", + "rev": "cdc83446c302961cd6abd2bca8c3e73dde8f6eab", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "63397c713d21322434d572281c1407d929a1189e", + "rev": "cdc83446c302961cd6abd2bca8c3e73dde8f6eab", "type": "github" } }, @@ -1227,11 +1227,11 @@ }, "nixpkgs_5": { "locked": { - "lastModified": 1696039360, - "narHash": "sha256-g7nIUV4uq1TOVeVIDEZLb005suTWCUjSY0zYOlSBsyE=", + "lastModified": 1696983906, + "narHash": "sha256-L7GyeErguS7Pg4h8nK0wGlcUTbfUMDu+HMf1UcyP72k=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "32dcb45f66c0487e92db8303a798ebc548cadedc", + "rev": "bd1cde45c77891214131cbbea5b1203e485a9d51", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 441f83602c1..8823dd35c94 100644 --- a/flake.nix +++ b/flake.nix @@ -2,9 +2,9 @@ description = "K Framework"; inputs = { nixpkgs.url = "nixpkgs/nixos-23.05"; - haskell-backend.url = "github:runtimeverification/haskell-backend/63397c713d21322434d572281c1407d929a1189e"; + haskell-backend.url = "github:runtimeverification/haskell-backend/cdc83446c302961cd6abd2bca8c3e73dde8f6eab"; booster-backend = { - url = "github:runtimeverification/hs-backend-booster/6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566"; + url = "github:runtimeverification/hs-backend-booster/5a283f7c85c5b4f66ff477b494c5d138c54706e6"; # NB booster-backend will bring in another dependency on haskell-backend, # but the two are not necessarily the same (different more often than not). # We get two transitive dependencies on haskell-nix. diff --git a/haskell-backend/src/main/native/haskell-backend b/haskell-backend/src/main/native/haskell-backend index 63397c713d2..cdc83446c30 160000 --- a/haskell-backend/src/main/native/haskell-backend +++ b/haskell-backend/src/main/native/haskell-backend @@ -1 +1 @@ -Subproject commit 63397c713d21322434d572281c1407d929a1189e +Subproject commit cdc83446c302961cd6abd2bca8c3e73dde8f6eab diff --git a/hs-backend-booster/src/main/native/hs-backend-booster b/hs-backend-booster/src/main/native/hs-backend-booster index 6c2f5ab988e..5a283f7c85c 160000 --- a/hs-backend-booster/src/main/native/hs-backend-booster +++ b/hs-backend-booster/src/main/native/hs-backend-booster @@ -1 +1 @@ -Subproject commit 6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566 +Subproject commit 5a283f7c85c5b4f66ff477b494c5d138c54706e6 diff --git a/package/arch/Dockerfile b/package/arch/Dockerfile index 1dfbce7dd9c..9cd5c8568b6 100644 --- a/package/arch/Dockerfile +++ b/package/arch/Dockerfile @@ -27,6 +27,7 @@ RUN pacman -Sy --noconfirm archlinux-keyring \ hub \ jdk-openjdk \ jemalloc \ + libsecp256k1 \ libyaml \ lld \ llvm \ diff --git a/package/arch/Dockerfile.stack-deps b/package/arch/Dockerfile.stack-deps index 42d333b5952..2c4c3954a4c 100644 --- a/package/arch/Dockerfile.stack-deps +++ b/package/arch/Dockerfile.stack-deps @@ -6,7 +6,9 @@ RUN pacman -Sy --noconfirm archlinux-keyring \ && pacman -Syyu --noconfirm \ && pacman -S --noconfirm \ clang \ + libsecp256k1 \ make \ + pkgconf \ stack # The image is built specifically for an environment with this user/group diff --git a/package/arch/PKGBUILD b/package/arch/PKGBUILD index 562d5f62cc4..79e754c33e6 100644 --- a/package/arch/PKGBUILD +++ b/package/arch/PKGBUILD @@ -8,7 +8,7 @@ arch=('x86_64') url="https://github.com/runtimeverification/k" license=('custom') groups=() -depends=( 'bison' 'clang' 'diffutils' 'flex' 'fmt' 'gawk' 'gcc' 'gettext' 'gmp' 'grep' 'java-runtime' 'jemalloc' 'libyaml' 'lld' 'llvm' 'make' 'mpfr' 'patch' 'python' 'tar' 'z3' ) +depends=( 'bison' 'clang' 'diffutils' 'flex' 'fmt' 'gawk' 'gcc' 'gettext' 'gmp' 'grep' 'java-runtime' 'jemalloc' 'libsecp256k1' 'libyaml' 'lld' 'llvm' 'make' 'mpfr' 'patch' 'python' 'tar' 'z3' ) makedepends=( 'boost' 'cmake' 'jdk-openjdk' 'maven' 'python' 'zlib' ) checkdepends=() optdepends=() diff --git a/package/debian/Dockerfile b/package/debian/Dockerfile index 740695c6ccd..17f432244b6 100644 --- a/package/debian/Dockerfile +++ b/package/debian/Dockerfile @@ -30,6 +30,7 @@ RUN apt-get update \ libncurses5-dev \ libnss3-dev \ libreadline-dev \ + libsecp256k1-dev \ libsqlite3-dev \ libssl-dev \ libyaml-dev \ diff --git a/package/debian/compat.focal b/package/debian/compat.focal deleted file mode 100644 index ec635144f60..00000000000 --- a/package/debian/compat.focal +++ /dev/null @@ -1 +0,0 @@ -9 diff --git a/package/debian/control.bookworm b/package/debian/control.bookworm index 7a03ddd4132..dffbfae42c7 100644 --- a/package/debian/control.bookworm +++ b/package/debian/control.bookworm @@ -2,7 +2,7 @@ Source: kframework Section: devel Priority: optional Maintainer: Dwight Guth -Build-Depends: clang-14 , cmake , debhelper (>=9) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libyaml-dev , maven , openjdk-17-jdk , zlib1g-dev +Build-Depends: clang-14 , cmake , debhelper (>=9) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , zlib1g-dev Standards-Version: 3.9.6 Homepage: https://github.com/runtimeverification/k @@ -10,7 +10,7 @@ Package: kframework Architecture: any Section: devel Priority: optional -Depends: bison , clang-14 , default-jre-headless , flex , gcc , g++ , libboost-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libyaml-0-2 , libz3-4 , lld-14 , pkg-config , llvm-14 +Depends: bison , clang-14 , default-jre-headless , flex , gcc , g++ , libboost-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-1 , libyaml-0-2 , libz3-4 , lld-14 , pkg-config , llvm-14 Recommends: z3 Description: K framework toolchain Includes K Framework compiler for K language definitions, and K interpreter diff --git a/package/debian/control.focal b/package/debian/control.focal deleted file mode 100644 index 0d94ac2922f..00000000000 --- a/package/debian/control.focal +++ /dev/null @@ -1,18 +0,0 @@ -Source: kframework -Section: devel -Priority: optional -Maintainer: Dwight Guth -Build-Depends: clang-12 , cmake , debhelper (>=9) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libyaml-dev , maven , openjdk-11-jdk , python3 , python3-dev , python3-distutils , python3-pip , zlib1g-dev -Standards-Version: 3.9.6 -Homepage: https://github.com/runtimeverification/k - -Package: kframework -Architecture: any -Section: devel -Priority: optional -Depends: bison , clang-12 , default-jre-headless , flex , gcc , g++ , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libtinfo-dev , libyaml-0-2 , libz3-4 , lld-12 , llvm-12 , 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/control.jammy b/package/debian/control.jammy index de8d652e60b..30972fdf9c1 100644 --- a/package/debian/control.jammy +++ b/package/debian/control.jammy @@ -2,7 +2,7 @@ Source: kframework Section: devel Priority: optional Maintainer: Dwight Guth -Build-Depends: clang-14 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , zlib1g-dev +Build-Depends: clang-14 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , zlib1g-dev Standards-Version: 3.9.6 Homepage: https://github.com/runtimeverification/k @@ -10,7 +10,7 @@ Package: kframework Architecture: any Section: devel Priority: optional -Depends: bison , clang-14 , default-jre-headless , flex , gcc , g++ , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libtinfo-dev , libyaml-0-2 , libz3-4 , lld-14 , llvm-14 , pkg-config +Depends: bison , clang-14 , default-jre-headless , flex , gcc , g++ , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-0 , libtinfo-dev , libyaml-0-2 , libz3-4 , lld-14 , llvm-14 , pkg-config Recommends: z3 Description: K framework toolchain Includes K Framework compiler for K language definitions, and K interpreter diff --git a/package/debian/rules.focal b/package/debian/rules.focal deleted file mode 100755 index 500d34c1e09..00000000000 --- a/package/debian/rules.focal +++ /dev/null @@ -1,39 +0,0 @@ -#!/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) -export DEB_BUILD_MAINT_OPTIONS=hardening=-stackprotector - -# 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.8 -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) -