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

The

kore

Building

Besides git, you will need stack or cabal to build

kore

stack build kore
# or
cabal build kore

If using

cabal

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 ...

Recommended dependencies

For setting up a development environment, we recommend:

• direnv to make the project's tools available in shells and editors.
• ghcide or haskell-language-server, language servers for Haskell that are compatible with most editors. See instructions below to run a language server.
• hlint and stylish-haskell 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.