Merge remote-tracking branch 'origin/master' into new-type-inference

.github/actions/with-docker/action.yml

@@ -42,20 +42,13 @@ runs:
     run: |
       set -euxo pipefail
 
-      Z3_VERSION=4.8.15
+      Z3_VERSION=$(cat deps/z3)
       K_VERSION=$(cat ${SUBDIR}package/version)
       USER=$(id -un)
       USER_ID=$(id -u)
       GROUP=$(id -gn)
       GROUP_ID=$(id -g)
 
-      docker build ${SUBDIR}                                          \
-          --build-arg USER=${USER} --build-arg USER_ID=${USER_ID}     \
-          --build-arg GROUP=${GROUP} --build-arg GROUP_ID=${GROUP_ID} \
-          --build-arg BASE_OS=${BASE_OS}                              \
-          --build-arg BASE_DISTRO=${BASE_DISTRO}                      \
-          --tag z3:${BASE_DISTRO}-${Z3_VERSION}                       \
-          --file ${SUBDIR}${DOCKERFILE}.z3
       docker build ${SUBDIR}                                          \
           --build-arg USER=${USER} --build-arg USER_ID=${USER_ID}     \
           --build-arg GROUP=${GROUP} --build-arg GROUP_ID=${GROUP_ID} \

.github/workflows/Dockerfile

@@ -1,8 +1,9 @@
 ARG BASE_OS
 ARG BASE_DISTRO
 ARG K_VERSION
+
 ARG Z3_VERSION
-FROM z3:${BASE_DISTRO}-${Z3_VERSION} as Z3
+FROM runtimeverificationinc/z3:${BASE_OS}-${BASE_DISTRO}-${Z3_VERSION} as Z3
 
 ARG BASE_OS
 ARG BASE_DISTRO
@@ -46,6 +47,7 @@ RUN    apt-get update              \
         libncurses5-dev            \
         libnss3-dev                \
         libreadline-dev            \
+        libsecp256k1-dev           \
         libsqlite3-dev             \
         libssl-dev                 \
         libyaml-dev                \

.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
+RUN cd /home/$USER/.tmp-booster && stack build --only-snapshot

.github/workflows/release.yml

@@ -63,7 +63,7 @@ jobs:
             trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
 
       - name: Upload release.nix
-        uses: ttuegel/upload-release.nix@v1.0
+        uses: runtimeverification/upload-release.nix@v1.1
         with:
           token: ${{ secrets.GITHUB_TOKEN }}
 
@@ -117,59 +117,7 @@ jobs:
           name: kore-exec.tar.gz
           path: |
             **/kore-exec.tar.gz
- 
-  ubuntu-focal:
-    name: 'K Ubuntu Focal Package'
-    runs-on: [self-hosted, linux, normal]
-    timeout-minutes: 90
-    steps:
-      - uses: actions/checkout@v3
-      - name: 'Build and Test Package'
-        uses: ./.github/actions/test-package
-        with:
-          os: ubuntu
-          distro: focal
-          llvm: 12
-          jdk: 11
-          pkg-name: kframework_amd64_ubuntu_focal.deb
-          build-package: package/debian/build-package focal
-          test-package: package/debian/test-package
-      - name: 'Upload Package to Release'
-        env:
-          GITHUB_TOKEN: ${{ secrets.JENKINS_GITHUB_PAT }}
-        run: |
-          set -x
-          version=$(cat package/version)
-          cp kframework_amd64_ubuntu_focal.deb kframework_${version}_amd64_ubuntu_focal.deb
-          gh release upload --repo runtimeverification/k --clobber v${version} kframework_${version}_amd64_ubuntu_focal.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-focal-${version}
-          docker login --username rvdockerhub --password ${DOCKERHUB_PASSWORD}
-          docker image build . --file package/docker/Dockerfile.ubuntu-focal --tag ${DOCKERHUB_REPO}:${version_tag}
-          docker run --name k-package-docker-test-focal-${GITHUB_SHA} --rm -it --detach ${DOCKERHUB_REPO}:${version_tag}
-          docker exec -t k-package-docker-test-focal-${GITHUB_SHA} bash -c 'cd ~ && echo "module TEST imports BOOL endmodule" > test.k'
-          docker exec -t k-package-docker-test-focal-${GITHUB_SHA} bash -c 'cd ~ && kompile test.k --backend llvm'
-          docker exec -t k-package-docker-test-focal-${GITHUB_SHA} bash -c 'cd ~ && 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-focal-${GITHUB_SHA}
-      - name: On Failure, Upload the kore-exec.tar.gz file to the Summary Page
-        if: failure()
-        uses: actions/upload-artifact@v2
-        with:
-          name: kore-exec.tar.gz
-          path: |
-            **/kore-exec.tar.gz
-   
+
   debian-bookworm:
     name: 'K Debian Bookworm Package'
     runs-on: [self-hosted, linux, normal]
@@ -220,7 +168,7 @@ jobs:
 
   macos-build:
     name: 'Build MacOS Package'
