From e91a00021c932b002c47a693dbff1c00cfca32b4 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Tue, 9 Apr 2024 03:07:37 -0600 Subject: [PATCH] Update dependency: deps/k_release (https://github.com/runtimeverification/pyk/pull/1070) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Related: * runtimeverification/k#4146 * runtimeverification/haskell-backend#3761 --------- Co-authored-by: devops Co-authored-by: Tamás Tóth --- pyk/deps/k_release | 2 +- pyk/docs/conf.py | 4 ++-- pyk/package/version | 2 +- pyk/pyproject.toml | 2 +- pyk/src/pyk/__init__.py | 2 +- pyk/src/pyk/konvert/_module_to_kore.py | 20 +++++++++++-------- .../tests/integration/proof/test_mini_kevm.py | 2 ++ 7 files changed, 20 insertions(+), 14 deletions(-) diff --git a/pyk/deps/k_release b/pyk/deps/k_release index 0ea0dfb4249..a545989c7e5 100644 --- a/pyk/deps/k_release +++ b/pyk/deps/k_release @@ -1 +1 @@ -6.3.75 +6.3.77 diff --git a/pyk/docs/conf.py b/pyk/docs/conf.py index 26cf730b314..53c007fdd50 100644 --- a/pyk/docs/conf.py +++ b/pyk/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/pyk/package/version b/pyk/package/version index da9223fb727..3f36f20c5e9 100644 --- a/pyk/package/version +++ b/pyk/package/version @@ -1 +1 @@ -0.1.777 +0.1.778 diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml index a128f511ad7..ccf8943e3af 100644 --- a/pyk/pyproject.toml +++ b/pyk/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. ", diff --git a/pyk/src/pyk/__init__.py b/pyk/src/pyk/__init__.py index 1e56c2a9dc6..62113f5bdd0 100644 --- a/pyk/src/pyk/__init__.py +++ b/pyk/src/pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -K_VERSION: Final = '6.3.75' +K_VERSION: Final = '6.3.77' diff --git a/pyk/src/pyk/konvert/_module_to_kore.py b/pyk/src/pyk/konvert/_module_to_kore.py index a6f9aec2b40..e038e62afeb 100644 --- a/pyk/src/pyk/konvert/_module_to_kore.py +++ b/pyk/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.""" diff --git a/pyk/src/tests/integration/proof/test_mini_kevm.py b/pyk/src/tests/integration/proof/test_mini_kevm.py index c15723bd1dc..136354bfcdc 100644 --- a/pyk/src/tests/integration/proof/test_mini_kevm.py +++ b/pyk/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',