Merge branch 'develop' into calibre

runtimeverification · Oct 23, 2023 · 7a77668 · 7a77668
2 parents 60dbf38 + e5a4a23
commit 7a77668
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 10 deletions.
diff --git 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
@@ -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
@@ -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