{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":50041690,"defaultBranch":"master","name":"k","ownerLogin":"runtimeverification","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2016-01-20T16:05:56.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/3732719?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1725917145.0","currentOid":""},"activityList":{"items":[{"before":"a91e1335840eda4993bcce31c3f30e0eaa789890","after":"eda96375b808442ebd968812c7e5500b20a18d88","ref":"refs/heads/gh-pages","pushedAt":"2024-09-09T22:17:57.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"gh-pages: Updated the website","shortMessageHtmlLink":"gh-pages: Updated the website"}},{"before":"464852c23ecdf15bbe772802e0a4b96e5b95ee47","after":"ddc22368b132914e64811f507c87725d1b96dc4d","ref":"refs/heads/master","pushedAt":"2024-09-09T21:25:31.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"Set Version: 7.1.139","shortMessageHtmlLink":"Set Version: 7.1.139"}},{"before":"cf82a80c976eb96c5a63fddb667b8bb930ef3dc0","after":null,"ref":"refs/heads/fix-subst-minimize","pushedAt":"2024-09-09T21:25:12.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"}},{"before":"2f4d4f5575ca44b2e5860fcac200de1e5903dcf6","after":"b6e638de1c92888f1ac8f94b223fa3eb408adbd9","ref":"refs/heads/develop","pushedAt":"2024-09-09T21:25:10.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"Minimize substitutions by default (#4635)\n\nSubstitutions in actual proofs are really quite large, so this addresses\ntwo problems:\n\n- When printing multiline substitutions, we had some whitespace/newline\nerrors.\n- Substitutions shouldn't be printed unless non-minimization is turned\non.","shortMessageHtmlLink":"Minimize substitutions by default (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2514815185\" data-permission-text=\"Title is private\" data-url=\"https://github.com/runtimeverification/k/issues/4635\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/runtimeverification/k/pull/4635/hovercard\" href=\"https://github.com/runtimeverification/k/pull/4635\">#4635</a>)"}},{"before":"c449855d8c55bf45a3ac294d912e184ed31ea4e3","after":"e5340387754ce3bae088d854a90f012418a4ed46","ref":"refs/heads/_update-deps/runtimeverification/haskell-backend","pushedAt":"2024-09-09T21:00:11.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"flake.lock: update","shortMessageHtmlLink":"flake.lock: update"}},{"before":"9e37c487d1871aa9e4e3a6faa43934f0cf215dcc","after":"c449855d8c55bf45a3ac294d912e184ed31ea4e3","ref":"refs/heads/_update-deps/runtimeverification/haskell-backend","pushedAt":"2024-09-09T20:59:03.000Z","pushType":"push","commitsCount":9,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"deps/haskell-backend_release: Set Version v0.1.81","shortMessageHtmlLink":"deps/haskell-backend_release: Set Version v0.1.81"}},{"before":null,"after":"cf82a80c976eb96c5a63fddb667b8bb930ef3dc0","ref":"refs/heads/fix-subst-minimize","pushedAt":"2024-09-09T20:04:55.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ehildenb","name":"Everett Hildenbrandt","path":"/ehildenb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12721972?s=80&v=4"},"commit":{"message":"pyk/tests/unit/test_kcfg: update expected output","shortMessageHtmlLink":"pyk/tests/unit/test_kcfg: update expected output"}},{"before":"4e44f2dbe3fa7fd164711bf5bc20a4045224b437","after":"b4ebdc94d8741e0c359f43daf88db5b4a8428b93","ref":"refs/heads/list-set","pushedAt":"2024-09-09T19:57:51.000Z","pushType":"push","commitsCount":10,"pusher":{"login":"dwightguth","name":"Dwight Guth","path":"/dwightguth","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5104541?s=80&v=4"},"commit":{"message":"fix bug in raising of exceptions from llvm backend pattern matching code","shortMessageHtmlLink":"fix bug in raising of exceptions from llvm backend pattern matching code"}},{"before":"31650b5185acf16b96ea4115906e97656a7daf27","after":"a91e1335840eda4993bcce31c3f30e0eaa789890","ref":"refs/heads/gh-pages","pushedAt":"2024-09-09T19:15:29.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"gh-pages: Updated the website","shortMessageHtmlLink":"gh-pages: Updated the website"}},{"before":"80310780c3a65102b86692184ff7761e447efa40","after":"464852c23ecdf15bbe772802e0a4b96e5b95ee47","ref":"refs/heads/master","pushedAt":"2024-09-09T18:28:50.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"Set Version: 7.1.138","shortMessageHtmlLink":"Set Version: 7.1.138"}},{"before":"0e6ba9887c49336b4e95052489f2c43a807a7bc3","after":null,"ref":"refs/heads/fix-subst-ml-pred","pushedAt":"2024-09-09T18:28:30.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"}},{"before":"15cbf88d8c337adc48b3c475e941c9addd438e06","after":"2f4d4f5575ca44b2e5860fcac200de1e5903dcf6","ref":"refs/heads/develop","pushedAt":"2024-09-09T18:28:29.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"Cleanups to handling ml predicates and substitutions (#4625)\n\n~Blocked on: https://github.com/runtimeverification/k/pull/4631~\n~Blocked on: https://github.com/runtimeverification/k/pull/4630~\n~Blocked on: https://github.com/runtimeverification/k/pull/4633~\n\nWhile reviewing and going over\nhttps://github.com/runtimeverification/k/pull/4621 with @Stevengre , it\nbecame somewhat clear that how we handle turning substitions into ML\npredicates is a bit dirty. This attempts to clean this up a bit. Where\npotentially breaking changes to API are introduced here, I've checked if\nit affects the following repos when I mention \"downstream\" below:\n`evm-semantics kontrol wasm-semantics riscv-semantics mir-semantics`.\n\nIn particular:\n\n- The function `CTerm.anti_unify` has a simplification where it reuses a\nfunction from `kast.manip` instead of reimplementing it.\n- The functions `CSubst.from_pred` and `CSubst.pred` are added, as\nreplacements for `Subst.ml_pred`. This is because `Subst.ml_pred`\ndoesn't have a good way to produce correctly sorted predicates, because\nit's in module `kast.inner`.\n- `Subst.ml_pred` is removed, and tests are updated to use the new\n`CSubst` variant. None of the downstream repositories use\n`Subst.ml_pred` directly.\n- The new `CSubst.pred` correctly sorts the generated `#Equals` clauses,\ndefaulting to `K` sort or if a `KDefinition` is supplied using it to do\nsort inference. It also provides options for controlling whether we\ninclude the substitution or the constraints in the generated predicate.\n- A test is added for a `CSubst.pred` case which caused a bug in the\nintegration tests dealing with identity substitutions.\n- The `CTermSymbolic.implies` function is updated to reuse\n`CSubst.from_pred` instead of reimplementing it.\n- On the case of duplicate entries, the first is kept and the latter are\nmade as predicates.","shortMessageHtmlLink":"Cleanups to handling ml predicates and substitutions (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2508871854\" data-permission-text=\"Title is private\" data-url=\"https://github.com/runtimeverification/k/issues/4625\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/runtimeverification/k/pull/4625/hovercard\" href=\"https://github.com/runtimeverification/k/pull/4625\">#4625</a>)"}},{"before":"221a49aae1d9915157f0aade63e80e8dbbfd59f1","after":"505e597f3eb64eb2760cc4ee01e1843ab0a4a3cd","ref":"refs/heads/_update-deps/runtimeverification/llvm-backend","pushedAt":"2024-09-09T17:05:12.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"flake.lock: update","shortMessageHtmlLink":"flake.lock: update"}},{"before":"a2d4f654ca627ab1ad10952995b678d243a4fc22","after":"221a49aae1d9915157f0aade63e80e8dbbfd59f1","ref":"refs/heads/_update-deps/runtimeverification/llvm-backend","pushedAt":"2024-09-09T17:03:56.000Z","pushType":"push","commitsCount":9,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"deps/llvm-backend_release: Set Version 0.1.86","shortMessageHtmlLink":"deps/llvm-backend_release: Set Version 0.1.86"}},{"before":"8757594842a364961e4af4d3f6d403b8ede82072","after":"0e6ba9887c49336b4e95052489f2c43a807a7bc3","ref":"refs/heads/fix-subst-ml-pred","pushedAt":"2024-09-09T15:45:13.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"ehildenb","name":"Everett Hildenbrandt","path":"/ehildenb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12721972?s=80&v=4"},"commit":{"message":"pyk/cterm/cterm.py: only call sort_with once","shortMessageHtmlLink":"pyk/cterm/cterm.py: only call sort_with once"}},{"before":"79d45ec730fc29900e90ad6964c6cc3f652234a9","after":"31650b5185acf16b96ea4115906e97656a7daf27","ref":"refs/heads/gh-pages","pushedAt":"2024-09-09T03:21:03.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"gh-pages: Updated the website","shortMessageHtmlLink":"gh-pages: Updated the website"}},{"before":"9a24de6622a6046f4806411b21e1e4c63d9204f1","after":"a2221ec0e917b8067e5c05184875913d9bfbf300","ref":"refs/heads/feature-merge-node","pushedAt":"2024-09-09T02:51:55.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Stevengre","name":"JianHong Zhao","path":"/Stevengre","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22110165?s=80&v=4"},"commit":{"message":"update test","shortMessageHtmlLink":"update test"}},{"before":"62e06f466f3fef150598894798fa340d68bb3fdb","after":"80310780c3a65102b86692184ff7761e447efa40","ref":"refs/heads/master","pushedAt":"2024-09-09T02:34:41.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"Set Version: 7.1.137","shortMessageHtmlLink":"Set Version: 7.1.137"}},{"before":"fb07b5da1ffa1365ca2d0607134903de64ef3ca9","after":null,"ref":"refs/heads/create-split-by-nodes","pushedAt":"2024-09-09T02:34:20.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Stevengre","name":"JianHong Zhao","path":"/Stevengre","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22110165?s=80&v=4"}},{"before":"86cb320c64e7dff745ea20ce75005cb36e97c990","after":"15cbf88d8c337adc48b3c475e941c9addd438e06","ref":"refs/heads/develop","pushedAt":"2024-09-09T02:34:19.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Stevengre","name":"JianHong Zhao","path":"/Stevengre","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22110165?s=80&v=4"},"commit":{"message":"Create Split without CSubst (#4617)\n\n1. generate `CSubst` from the targets for `Split`\r\n2. fix a bug in `CSubst.apply`.","shortMessageHtmlLink":"Create Split without CSubst (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2500278833\" data-permission-text=\"Title is private\" data-url=\"https://github.com/runtimeverification/k/issues/4617\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/runtimeverification/k/pull/4617/hovercard\" href=\"https://github.com/runtimeverification/k/pull/4617\">#4617</a>)"}},{"before":"bc096e530f85b0e37785ac61ebbfd0929dbb3c67","after":"fb07b5da1ffa1365ca2d0607134903de64ef3ca9","ref":"refs/heads/create-split-by-nodes","pushedAt":"2024-09-09T00:59:00.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Stevengre","name":"JianHong Zhao","path":"/Stevengre","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22110165?s=80&v=4"},"commit":{"message":"udpate test","shortMessageHtmlLink":"udpate test"}},{"before":"fabd007cf2f69ba8be87eeadda5218ff8979a934","after":"bc096e530f85b0e37785ac61ebbfd0929dbb3c67","ref":"refs/heads/create-split-by-nodes","pushedAt":"2024-09-09T00:52:51.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"Stevengre","name":"JianHong Zhao","path":"/Stevengre","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22110165?s=80&v=4"},"commit":{"message":"udpate test","shortMessageHtmlLink":"udpate test"}},{"before":"a4a3ae954df1732817bf15b260c2bd418d6599b2","after":"8757594842a364961e4af4d3f6d403b8ede82072","ref":"refs/heads/fix-subst-ml-pred","pushedAt":"2024-09-06T18:31:12.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ehildenb","name":"Everett Hildenbrandt","path":"/ehildenb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12721972?s=80&v=4"},"commit":{"message":"cterm/cterm: do not include identity substiutions in CSubst.pred","shortMessageHtmlLink":"cterm/cterm: do not include identity substiutions in CSubst.pred"}},{"before":"b895f563aa394900c01e6c33dcfcfccb865c1157","after":"79d45ec730fc29900e90ad6964c6cc3f652234a9","ref":"refs/heads/gh-pages","pushedAt":"2024-09-06T18:28:59.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"gh-pages: Updated the website","shortMessageHtmlLink":"gh-pages: Updated the website"}},{"before":"5a9154997d06f3008697c39ed63d2131811f100f","after":"62e06f466f3fef150598894798fa340d68bb3fdb","ref":"refs/heads/master","pushedAt":"2024-09-06T17:42:56.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"Set Version: 7.1.136","shortMessageHtmlLink":"Set Version: 7.1.136"}},{"before":"74a46261f53f221147e523a3ac09517e7330778f","after":null,"ref":"refs/heads/ml-equals-sort","pushedAt":"2024-09-06T17:42:36.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"}},{"before":"82f8de028d51876bddcf44a3b658ecb58a880306","after":"86cb320c64e7dff745ea20ce75005cb36e97c990","ref":"refs/heads/develop","pushedAt":"2024-09-06T17:42:34.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"Adjust the sort of `mlEquals` (#4633)\n\nCurrently `mlEquals` has `GeneratedTopCell` as the default argument\nsort, which is pretty specific/limited. Instead, we set `K` as the\ndefault argument sort (supersort of all sorts), and then go to all the\nsites that use it and specify the argument sort more carefully.\n\nThis doesn't affect any downstream repos, none of them use `mlEquals`\ndirectly.","shortMessageHtmlLink":"Adjust the sort of <code>mlEquals</code> (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2510665581\" data-permission-text=\"Title is private\" data-url=\"https://github.com/runtimeverification/k/issues/4633\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/runtimeverification/k/pull/4633/hovercard\" href=\"https://github.com/runtimeverification/k/pull/4633\">#4633</a>)"}},{"before":"3221eca9b0a0b09082f171349ba31cd69a085f3e","after":"b895f563aa394900c01e6c33dcfcfccb865c1157","ref":"refs/heads/gh-pages","pushedAt":"2024-09-06T16:21:14.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"gh-pages: Updated the website","shortMessageHtmlLink":"gh-pages: Updated the website"}},{"before":"18c334a10bdf2f513c3eba72ace3d5e72beb598e","after":"74a46261f53f221147e523a3ac09517e7330778f","ref":"refs/heads/ml-equals-sort","pushedAt":"2024-09-06T16:16:25.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"ehildenb","name":"Everett Hildenbrandt","path":"/ehildenb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12721972?s=80&v=4"},"commit":{"message":"Merge branch 'develop' into ml-equals-sort","shortMessageHtmlLink":"Merge branch 'develop' into ml-equals-sort"}},{"before":"9235730f556700da132637ed71fc35aa9b252475","after":"3221eca9b0a0b09082f171349ba31cd69a085f3e","ref":"refs/heads/gh-pages","pushedAt":"2024-09-06T15:31:25.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"rv-jenkins","name":null,"path":"/rv-jenkins","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7210875?s=80&v=4"},"commit":{"message":"gh-pages: Updated the website","shortMessageHtmlLink":"gh-pages: Updated the website"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEsWjoCwA","startCursor":null,"endCursor":null}},"title":"Activity · runtimeverification/k"}