Skip to content

Releases: runtimeverification/mir-semantics

v0.2.32: Update dependency: deps/pyk_release (#333)

28 Feb 20:07
d1ba399
Compare
Choose a tag to compare
Automerge https://github.com/runtimeverification/mir-semantics/pull/333: Update dependency: deps/pyk_release

v0.2.31: Update dependency: deps/pyk_release (#332)

28 Feb 15:07
577ba08
Compare
Choose a tag to compare
* deps/pyk_release: Set Version v0.1.661

* Set Version: 0.2.31

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.662

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

---------

Co-authored-by: devops <devops@runtimeverification.com>

v0.2.30: Update dependency: deps/pyk_release (#331)

27 Feb 22:48
2516ab9
Compare
Choose a tag to compare
* deps/pyk_release: Set Version v0.1.657

* Set Version: 0.2.30

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.658

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.659

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.660

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

---------

Co-authored-by: devops <devops@runtimeverification.com>

v0.2.29: Update dependency: deps/pyk_release (#326)

27 Feb 15:59
23b3ff1
Compare
Choose a tag to compare
* deps/pyk_release: Set Version v0.1.620

* Set Version: 0.2.27

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.621

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.622

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.623

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.624

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.625

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.626

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.627

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.628

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.2.27

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.629

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.630

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.631

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.632

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.633

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.2.30

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.634

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.635

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.2.31

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.636

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.2.33

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.637

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.2.35

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.638

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.639

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.640

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.641

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.642

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.643

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.2.37

* flake.{nix,lock}: update Nix derivations

* Change EqualityProver to ImpliesProver

* Moved arguments for `advance_proof` to `APRProver`

* deps/pyk_release: Set Version v0.1.644

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.2.38

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.645

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.646

* Set Version: 0.2.28

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.647

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.648

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.3.3

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.649

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.3.4

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.650

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.3.5

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.651

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.653

* Set Version: 0.2.29

* deps/pyk_release: Set Version v0.1.654

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.655

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* kmir.py/: adjustments for new CTermSymbolic/KCFGExplore interface

* sum-to-n.run.out: update expected output

* deps/pyk_release: Set Version v0.1.656

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: dkcumming <daniel.cumming@runtimeverification.com>
Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

v0.2.28: Add feature: prove a single claim in `kmir prove` (#325)

26 Feb 14:56
d0092c0
Compare
Choose a tag to compare
* add command option `--claim` for `kmir prove`

* Set Version: 0.2.26

* fix claim not found issue

* add `--claim-list` option

* Set Version: 0.2.27

* Set Version: 0.2.27

* Set Version: 0.2.28

---------

Co-authored-by: yanliu18 <yan.emma.liu@gmail.com>
Co-authored-by: devops <devops@runtimeverification.com>

v0.2.27: Replace usages of `priorities`, `require`, and `import` (#329)

22 Feb 10:29
7598a55
Compare
Choose a tag to compare
* Replace deprecated tokens

* Set Version: 0.2.27

---------

Co-authored-by: devops <devops@runtimeverification.com>

v0.2.26: Update dependency: deps/pyk_release (#324)

12 Feb 02:29
baa8be0
Compare
Choose a tag to compare
* deps/pyk_release: Set Version v0.1.615

* Set Version: 0.2.26

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.616

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.617

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.618

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.619

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

---------

Co-authored-by: devops <devops@runtimeverification.com>

v0.2.25: Update dependency: deps/pyk_release (#314)

06 Feb 02:43
49cfe8d
Compare
Choose a tag to compare
* deps/pyk_release: Set Version v0.1.606

* Set Version: 0.2.23

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.607

* Set Version: 0.2.24

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.608

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.1.105

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.609

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.1.106

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.610

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.2.1

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.611

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.2.2

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.612

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.613

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.614

* kmir/{pyproject.toml,poetry.lock}: sync Poetry files

* deps/k_release: sync release file version 6.2.4

* flake.{nix,lock}: update Nix derivations

* Set Version: 0.2.25

* Added label to labelless claim

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>
Co-authored-by: dkcumming <daniel.cumming@runtimeverification.com>

v0.2.24: Updates to proof feedback. (#323)

06 Feb 00:17
cc1a794
Compare
Choose a tag to compare
* Updates to proof feedback.

Replaced printing of information for passing and failing proofs.
Updated `prove` so pytest catches all failures.
In process of creating `show-proof` test harness.

* Set Version: 0.2.24

* Fixed formatting and typing

* Updated failing `.tsv`

* Back to file names instead of specific tests in report file

* Partial add of functionality to compare and save tests

* Moved printing of `show_proof` out to `__main__.py`

* Progress on storing and comparing show output

* Flag passed to pytest to update expected output

* Formatting and types

* Fixed bug for report file, and added documentation update

* removed unnecessary comment

* Fixed typo

---------

Co-authored-by: devops <devops@runtimeverification.com>

v0.2.23: Refactor/kmir class (#312)

31 Jan 09:19
61d7d1b
Compare
Choose a tag to compare
* add the overflow test case

* move overflow test case to buggy program folder

* minor resutructure of tests

* move overflow test case to demo folder

* restructured test-prove.py test input, updated failed test list

* restrcture prove test

* updated manual

* Manual update finish

* fix type and formatting

* format issue

* exclude parse fail tests cases from run test

* minor update of run test script

* add allow skip and report file to test_prove

* fix nix test command

* fix nix .kmir-test build failure

* fix required directory

* adding links to prerequisites installation

* fix comments

* refactor parse and run

* refactor prove

* Set Version: 0.2.5

* add kmir object

* refine KMIR class object, simplify parse/run methdos

* fix llvm interpreter in run, supporting latex and binary as run output format

* add parse output format support for binary and latex

* remove repeated print code, keep KORE object within KMIR class

* kore-print pretty

* add logging format

* Set Version: 0.2.10

* redesign kmir prove

* sync init

* proof.status not reachable

* minor

* obtain proof result

* using KMIR object in show kcfg

* merge with stashed changes

* Set Version: 0.2.15

* failed to modularise the rpc call

* add a prove example to demo

* prepare a clean version for debugging

* experiment with context manager

* fix kcfg_explore

* minor renaming

* minor

* Set Version: 0.2.19

* minor

* kmir prove is working

* formatting

* update kmir command

* change to 1 to 1 server-client

* formatting

* update nix texts

* refactoring kcfg show to show proof of a claim

* refactor the view kcfg option

* use APRProofShow

* update manual

* merge show and view proof to prove

* cleanup codebase and update manual

* Set Version: 0.2.22

* revise the unit test case

* Update kmir/src/tests/integration/test_prove.py

remove comments

Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>

* minor

* reformat

* Set Version: 0.2.23

* fixed KoreServer breaking change from pyk update

---------

Co-authored-by: yanliu18 <yan.emma.liu@gmail.com>
Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>
Co-authored-by: dkcumming <daniel.cumming@runtimeverification.com>