From e8f99969ea8a27b082cfbb79e5824d5f07206a2a Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 8 Apr 2024 14:00:03 +0000 Subject: [PATCH 1/5] deps/k_release: Set Version 6.3.77 --- deps/k_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/k_release b/deps/k_release index 0ea0dfb42..a545989c7 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -6.3.75 +6.3.77 From fc0acbfe85b6184d72628718ebc556caa71cc97e Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 8 Apr 2024 14:00:20 +0000 Subject: [PATCH 2/5] Set K Version: 6.3.77 --- src/pyk/__init__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pyk/__init__.py b/src/pyk/__init__.py index 1e56c2a9d..62113f5bd 100644 --- a/src/pyk/__init__.py +++ b/src/pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -K_VERSION: Final = '6.3.75' +K_VERSION: Final = '6.3.77' From 2ab68cbcb7414ff5240c0503a657a914d5c32a1c Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 8 Apr 2024 14:00:48 +0000 Subject: [PATCH 3/5] Set Version: 0.1.778 --- docs/conf.py | 4 ++-- package/version | 2 +- pyproject.toml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/conf.py b/docs/conf.py index 26cf730b3..53c007fdd 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.777' -release = '0.1.777' +version = '0.1.778' +release = '0.1.778' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index da9223fb7..3f36f20c5 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.777 +0.1.778 diff --git a/pyproject.toml b/pyproject.toml index a128f511a..ccf8943e3 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.777" +version = "0.1.778" description = "" authors = [ "Runtime Verification, Inc. ", From 5f95880ae523590b1af9ee0bc2c674ba1526f97a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 8 Apr 2024 15:12:41 +0000 Subject: [PATCH 4/5] Do not generate syntax attributes --- src/pyk/konvert/_module_to_kore.py | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/src/pyk/konvert/_module_to_kore.py b/src/pyk/konvert/_module_to_kore.py index a6f9aec2b..e038e62af 100644 --- a/src/pyk/konvert/_module_to_kore.py +++ b/src/pyk/konvert/_module_to_kore.py @@ -722,20 +722,27 @@ def simplified_module(definition: KDefinition, module_name: str | None = None) - PullUpRewrites(), DiscardSymbolAtts( [ + Atts.ASSOC, Atts.CELL, Atts.CELL_FRAGMENT, Atts.CELL_NAME, Atts.CELL_OPT_ABSENT, + Atts.COLOR, + Atts.COLORS, + Atts.COMM, + Atts.FORMAT, Atts.GROUP, Atts.IMPURE, Atts.INDEX, Atts.INITIALIZER, + Atts.LEFT, Atts.MAINCELL, Atts.PREDICATE, Atts.PREFER, Atts.PRIVATE, Atts.PRODUCTION, Atts.PROJECTION, + Atts.RIGHT, Atts.SEQSTRICT, Atts.STRICT, Atts.USER_LIST, @@ -747,14 +754,6 @@ def simplified_module(definition: KDefinition, module_name: str | None = None) - AddSymbolAtts(Atts.FUNCTIONAL(None), _is_functional), AddSymbolAtts(Atts.INJECTIVE(None), _is_injective), AddSymbolAtts(Atts.CONSTRUCTOR(None), _is_constructor), - AddDefaultFormatAtts(), - DiscardFormatAtts(), - InlineFormatTerminals(), - AddColorAtts(), - DiscardSymbolAtts([Atts.COLOR]), - AddTerminalAtts(), - AddPrioritiesAtts(), - AddAssocAtts(), ) definition = reduce(lambda defn, step: step.execute(defn), pipeline, definition) module = definition.modules[0] @@ -1118,6 +1117,11 @@ def _update(self, production: KProduction) -> KProduction: return production.let(att=production.att.discard(self.keys)) +# ----------------- +# Syntax attributes +# ----------------- + + @dataclass class AddDefaultFormatAtts(SingleModulePass): """Add a default format attribute value to each symbol profuction missing one.""" From 0b8d62a0602c7cbcd2ffe0d6b066a21e681625c3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Tue, 9 Apr 2024 08:26:20 +0000 Subject: [PATCH 5/5] Disable `TestMiniKEVM` on the legacy backend --- src/tests/integration/proof/test_mini_kevm.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/tests/integration/proof/test_mini_kevm.py b/src/tests/integration/proof/test_mini_kevm.py index c15723bd1..136354bfc 100644 --- a/src/tests/integration/proof/test_mini_kevm.py +++ b/src/tests/integration/proof/test_mini_kevm.py @@ -50,6 +50,8 @@ def leaf_number(proof: APRProof) -> int: class TestMiniKEVM(KCFGExploreTest, KProveTest): KOMPILE_MAIN_FILE = K_FILES / 'mini-kevm.k' + # Disabled until resolved: https://github.com/runtimeverification/haskell-backend/issues/3761 + DISABLE_LEGACY = True @pytest.mark.parametrize( 'test_id,spec_file,spec_module,claim_id,max_iterations,max_depth,cut_rules,proof_status,expected_leaf_number',