The Kore Language

Kore is the "core" part of the K framework.

What is Kore all about?

In short, we need a formal semantics of K. In K, users can define formal syntax and semantics of programming languages as K definitions, and automatically obtain parsers, interpreters, compilers, and various verification tools for their languages. Therefore K is a language-independent framework.

Thanks to years of research in matching logic and reachability logic, we know that all K does can be nicely formalized as logic reasoning in matching logic. To give K a formal semantics, we only need to formally specify the underlying matching logic theories with which K does reasoning. In practice, these underlying theories are complex and often infinite, and it is tricky to specify infinite theories without a carefully designed formal specification language. And Kore is such a language.

Structure of this project

The docs directory contains a collection of documents that describe the mathematical foundation of Kore and a BNF grammar that defines the syntax of Kore language. See /docs/introduction.md for an overview of the components of Kore.

The

kore

Building

Besides git, you will need stack or cabal to build

kore

stack build kore
# or
cabal build kore

If using

cabal

Using make:

make all # builds all binaries

Apple Silicon

If you are building the project on an Apple Silicon machine, a temporary workaround is necessary to install a new enough version of GHC with support for ARM64 Darwin. To do so, follow the instructions in this comment. The command-line flags for

stack

stack

make

STACK_BUILD_OPTS=--compiler ghc-8.10.7 --system-ghc

When

stack

ghc

Developing

Developers will require all the dependencies listed above, in addition to the requirements and recommendations below.

Required dependencies

For integration testing, we require:

• GNU make
• The K Framework frontend.

Instead of installing the frontend, you can use our

Dockerfile

docker.sh

./docker/build.sh  # run once when dependencies change
./docker/run.sh make all  # build the backend
./docker/run.sh make test  # run all tests
./docker/run.sh make -C test/imp test  # run all tests in test/imp

Recommended dependencies

For setting up a development environment, we recommend:

• direnv to make the project's tools available in shells and editors.
• haskell-language-server, a language server for Haskell that is compatible with most editors. See instructions below to run a language server.
• hlint for compliance with project guidelines.
• entr and fd for running

  ./entr.sh

  to keep important files up-to-date.

We recommend to keep

./entr.sh

Running a language server

To run a language server, developers will need to activate the appropriate

hie.yaml

ln -s hie-stack.yaml hie.yaml  # for Stack
# or
ln -s hie-cabal.yaml hie.yaml  # for Cabal
# or
ln -s hie-bios.yaml hie.yaml  # if all else fails

The project's dependencies must be installed before starting the language server:

stack build --test --bench --only-dependencies
# or
cabal build --enable-tests --enable-benchmarks --only-dependencies kore

Developing with Nix

We provide a

shell.nix

nix-shell

cabal

When the

.cabal

# Requires Nix to be installed.
./nix/rematerialize.sh

This script is also run by an automatic workflow.

We provide a

test.nix

nix-build test.nix  # run all integration tests
nix-build test.nix --argstr test imp  # run the integration tests in test/imp
nix-shell test.nix  # enter a shell where we can run tests manually