Merge remote-tracking branch 'origin/develop' into _update-deps/runti…

…meverification/haskell-backend

pyk/src/pyk/kore/rpc.py

@@ -570,8 +570,6 @@ class LogEntry(ABC):
     @classmethod
     def from_dict(cls: type[LE], dct: Mapping[str, Any]) -> LE:
         match dct['tag']:
-            case 'processing-time':
-                return LogTiming.from_dict(dct)  # type: ignore
             case 'rewrite':
                 return LogRewrite.from_dict(dct)  # type: ignore
             case _:
@@ -581,27 +579,6 @@ def from_dict(cls: type[LE], dct: Mapping[str, Any]) -> LE:
     def to_dict(self) -> dict[str, Any]: ...
 
 
-@final
-@dataclass(frozen=True)
-class LogTiming(LogEntry):
-    class Component(Enum):
-        KORE_RPC = 'kore-rpc'
-        BOOSTER = 'booster'
-        PROXY = 'proxy'
-
-    time: float
-    component: Component | None
-
-    @classmethod
-    def from_dict(cls, dct: Mapping[str, Any]) -> LogTiming:
-        return LogTiming(
-            time=dct['time'], component=LogTiming.Component(dct['component']) if 'component' in dct else None
-        )
-
-    def to_dict(self) -> dict[str, Any]:
-        return {'tag': 'processing-time', 'time': self.time, 'component': self.component}
-
-
 @final
 @dataclass(frozen=True)
 class LogRewrite(LogEntry):
@@ -1025,7 +1002,6 @@ def execute(
         module_name: str | None = None,
         log_successful_rewrites: bool | None = None,
         log_failed_rewrites: bool | None = None,
-        log_timing: bool | None = None,
     ) -> ExecuteResult:
         params = filter_none(
             {
@@ -1039,7 +1015,6 @@ def execute(
                 'state': self._state(pattern),
                 'log-successful-rewrites': log_successful_rewrites,
                 'log-failed-rewrites': log_failed_rewrites,
-                'log-timing': log_timing,
             }
         )
 
@@ -1052,14 +1027,12 @@ def implies(
         consequent: Pattern,
         *,
         module_name: str | None = None,
-        log_timing: bool | None = None,
     ) -> ImpliesResult:
         params = filter_none(
             {
                 'antecedent': self._state(antecedent),
                 'consequent': self._state(consequent),
                 'module': module_name,
-                'log-timing': log_timing,
             }
         )
 
@@ -1071,13 +1044,11 @@ def simplify(
         pattern: Pattern,
         *,
         module_name: str | None = None,
-        log_timing: bool | None = None,
     ) -> tuple[Pattern, tuple[LogEntry, ...]]:
         params = filter_none(
             {
                 'state': self._state(pattern),
                 'module': module_name,
-                'log-timing': log_timing,
             }
         )
 

pyk/src/tests/integration/kore/test_kore_client.py

@@ -40,7 +40,6 @@
     InvalidModuleError,
     LogOrigin,
     LogRewrite,
-    LogTiming,
     RewriteFailure,
     RewriteSuccess,
     SatResult,
@@ -625,48 +624,6 @@ def test(
         assert actual == expected[server_type]
 
 
-class TestTimeLogging(KoreClientTest):
-    KOMPILE_DEFINITION = """
-        module TIMING-TEST
-            imports INT
-            configuration <k> $PGM:Int </k>
-        endmodule
-    """
-    KOMPILE_MAIN_MODULE = 'TIMING-TEST'
-    KOMPILE_ARGS = {'syntax_module': 'TIMING-TEST'}
-    LLVM_ARGS = KOMPILE_ARGS
-
-    @staticmethod
-    def config(i: int) -> Pattern:
-        return generated_top((k(kseq((inj(INT, SORT_K_ITEM, int_dv(i)),))), generated_counter(int_dv(0))))
-
-    def test_execute(self, kore_client: KoreClient) -> None:
-        # When
-        response = kore_client.execute(self.config(0), log_timing=True)
-        logs = response.logs
-
-        # Then
-        assert logs
-        assert all(isinstance(log, LogTiming) for log in logs)
-
-    def test_implies(self, kore_client: KoreClient) -> None:
-        # When
-        response = kore_client.implies(EVar('X', INT), int_top, log_timing=True)
-        logs = response.logs
-
-        # Then
-        assert logs
-        assert all(isinstance(log, LogTiming) for log in logs)
-
-    def test_simplify(self, kore_client: KoreClient) -> None:
-        # When
-        _, logs = kore_client.simplify(int_top, log_timing=True)
-
-        # Then
-        assert logs
-        assert all(isinstance(log, LogTiming) for log in logs)
-
-
 class TestAddModule(KoreClientTest):
     KOMPILE_DEFINITION = """
         module INT-CONFIG