Kore REPL

Kore REPL

The Kore REPL is currently under early active development. Breaking changes may occur at any time.

Prerequisites

In order to see the execution graph (the graph command), you will need graphviz installed (and dot available in your path). This option currently only works on Linux.

In the root of the repository:

$ make k-frontend
$ stack build

Running the REPL

The REPL is currently setup to work with the imp proofs under the repository:

$ cd src/main/k/working/imp
$ make prove/max-spec.krepl

Running with other definitions/proofs

The kore-repl executable can be ran with any other languages/definitions.

You can run it with kprove, for example:

$ kprove --haskell-backend-command "/path/to/kore-repl " -d . -m VERIFICATION spec.k

In order to get the path to kore-repl, you can run stack exec -- which kore-repl.

Alternatively, you can run kore-repl directly:

$ /path/to/kore-repl path/to/vdefinition.kore --module VERIFICATION --prove /path/to/spec.kore --spec-module SPEC-NAME

Note you will have to manually compile to kore to obtain vdefinition.kore and spec.kore if you chose to run kore-repl yourself.

Interrupting

You can interrupt the repl while it is evaluating steps in order to stop long-running/infinite loops by pressing Ctrl-C. Please note that this not work if you run the repl through kprove. See above for how to run kore-repl directly.