Skip to content

Kore REPL

Jump to bottom
David Cox edited this page Oct 12, 2021 · 18 revisions

Kore REPL

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

Prerequisites

Clone Kore and build the REPL:

$ git clone https://github.com/kframework/kore.git
$ cd kore/
$ make kore-repl

This will install the kore-repl executable to path/to/kore/.build/kore/bin so be sure to add path/to/kore/.build/kore/bin to your PATH.

Tip: replace make kore-repl with make all above to build all executables including kore-exec, kore-repl, and kore-parser.

Install the K frontend. Note, we skip building the Haskell backend with -Dhaskell.backend.skip because we already built Kore above.

$ git clone https://github.com/kframework/k.git
$ cd k/
$ mvn package -Dhaskell.backend.skip

This will install the K frontend executables to path/to/k/k-distribution/target/release/k/bin so be sure to add path/to/k/k-distribution/target/release/k/bin to your PATH.

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. E.g. on Ubuntu:

$ sudo apt install graphviz
$ which dot
/usr/bin/dot

Running the REPL

Let's start an example REPL on the Kore test all-path/00-basic/00-no-rules with distinct-spec.k:

$ cd test/all-path/00-basic/00-no-rules
$ make distinct-spec.k.repl
...
Welcome to the Kore Repl! Use 'help' to get started.

Kore (0)> ...

Alternatively, use make -C to run the REPL from the test directory:

$ make -C all-path/00-basic/00-no-rules distinct-spec.k.repl

Looking under the make hood, the Makefile first kompiles the definition then uses kprove to start the repl:

$ kompile --backend haskell -d . path.k
$ kprove --haskell-backend-command /path/to/kore/.build/kore/bin/kore-repl -d . -m VERIFICATION distinct-spec.k

The --directory, -d switch sets the path to the directory in which the output resides. An output can be either a kompiled K definition or a document which depends on the type of backend. The default is the directory containing the main definition file.

The --def-module, -m switch sets the name of module containing the definition to prove under. You can find the VERIFICATION module for this test in distinct-spec.k.

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

You will have to manually compile to kore to obtain vdefinition.kore and spec.kore if you chose to run kore-repl yourself. Continuing the example above in kore/test/all-path/00-basic/00-no-rules, first we run kompile then we run kprove with the --dry-run switch. This will print out the kore-repl command we can call to enter the repl. Additionally kprove will create a .kprove-... directory containing spec.kore and vdefinition.kore. Note that kprove will not run the Haskell backend when using the --dry-run switch.

$ kompile --backend haskell -d . path.k
$ kprove --dry-run --haskell-backend-command kore-repl -d . -m VERIFICATION distinct-spec.k
kore-repl path/to/all-path/00-basic/00-no-rules/./.kprove-.../vdefinition.kore --module VERIFICATION --prove path/to/all-path/00-basic/00-no-rules/./.kprove-.../spec.kore --spec-module DISTINCT-SPEC --output path/to/all-path/00-basic/00-no-rules/./.kprove-.../result.kore

If you want to run the Haskell backend while also saving the .kore-... directory created by kprove then remove --dry-run and instead use the --save-temps switch.

Commands in the Kore REPL

Within the REPL, run help to see a list of available REPL commands, modifiers, explanations, and log-entry types. When finished, run exit to quit the REPL.

Alternatively, run kore-repl --help from the command line.

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 does not work if you run the repl through kprove. See above for how to run kore-repl directly.

REPL scripts

The REPL can execute commands from a file. When supplying a repl script file as a command line argument, the repl can be run in two modes: interactive (default) or run-mode. After a script is executed in interactive mode you will be taken to the repl prompt. Running a script in run-mode will output the status of the proof after executing the script and exit. You can also load scripts while inside the repl by using the load command.

Command line arguments for when running kore-repl directly (as above):

  • --run-mode or -r: flag to run in run-mode; if you omit this argument you will run the repl in interactive mode
  • --repl-script: path to the script

So, in order to run in run-mode using script.kscript found in the current directory:

$ /path/to/kore-repl path/to/vdefinition.kore --module VERIFICATION --prove /path/to/spec.kore --spec-module SPEC-NAME --repl-script script.kscript --run-mode

Exit codes for run-mode:

  • exit code 0: successful execution and proof was completed
  • exit code 1: error during execution
  • exit code 2: successful execution but proof was not finished

K output

The repl has some commands which output patterns. By default, these patterns are written in KORE, but can be transformed to K by using the commands defined in kore/dist/kast.kscript. You can manually load the script using load after starting the repl, or execute the script at the beginning by supplying it as a command line argument (see the section above for further details).

The commands which output K have similar names to their KORE outputting counterparts, e.g. konfig instead of config or ktry instead of try. Some can be suffixed with -n, -d or -nd for specifying the argument, the directory or both, respectively.

  • kcliam, konfig and krule don't require the argument for their counterparts; can be suffixed with -n, -d or -nd
  • kaxiom, ktry and ktryf require the argument for their counterparts; can be suffixed with -d

See the kast.kscript for the full list of K commands.

Clone this wiki locally