-    runs-on: macos-11
+    runs-on: macos-13
     timeout-minutes: 120
     environment: production
     needs: [set-release-id, source-tarball]
@@ -273,7 +221,7 @@ jobs:
           git commit Formula/$PACKAGE.rb -m "Update ${PACKAGE} to ${VERSION}: part 1"
           ../kframework/package/macos/brew-build-and-update-to-local-bottle ${PACKAGE} ${VERSION} ${ROOT_URL}
           git reset HEAD^
-          LOCAL_BOTTLE_NAME=$(basename $(find . -name "kframework--${VERSION}.big_sur.bottle*.tar.gz"))
+          LOCAL_BOTTLE_NAME=$(basename $(find . -name "kframework--${VERSION}.ventura.bottle*.tar.gz"))
           BOTTLE_NAME=$(echo ${LOCAL_BOTTLE_NAME#./} | sed 's!kframework--!kframework-!')
           ../kframework/package/macos/brew-update-to-final ${PACKAGE} ${VERSION} ${ROOT_URL}
           echo "path=${LOCAL_BOTTLE_NAME}" >> ${GITHUB_OUTPUT}
@@ -302,7 +250,7 @@ jobs:
 
   macos-test:
     name: 'Test MacOS Package'
-    runs-on: macos-11
+    runs-on: macos-13
     timeout-minutes: 60
     environment: production
     needs: [macos-build, set-release-id]
@@ -400,7 +348,7 @@ jobs:
     name: 'Publish Release'
     runs-on: [self-hosted, linux, normal]
     environment: production
-    needs: [nix-release, macos-build, macos-test, source-tarball, ubuntu-jammy, ubuntu-focal, debian-bookworm, set-release-id, arch]
+    needs: [nix-release, macos-build, macos-test, source-tarball, ubuntu-jammy, debian-bookworm, set-release-id, arch]
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
@@ -416,7 +364,7 @@ jobs:
           server-id: runtime.verification.snapshots
           server-username: MAVEN_USERNAME
           server-password: MAVEN_PASSWORD
-      
+
       # Build and Run Tests in Docker
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
@@ -477,7 +425,7 @@ jobs:
         run: |
           sudo apt update --yes
           sudo apt install --yes wget texlive-xetex
-          sudo wget -nv -O- https://download.calibre-ebook.com/linux-installer.sh | sh /dev/stdin version=5.42.0
+          sudo wget -nv -O- https://download.calibre-ebook.com/linux-installer.sh | sh /dev/stdin version=5.44.0
           sudo wget https://github.com/jgm/pandoc/releases/download/2.18/pandoc-2.18-1-amd64.deb -O /tmp/pandoc.deb
           sudo dpkg -i /tmp/pandoc.deb
       - name: 'Checkout code and set up web build'

deps/hs-backend-booster_release

@@ -1 +1 @@
-6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566
+5a283f7c85c5b4f66ff477b494c5d138c54706e6

deps/z3

@@ -0,0 +1 @@
+4.12.1

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.

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java

@@ -26,6 +26,7 @@ public List<Module> getKompileModules() {
         mods.add(new AbstractModule() {
             @Override
             protected void configure() {
+                binder().requireAtInjectOnConstructors();
                 bindOptions(HaskellBackendKModule.this::kompileOptions, binder());
                 installHaskellBackend(binder());
             }
@@ -54,6 +55,7 @@ public List<Module> getKRunModules() {
         return Collections.singletonList(new AbstractModule() {
             @Override
             protected void configure() {
+                binder().requireAtInjectOnConstructors();
                 installHaskellRewriter(binder());
             }
         });
@@ -74,6 +76,7 @@ public List<Module> getKProveModules() {
         return Collections.singletonList(new AbstractModule() {
             @Override
             protected void configure() {
+                binder().requireAtInjectOnConstructors();
                 installHaskellBackend(binder());
                 installHaskellRewriter(binder());
             }

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java

@@ -2,12 +2,15 @@
 package org.kframework.backend.haskell;
 
 import com.beust.jcommander.Parameter;
+import com.google.inject.Inject;
 import org.kframework.backend.kore.ModuleToKORE;
 import org.kframework.utils.inject.RequestScoped;
 import org.kframework.utils.options.BaseEnumConverter;
 
 @RequestScoped
 public class HaskellKRunOptions {
+    @Inject
+    public HaskellKRunOptions() {}
 
     @Parameter(names="--haskell-backend-command", descriptionKey = "command",
             description="Command to run the Haskell backend execution engine.", hidden = true)

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java

@@ -2,11 +2,14 @@
 package org.kframework.backend.haskell;
 
 import com.beust.jcommander.Parameter;
+import com.google.inject.Inject;
 import org.kframework.utils.inject.RequestScoped;
 
 @RequestScoped
 public class HaskellKompileOptions {
 
+    @Inject
+    public HaskellKompileOptions() {}
     @Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.", descriptionKey = "command", hidden = true)
     public String haskellBackendCommand = "kore-exec";