Skip to content
This repository was archived by the owner on Apr 25, 2024. It is now read-only.

Tags: runtimeverification/pyk

Tags

v0.1.769

Toggle v0.1.769's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Update dependency: deps/k_release (#1060)

Co-authored-by: devops <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>

v0.1.768

Toggle v0.1.768's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Enable Booster in all `KoreClientTest` subclasses (#1058)

Fixes #1005

---------

Co-authored-by: devops <[email protected]>

v0.1.767

Toggle v0.1.767's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Minimization algorithm correction (#1059)

This PR corrects an error in the KCFG minimization algorithm, where the
`_lift_split` function would incorrectly return `False` instead of
`True` even though a lift has been performed successfully. It also
contains a test that triggers the bug, that is, it fails using the
current `master` branch and passes using this PR.

---------

Co-authored-by: devops <[email protected]>

v0.1.766

Toggle v0.1.766's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Update dependency: deps/k_release (#1057)

Co-authored-by: devops <[email protected]>

v0.1.765

Toggle v0.1.765's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Add JSON-RPC server to pyk (#1014)

Addresses:
- #1019

Adds:
- Class `JsonRpcServer`, an abstract class for exposing a JSON RPC
interface over HTTP from pyk.
- The server is initialized with a host and port. Methods are registered
with `JsonRpcServer.register_method`, and the server is started with
`JsonRpcServer.serve`.
- A test that uses JSON-RPC methods to interact with a k configuration
and request concrete execution steps on it.

---------

Co-authored-by: devops <[email protected]>

v0.1.764

Toggle v0.1.764's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Further KCFG-to-KCFG transformations (#1009)

This PR expands on #995 by adding a transformation that joins
consecutive `Split` nodes into a single `Split`.

Additionally, the PR:
- corrects a bug in `lift_splits` that led to infinite looping in the
case a split could not be lifted due to freshly created variables;
- corrects the substitution computation in `lift_split`;
- non-destructively expands the testing helpers in `test_kcfg.py` to
allow for more expressivity;
- fixes a typo in the documentation of `CSubst.from_dict`.

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Palina Tolmach <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

v0.1.763

Toggle v0.1.763's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Fix `as_subsort` (#1046)

If `symbol` is present on a production, then it is not a subsort
production, even if it has a single, non-terminal production item.

---------

Co-authored-by: devops <[email protected]>

v0.1.762

Toggle v0.1.762's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Adjust overload axiom generation (#1028)

Related:
* runtimeverification/k#4136

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>

v0.1.761

Toggle v0.1.761's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Fix `SmtSolverError` (#1055)

Related:
* runtimeverification/haskell-backend#3748

---------

Co-authored-by: devops <[email protected]>

v0.1.760

Toggle v0.1.760's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Enable inline K definitions in tests (#1050)

* Add parameter `definition` to `Kompiler.__call__`
* Add attribute `KOMPILE_DEFINITION` to `KompiledTest`
* Inline small, single-use definitions
* Remove unused definitions
* Move `k-files` into `test-data`
* Fix (most) kompilation warnings

---------

Co-authored-by: devops <[email protected]>