diff --git a/deps/k_release b/deps/k_release index b98d1d3fa..a3aaad93a 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -6.3.5 +6.3.18 diff --git a/deps/pyk_release b/deps/pyk_release index 105f5e4d4..634c104e5 100644 --- a/deps/pyk_release +++ b/deps/pyk_release @@ -1 +1 @@ -v0.1.662 +v0.1.665 diff --git a/flake.lock b/flake.lock index 3d9b22632..762f9b084 100644 --- a/flake.lock +++ b/flake.lock @@ -18,17 +18,17 @@ ] }, "locked": { - "lastModified": 1708422161, - "narHash": "sha256-0iGpmXEdDE0lK66slTyYlbylE4eVOM6nIEM9ffhWYsw=", + "lastModified": 1709082085, + "narHash": "sha256-eRMMmqw0EB2qKXKTVmRycD1X4kTMFrjZH1/EqunEGkg=", "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "54a1eb9c4278460b69b19d72280db54108f2d467", + "rev": "a3d89c2f3af1ccbe56ca88d25bcf6c697c333c21", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "54a1eb9c4278460b69b19d72280db54108f2d467", + "rev": "a3d89c2f3af1ccbe56ca88d25bcf6c697c333c21", "type": "github" } }, @@ -103,22 +103,29 @@ }, "haskell-backend": { "inputs": { - "nixpkgs": "nixpkgs", + "nixpkgs": [ + "k-framework", + "haskell-backend", + "rv-utils", + "nixpkgs" + ], + "nixpkgs2305": "nixpkgs2305", + "rv-utils": "rv-utils", "stacklock2nix": "stacklock2nix", "z3": "z3" }, "locked": { - "lastModified": 1708380172, - "narHash": "sha256-rIKNZKY+a2XX2MnUlMGeKT7kcsiX4BgoQoAQHqXk85w=", + "lastModified": 1709046454, + "narHash": "sha256-ZCuQ7Mi99OkUocDJ+FKZQI5NZQjyEKPks7lg7b/rTKc=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "ac6908d0ca26f194802c72f66f200e7079139f1b", + "rev": "62a3e13dc5c681a536271b834b11098aae9bce35", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "ac6908d0ca26f194802c72f66f200e7079139f1b", + "rev": "62a3e13dc5c681a536271b834b11098aae9bce35", "type": "github" } }, @@ -150,19 +157,19 @@ "llvm-backend", "nixpkgs" ], - "rv-utils": "rv-utils_2" + "rv-utils": "rv-utils_3" }, "locked": { - "lastModified": 1708691408, - "narHash": "sha256-LsY4LjQZD0IpTSHmCcPJvHQdULR6mteQCgkcqPXzMPk=", + "lastModified": 1709129006, + "narHash": "sha256-i1xBiYpqbGA4ARjHkaZzUQkhgqvM1n92VRDIG6Ib4Rs=", "owner": "runtimeverification", "repo": "k", - "rev": "457642e3f660265157573771cb5ee46d7662642b", + "rev": "0179b261340c73decda52ce8971942ea6a69b4da", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v6.3.5", + "ref": "v6.3.18", "repo": "k", "type": "github" } @@ -181,18 +188,18 @@ ], "pybind11-src": "pybind11-src", "rapidjson-src": "rapidjson-src", - "rv-utils": "rv-utils", + "rv-utils": "rv-utils_2", "utils": [ "k-framework", "flake-utils" ] }, "locked": { - "lastModified": 1708687355, - "narHash": "sha256-+hxlSYI5NGNg1yS7wzdqnPRWwt+K4Gl5rDEwA7Rn9Ss=", + "lastModified": 1709121853, + "narHash": "sha256-t66d/iMvidCe8Spd31mV9xl6TtDC+HEcdaNlAQ31Qck=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "411cfc5ffc51a48422a021cb1a70d9353be2ffc5", + "rev": "7b744a2fb5e0f752b6c8c5afbfe79904c3c637cf", "type": "github" }, "original": { @@ -243,6 +250,22 @@ } }, "nixpkgs": { + "locked": { + "lastModified": 1707163378, + "narHash": "sha256-oz+BzUDwtyircjjxv9aPYOS5gobxLCjD2il+gb/bCRo=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "e2ffefe304d941bb98989847944f3b58e0adcdd5", + "type": "github" + }, + "original": { + "owner": "nixos", + "repo": "nixpkgs", + "rev": "e2ffefe304d941bb98989847944f3b58e0adcdd5", + "type": "github" + } + }, + "nixpkgs2305": { "locked": { "lastModified": 1704290814, "narHash": "sha256-LWvKHp7kGxk/GEtlrGYV68qIvPHkU9iToomNFGagixU=", @@ -372,16 +395,16 @@ "poetry2nix": "poetry2nix" }, "locked": { - "lastModified": 1709130862, - "narHash": "sha256-VHOT9mXuAYE/9rjEkyjp9TYhp7JjUCx/rRm4L0/Ahrg=", + "lastModified": 1709143656, + "narHash": "sha256-QFiS5GLwJGdzCJ5RG66rwl0njFyyKOgEu5ssm+w2rvw=", "owner": "runtimeverification", "repo": "pyk", - "rev": "975f9d0e8d5ebe28fbda58b56325ef5aee9a075b", + "rev": "d6d707de8ac114940e15e31db75627ede9bc3adf", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.662", + "ref": "v0.1.665", "repo": "pyk", "type": "github" } @@ -431,7 +454,7 @@ }, "rv-utils": { "inputs": { - "nixpkgs": "nixpkgs_3" + "nixpkgs": "nixpkgs" }, "locked": { "lastModified": 1707492220, @@ -448,6 +471,24 @@ } }, "rv-utils_2": { + "inputs": { + "nixpkgs": "nixpkgs_3" + }, + "locked": { + "lastModified": 1707492220, + "narHash": "sha256-KRndaUPzUumDlNcKF7KzA8F/EZKLYCvurh7Z13sw2PI=", + "owner": "runtimeverification", + "repo": "rv-nix-tools", + "rev": "abf86805a623948c941e603e2fc4c26a06ea6eb6", + "type": "github" + }, + "original": { + "owner": "runtimeverification", + "repo": "rv-nix-tools", + "type": "github" + } + }, + "rv-utils_3": { "inputs": { "nixpkgs": "nixpkgs_4" }, @@ -467,11 +508,11 @@ }, "stacklock2nix": { "locked": { - "lastModified": 1700633677, - "narHash": "sha256-ATrA3tZZYo9aj9IAZZNqyvtkz4Ub1Q3q5OgADwxImTA=", + "lastModified": 1705051190, + "narHash": "sha256-xgH0gaD3dNtOzZzX3A40hZTiHJP5cIGmifbmfcS2OGI=", "owner": "cdepillabout", "repo": "stacklock2nix", - "rev": "84694f48ddd8e49b96a02216ca2ab406fba25e65", + "rev": "22676dfc45fa1c33899ba1da1a23665172a18ba7", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 46a498d63..290f3e2d7 100644 --- a/flake.nix +++ b/flake.nix @@ -2,11 +2,11 @@ description = " A flake for KMIR Semantics"; inputs = { - k-framework.url = "github:runtimeverification/k/v6.3.5"; + k-framework.url = "github:runtimeverification/k/v6.3.18"; nixpkgs.follows = "k-framework/nixpkgs"; flake-utils.follows = "k-framework/flake-utils"; rv-utils.follows = "k-framework/rv-utils"; - pyk.url = "github:runtimeverification/pyk/v0.1.662"; + pyk.url = "github:runtimeverification/pyk/v0.1.665"; nixpkgs-pyk.follows = "pyk/nixpkgs"; poetry2nix.follows = "pyk/poetry2nix"; }; diff --git a/kmir/poetry.lock b/kmir/poetry.lock index 1c0fc4ba4..dc1a1db01 100644 --- a/kmir/poetry.lock +++ b/kmir/poetry.lock @@ -649,7 +649,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "0.1.662" +version = "0.1.665" description = "" category = "main" optional = false @@ -671,8 +671,8 @@ xdg-base-dirs = "^6.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.662" -resolved_reference = "975f9d0e8d5ebe28fbda58b56325ef5aee9a075b" +reference = "v0.1.665" +resolved_reference = "d6d707de8ac114940e15e31db75627ede9bc3adf" [[package]] name = "pyperclip" @@ -776,14 +776,14 @@ testing = ["filelock"] [[package]] name = "rich" -version = "13.7.0" +version = "13.7.1" description = "Render rich text, tables, progress bars, syntax highlighting, markdown and more to the terminal" category = "main" optional = false python-versions = ">=3.7.0" files = [ - {file = "rich-13.7.0-py3-none-any.whl", hash = "sha256:6da14c108c4866ee9520bbffa71f6fe3962e193b7da68720583850cd4548e235"}, - {file = "rich-13.7.0.tar.gz", hash = "sha256:5cb5123b5cf9ee70584244246816e9114227e0b98ad9176eede6ad54bf5403fa"}, + {file = "rich-13.7.1-py3-none-any.whl", hash = "sha256:4edbae314f59eb482f54e9e30bf00d33350aaa94f4bfcd4e9e3110e64d0d7222"}, + {file = "rich-13.7.1.tar.gz", hash = "sha256:9be308cb1fe2f1f57d67ce99e95af38a1e2bc71ad9813b0e247cf7ffbcc3a432"}, ] [package.dependencies] @@ -913,4 +913,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "dcf4f0674c222aa567772410ad66bec0b0f27f04fb8dd7f57cc8163e45456496" +content-hash = "506c9846dc5c195e0b1a6282221ea583f5ac9335a3bbd971ea06d05da4ec822a" diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 51893ff62..48bb01705 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmir" -version = "0.2.31" +version = "0.2.32" description = "" authors = [ "Runtime Verification, Inc. ", @@ -13,7 +13,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" filelock = "3.9.0" -pyk = { git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.662" } +pyk = { git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.665" } pytest-timeout = "2.1.0" [tool.poetry.group.dev.dependencies] diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index d253c566d..5b85f15c0 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -5,4 +5,4 @@ from .prove import prove, show_proof, view_proof from .run import run -VERSION: Final = '0.2.31' +VERSION: Final = '0.2.32' diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index ff774c8b8..850836305 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -104,7 +104,7 @@ def rpc_session(self, server: KoreServer, claim_id: str, trace_rewrites: bool = cterm_symbolic = CTermSymbolic( client, self.mir_prove.definition, self.mir_prove.kompiled_kore, trace_rewrites=trace_rewrites ) - yield KCFGExplore(self.mir_prove, cterm_symbolic, kcfg_semantics=KMIRSemantics(), id=claim_id) + yield KCFGExplore(cterm_symbolic, kcfg_semantics=KMIRSemantics(), id=claim_id) # A wrapper on KProve's get_claims def get_all_claims(self, spec_file: Path, claim_label: Optional[str]) -> list[KClaim]: diff --git a/package/version b/package/version index e652b57d7..a8498651b 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.2.31 +0.2.32