From c05b9acfc9b70565de00fc243e76fc5031b0ae64 Mon Sep 17 00:00:00 2001 From: Sam Balco Date: Fri, 20 Oct 2023 11:07:36 +0100 Subject: [PATCH 1/6] Replaced jdk with jre as a runtime dependency and removed llvm-backend-matching as it has been replaced by llvm-kompile-matching --- nix/k.nix | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/nix/k.nix b/nix/k.nix index e96bc7e0dc7..9ea9c360a55 100644 --- a/nix/k.nix +++ b/nix/k.nix @@ -1,6 +1,6 @@ { 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, jre_minimal, mpfr, ncurses, pkgconfig, python3, z3, haskell-backend, booster ? null +, prelude-kore, llvm-backend, debugger, version, llvm-kompile-libs }: let unwrapped = mavenix.buildMaven { @@ -75,7 +75,7 @@ in let flex (if stdenv.isDarwin then clang else gcc) gmp - jdk + jre_minimal mpfr ncurses pkgconfig @@ -123,6 +123,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 [ ] From 9d8ca8ef9a0e6bc9c184408f20a9efff6ad92037 Mon Sep 17 00:00:00 2001 From: Sam Balco Date: Fri, 20 Oct 2023 11:28:15 +0100 Subject: [PATCH 2/6] minimised size of jre on linux --- nix/k.nix | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/nix/k.nix b/nix/k.nix index 9ea9c360a55..5d6625618fa 100644 --- a/nix/k.nix +++ b/nix/k.nix @@ -1,6 +1,7 @@ { src, clang, stdenv, lib, mavenix, runCommand, makeWrapper, bison, flex, gcc -, git, gmp, jre_minimal, mpfr, ncurses, pkgconfig, python3, z3, haskell-backend, booster ? null -, prelude-kore, llvm-backend, 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 { @@ -52,7 +53,8 @@ let 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,7 @@ in let flex (if stdenv.isDarwin then clang else gcc) gmp - jre_minimal + (jre_minimal.override { jdk = jdk.override { headless = true; }; }) mpfr ncurses pkgconfig From 681d06c461bacd3bccfd4f0df14b983b70a56693 Mon Sep 17 00:00:00 2001 From: Sam Balco Date: Fri, 20 Oct 2023 11:30:49 +0100 Subject: [PATCH 3/6] fix jre on mac --- nix/k.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/nix/k.nix b/nix/k.nix index 5d6625618fa..baa955a1fcf 100644 --- a/nix/k.nix +++ b/nix/k.nix @@ -77,7 +77,7 @@ in let flex (if stdenv.isDarwin then clang else gcc) gmp - (jre_minimal.override { jdk = jdk.override { headless = true; }; }) + (if stdenv.isDarwin then jre_minimal else jre_minimal.override { jdk = jdk.override { headless = true; }; }) mpfr ncurses pkgconfig From e648db87deda42939c126ade67acae51c5bb3179 Mon Sep 17 00:00:00 2001 From: Sam Balco Date: Fri, 20 Oct 2023 13:19:07 +0100 Subject: [PATCH 4/6] add missing modules to jre --- nix/k.nix | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/nix/k.nix b/nix/k.nix index baa955a1fcf..360c31f8d7a 100644 --- a/nix/k.nix +++ b/nix/k.nix @@ -77,7 +77,10 @@ in let flex (if stdenv.isDarwin then clang else gcc) gmp - (if stdenv.isDarwin then jre_minimal else jre_minimal.override { jdk = jdk.override { headless = true; }; }) + (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 From cded82de192f16d5a55070f10c3b840d3775be22 Mon Sep 17 00:00:00 2001 From: Sam Balco Date: Fri, 20 Oct 2023 13:52:21 +0100 Subject: [PATCH 5/6] select same version of clang as runtime dependency as the one used by llvm-backend --- flake.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/flake.nix b/flake.nix index e5690b2fce5..ea4a8ed148b 100644 --- a/flake.nix +++ b/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; From ee93a2123619bf8cdfb5911c74cfe30f65cdf141 Mon Sep 17 00:00:00 2001 From: Sam Balco Date: Fri, 20 Oct 2023 14:11:46 +0100 Subject: [PATCH 6/6] copy cmake folder to avoid depending on the whole llvm-backend repo at runtime --- nix/k.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/nix/k.nix b/nix/k.nix index 360c31f8d7a..7d29456b8fa 100644 --- a/nix/k.nix +++ b/nix/k.nix @@ -47,7 +47,7 @@ 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/