From e5a4a237c9a63e7a0a35eaa97088506c60d63b8b Mon Sep 17 00:00:00 2001
From: Bruce Collie <brucecollie82@gmail.com>
Date: Mon, 23 Oct 2023 14:26:08 +0100
Subject: [PATCH] Fix for macOS nix / kup breakage (#3741)

On my Intel mac machine, the minimal JRE package is broken:
```console
$ /nix/store/6bqyc34isvgrrgl3nrqilzqbx7r1dyq5-zulu19.30.11-ca-jdk-minimal-jre-19.0.1/bin/java
[1]    31710 killed
```

This causes the default `kup`-installed K to break; the fix is just to
identify this platform and package the full JRE. The only downside here
is a slightly bigger closure for users on this platform, which is likely
to be deprecated at some point in the future anyway.

I have also added a new minimal "smoke test" to the Nix CI tests;
previously we were not checking that `kompile` etc. actually run on
Intel macOS.
---
 .github/workflows/test-pr.yml |  4 +++-
 flake.nix                     | 24 ++++++++++++++++++++----
 nix/k.nix                     | 11 ++++++-----
 3 files changed, 29 insertions(+), 10 deletions(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index aa4589e39c2..07dc74a5267 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -230,9 +230,11 @@ jobs:
       - name: 'Build K Framework'
         run: GC_DONT_GC=1 nix build --print-build-logs .
 
+      - name: 'Smoke test K'
+        run: GC_DONT_GC=1 nix build --print-build-logs .#smoke-test
+
       # These tests take a really long time to run on other platforms, so we
       # skip them unless we're on the M1 runner.
       - name: 'Test K'
         if: ${{ matrix.os == 'self-macos-12' }}
         run: GC_DONT_GC=1 nix build --print-build-logs .#test
-
diff --git a/flake.nix b/flake.nix
index ea4a8ed148b..661d2930d84 100644
--- a/flake.nix
+++ b/flake.nix
@@ -113,6 +113,7 @@
         };
 
       in rec {
+        k-version = pkgs.lib.removeSuffix "\n" (builtins.readFile ./package/version);
 
         packages = rec {
           k = pkgs.k-framework {
@@ -149,11 +150,26 @@
                 "llvm-backend/src/main/native/llvm-backend";
             };
 
+          smoke-test = with pkgs;
+            stdenv.mkDerivation {
+              name = "k-${k-version}-${self.rev or "dirty"}-smoke-test";
+              unpackPhase = "true";
+              buildInputs = [ fmt gmp mpfr k ];
+              buildPhase = ''
+                echo "module TEST imports BOOL endmodule" > test.k
+                kompile test.k --syntax-module TEST --backend llvm
+                rm -rf test-kompiled
+                kompile test.k --syntax-module TEST --backend haskell
+              '';
+              installPhase = ''
+                runHook preInstall
+                touch "$out"
+                runHook postInstall
+              '';
+            };
+
           test = with pkgs;
-            let
-              k-version =
-                lib.removeSuffix "\n" (builtins.readFile ./package/version);
-            in stdenv.mkDerivation {
+            stdenv.mkDerivation {
               name = "k-${k-version}-${self.rev or "dirty"}-test";
               src = lib.cleanSource
                 (nix-gitignore.gitignoreSourcePure [ ./.gitignore ]
diff --git a/nix/k.nix b/nix/k.nix
index 7d29456b8fa..7b9a08673b9 100644
--- a/nix/k.nix
+++ b/nix/k.nix
@@ -1,5 +1,5 @@
 { src, clang, stdenv, lib, mavenix, runCommand, makeWrapper, bison, flex, gcc
-, git, gmp, jdk, jre_minimal, mpfr, ncurses, pkgconfig, python3, z3
+, git, gmp, jdk, jre, jre_minimal, mpfr, ncurses, pkgconfig, python3, z3
 , haskell-backend, booster ? null, prelude-kore, llvm-backend, debugger, version
 , llvm-kompile-libs }:
 
@@ -77,10 +77,11 @@ in let
     flex
     (if stdenv.isDarwin then clang else gcc)
     gmp
-    (jre_minimal.override {
-      modules = [ "java.base" "java.desktop" "java.logging" "java.rmi" ];
-      jdk = if stdenv.isDarwin then jdk else jdk.override { headless = true; };
-    })
+    (if stdenv.isDarwin && stdenv.isx86_64 then jre else
+      (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