Merge branch 'merge-node' of https://github.com/runtimeverification/k …

…into merge-node

deps/haskell-backend_release

@@ -1 +1 @@
-v0.1.49
+v0.1.51

flake.nix

@@ -3,7 +3,7 @@
   inputs = {
     llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.64";
     haskell-backend = {
-      url = "github:runtimeverification/haskell-backend/v0.1.49";
+      url = "github:runtimeverification/haskell-backend/v0.1.51";
       inputs.rv-utils.follows = "llvm-backend/rv-utils";
       inputs.nixpkgs.follows = "llvm-backend/nixpkgs";
     };

k-distribution/src/main/scripts/bin/krun

@@ -37,7 +37,7 @@ filterSubst=
 
 if [[ "$OSTYPE" == "darwin"* ]]; then
   LLDB_FILE="$(dirname "$0")/../lib/kllvm/lldb/k_lldb_path"
-  if [ -f "$LLDB_FILE" ]; then
+  if [[ -f "$LLDB_FILE" && -f "$(cat "$LLDB_FILE")" ]]; then
     DBG_EXE="$(cat "$LLDB_FILE")"
   else
     DBG_EXE="lldb"

k-distribution/tests/regression-new/mint-llvm-2/Makefile

@@ -0,0 +1,7 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS=--syntax-module TEST
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/mint-llvm-2/test.k

@@ -0,0 +1,12 @@
+module TEST
+  imports BOOL
+  imports MINT
+
+  syntax MInt{64}
+  syntax MInt{32}
+
+  syntax MInt{32} ::= m32() [function]
+  syntax MInt{64} ::= m64() [function]
+  rule m64() => 0p64
+  rule m32() => 0p32
+endmodule

k-frontend/src/main/java/org/kframework/compile/AddSortInjections.java

@@ -488,7 +488,12 @@ private static Sort lub(
     }
 
     Set<Sort> nonParametric =
-        filteredEntries.stream().filter(s -> s.params().isEmpty()).collect(Collectors.toSet());
+        filteredEntries.stream()
+            .filter(
+                s ->
+                    s.params().isEmpty()
+                        || stream(s.params()).allMatch(p -> mod.allSorts().contains(p)))
+            .collect(Collectors.toSet());
     Set<Sort> bounds = mod.subsorts().upperBounds(nonParametric);
     // Anything less than KBott or greater than K is a syntactic sort from kast.md which should not
     // be considered

pyk/src/pyk/proof/proof.py

@@ -279,6 +279,10 @@ def lines(self) -> list[str]:
         subproofs_summaries = [subproof.summary for subproof in self.subproofs]
         return CompositeSummary([BaseSummary(self.id, self.status), *subproofs_summaries])
 
+    @property
+    def one_line_summary(self) -> str:
+        return self.status.name
+
     @abstractmethod
     def get_steps(self) -> Iterable[PS]:
         """Return all currently available steps associated with this Proof. Should not modify `self`."""
@@ -321,6 +325,7 @@ def parallel_advance_proof(
     max_iterations: int | None = None,
     fail_fast: bool = False,
     max_workers: int = 1,
+    callback: Callable[[P], None] = (lambda x: None),
 ) -> None:
     """Advance proof with multithreaded strategy.
 
@@ -342,6 +347,7 @@ def parallel_advance_proof(
         fail_fast: If the proof is failing after finishing a step,
           halt execution even if there are still available steps.
         max_workers: Maximum number of worker threads the pool can spawn.
+        callback: Callable to run in between each completed step, useful for getting real-time information about the proof.
     """
     pending: set[Future[Any]] = set()
     explored: set[PS] = set()
@@ -371,6 +377,7 @@ def submit_steps(_steps: Iterable[PS]) -> None:
                 for result in proof_results:
                     proof.commit(result)
                 proof.write_proof_data()
+                callback(proof)
                 iterations += 1
                 if max_iterations is not None and max_iterations <= iterations:
                     break
@@ -489,7 +496,13 @@ def init_proof(self, proof: P) -> None:
         """
         ...
 
-    def advance_proof(self, proof: P, max_iterations: int | None = None, fail_fast: bool = False) -> None:
+    def advance_proof(
+        self,
+        proof: P,
+        max_iterations: int | None = None,
+        fail_fast: bool = False,
+        callback: Callable[[P], None] = (lambda x: None),
+    ) -> None:
         """Advance a proof.
 
         Performs loop `Proof.get_steps()` -> `Prover.step_proof()` -> `Proof.commit()`.
@@ -499,6 +512,7 @@ def advance_proof(self, proof: P, max_iterations: int | None = None, fail_fast:
             max_iterations (optional): Maximum number of steps to take.
             fail_fast: If the proof is failing after finishing a step,
               halt execution even if there are still available steps.
+            callback: Callable to run in between each completed step, useful for getting real-time information about the proof.
         """
         iterations = 0
         _LOGGER.info(f'Initializing proof: {proof.id}')
@@ -520,5 +534,6 @@ def advance_proof(self, proof: P, max_iterations: int | None = None, fail_fast:
                 for result in results:
                     proof.commit(result)
                 proof.write_proof_data()
+                callback(proof)
         if proof.failed:
             proof.failure_info = self.failure_info(proof)

pyk/src/pyk/proof/reachability.py

@@ -503,6 +503,20 @@ def summary(self) -> CompositeSummary:
             ]
         )
 
+    @property
+    def one_line_summary(self) -> str:
+        nodes = len(self.kcfg.nodes)
+        pending = len(self.pending)
+        failing = len(self.failing)
+        branches = len(self.kcfg.ndbranches()) + len(self.kcfg.splits())
+        vacuous = len(self.kcfg.vacuous)
+        stuck = len(self.kcfg.stuck)
+        passed = len([cover for cover in self.kcfg.covers() if cover.target.id == self.target])
+        return (
+            super().one_line_summary
+            + f'/{nodes} nodes/{pending} pending/{passed} passed/{failing} failing/{branches} branches/{vacuous} vacuous/{stuck} stuck'
+        )
+
     def get_refutation_id(self, node_id: int) -> str:
         return f'{self.id}.node-infeasible-{node_id}'