Merge branch 'develop' into _update-deps/runtimeverification/llvm-bac…

…kend

README.md

@@ -109,7 +109,7 @@ The following dependencies are needed either at build time or runtime:
 *   [fmt](https://fmt.dev/)
 *   [gcc](https://gcc.gnu.org/)
 *   [gmp](https://gmplib.org/)
-*   [jdk](https://openjdk.java.net/) (version 11 or greater)
+*   [jdk](https://openjdk.java.net/) (version 17 or greater)
 *   [libjemalloc](https://github.com/jemalloc/jemalloc)
 *   [libyaml](https://pyyaml.org/wiki/LibYAML)
 *   [llvm](https://llvm.org/) (We require version 10 or greater for clang, lld, and llvm-tools. On some distributions, the utilities below are also needed and packaged separately.)
@@ -135,10 +135,10 @@ See the notes below.
 
 ### Installation Notes
 
-1.  Java Development Kit (required JDK11 or higher)
+1.  Java Development Kit (required JDK 17 or higher)
 
     *   Linux: Download from package manager
-        (e.g. `sudo apt-get install openjdk-11-jdk`).
+        (e.g. `sudo apt-get install openjdk-17-jdk`).
 
     *   macOS/brew: Download from package manager
         (e.g. `brew install java`).
@@ -419,10 +419,6 @@ Common build-time error messages:
       build path of your IDE. Generally this is solved by regenerating your project /
       re-syncing it with the pom.xml.
 
--   `[ERROR] Failed to execute goal org.apache.maven.plugins:maven-compiler-plugin:3.1:compile
-     (default-compile) on project k-core: Fatal error compiling: invalid target release: 11 -> [Help 1]`
-    + You either do not have Java 11 installed, or `$JAVA_HOME` does not point to a Java 11 JDK.
-
 -   `[ERROR] Failed to execute goal org.apache.maven.plugins:maven-antrun-plugin:1.7:run
      (build-haskell) on project haskell-backend: An Ant BuildException has occured: exec returned: 1`
 

flake.nix

@@ -64,6 +64,7 @@
             k-framework = { haskell-backend-bins, llvm-kompile-libs }:
               prev.callPackage ./nix/k.nix {
                 inherit (prev) llvm-backend;
+                clang = prev."clang_${toString final.llvm-version}";
                 booster = booster-backend.packages.${prev.system}.kore-rpc-booster;
                 mavenix = { inherit (prev) buildMaven; };
                 haskell-backend = haskell-backend-bins;

nix/k.nix

@@ -1,6 +1,7 @@
 { src, clang, stdenv, lib, mavenix, runCommand, makeWrapper, bison, flex, gcc
-, git, gmp, jdk, mpfr, ncurses, pkgconfig, python3, z3, haskell-backend, booster ? null
-, prelude-kore, llvm-backend, llvm-backend-matching, debugger, version, llvm-kompile-libs }:
+, git, gmp, jdk, jre_minimal, mpfr, ncurses, pkgconfig, python3, z3
+, haskell-backend, booster ? null, prelude-kore, llvm-backend, debugger, version
+, llvm-kompile-libs }:
 
 let
   unwrapped = mavenix.buildMaven {
@@ -46,13 +47,14 @@ let
         fi
       done
 
-      mkdir -p $out/lib/cmake/kframework && ln -sf ${llvm-backend.src}/cmake/* $out/lib/cmake/kframework/
+      mkdir -p $out/lib/cmake/kframework && cp ${llvm-backend.src}/cmake/* $out/lib/cmake/kframework/
       ln -sf ${llvm-backend}/include/kllvm $out/include/
       ln -sf ${llvm-backend}/include/kllvm-c $out/include/
       ln -sf ${llvm-backend}/lib/kllvm $out/lib/
       ln -sf ${llvm-backend}/lib/scripts $out/lib/
       ln -sf ${llvm-backend}/bin/* $out/bin/
-      ${lib.optionalString (booster != null ) "ln -sf ${booster}/bin/* $out/bin/"}
+      ${lib.optionalString (booster != null)
+      "ln -sf ${booster}/bin/* $out/bin/"}
 
       prelude_kore="$out/include/kframework/kore/prelude.kore"
       mkdir -p "$(dirname "$prelude_kore")"
@@ -75,7 +77,10 @@ in let
     flex
     (if stdenv.isDarwin then clang else gcc)
     gmp
-    jdk
+    (jre_minimal.override {
+      modules = [ "java.base" "java.desktop" "java.logging" "java.rmi" ];
+      jdk = if stdenv.isDarwin then jdk else jdk.override { headless = true; };
+    })
     mpfr
     ncurses
     pkgconfig
@@ -123,6 +128,5 @@ in let
       ln -sf ${haskell-backend}/bin/kore-parser $out/bin/kore-parser
       ln -sf ${haskell-backend}/bin/kore-repl $out/bin/kore-repl
       ln -sf ${haskell-backend}/bin/kore-match-disjunction $out/bin/kore-match-disjunction
-      ln -sf ${llvm-backend-matching}/bin/llvm-backend-matching $out/bin/llvm-backend-matching
     '';
 in final [ ]

package/debian/control.bookworm

@@ -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 , libsecp256k1-1 , libyaml-0-2 , libz3-4 , lld-14 , pkg-config , llvm-14
+Depends: bison , clang-14 , openjdk-17-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

package/debian/control.jammy

@@ -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 , libsecp256k1-0 , libtinfo-dev , libyaml-0-2 , libz3-4 , lld-14 , llvm-14 , pkg-config
+Depends: bison , clang-14 , openjdk-17-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

pom.xml

@@ -145,8 +145,8 @@
           <artifactId>maven-compiler-plugin</artifactId>
           <version>3.7.0</version>
           <configuration>
-            <source>11</source>
-            <target>11</target>
+            <source>17</source>
+            <target>17</target>
           </configuration>
         </plugin>
         <!-- Antrun plugin for running arbitrary shell commands (building subprojects) -->