From 5df9ce41f3441178bc7674085586d40ae41cc52e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Wed, 18 Sep 2024 20:44:33 +0200 Subject: [PATCH 1/2] No trimming of split constraints when printed (#4644) This PR disables the trimming of split constraints when showing a KCFG. The reason for this is as follows: - the constraints guide the debugging of Kontrol proofs in many cases, and it is likely that they will serve a similar purpose for other semantics; - if `--no-minimize` is turned on, which disables the trimming, the KCFG will also contain all of the substitutions printed explicitly, which are very large and hinder navigation through the KCFG considerably. --- pyk/src/pyk/kcfg/show.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/kcfg/show.py b/pyk/src/pyk/kcfg/show.py index 17cf07b6d2..47680f61d6 100644 --- a/pyk/src/pyk/kcfg/show.py +++ b/pyk/src/pyk/kcfg/show.py @@ -149,7 +149,7 @@ def _print_csubst( _constraint_strs = [ self.kprint.pretty_print(ml_pred_to_bool(constraint, unsafe=True)) for constraint in csubst.constraints ] - constraint_strs = _multi_line_print('constraint', _constraint_strs, 'true', max_width=max_width) + constraint_strs = _multi_line_print('constraint', _constraint_strs, 'true') if len(csubst.subst.minimize()) > 0 and minimize: subst_strs = ['subst: ...'] else: From e08769b3f230a3eb15d3bbd8230a9d9c66af4c78 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 19 Sep 2024 11:02:22 -0600 Subject: [PATCH 2/2] Update dependency: deps/llvm-backend_release (#4639) Co-authored-by: devops Co-authored-by: Roberto Rosmaninho --- deps/llvm-backend_release | 2 +- flake.lock | 8 ++++---- flake.nix | 2 +- llvm-backend/src/main/native/llvm-backend | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index 6667b8e5fa..8c2abf179c 100644 --- a/deps/llvm-backend_release +++ b/deps/llvm-backend_release @@ -1 +1 @@ -0.1.88 +0.1.92 diff --git a/flake.lock b/flake.lock index 28da80a2cb..ccfe29430c 100644 --- a/flake.lock +++ b/flake.lock @@ -112,16 +112,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1726098480, - "narHash": "sha256-BOCKGOKzJLlYHSOCd2QOERS/sE038domlBc1h6nvM5s=", + "lastModified": 1726682574, + "narHash": "sha256-7Ax/6SCgdhoLGtgBFnlj5mRSDqEgrY85pCPtiM+fGFU=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "344d1335c0fb8d146b0fa2954b0194afbe11dae6", + "rev": "bf51ee42f74066ab3bb6ef9e8697d04fbee503fd", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.88", + "ref": "v0.1.92", "repo": "llvm-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index d3773a100d..b7cdb4ebe7 100644 --- a/flake.nix +++ b/flake.nix @@ -1,7 +1,7 @@ { description = "K Framework"; inputs = { - llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.88"; + llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.92"; haskell-backend = { url = "github:runtimeverification/haskell-backend/v0.1.76"; inputs.rv-utils.follows = "llvm-backend/rv-utils"; diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index 344d1335c0..bf51ee42f7 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit 344d1335c0fb8d146b0fa2954b0194afbe11dae6 +Subproject commit bf51ee42f74066ab3bb6ef9e8697d04fbee503fd