Skip to content
K Framework Tools 5.0
Java Scala Standard ML OCaml Python Makefile Other
Branch: master
Clone or download
dwightguth and rv-jenkins bison depends on gettext but doesn't declare that dependency on arch (#…
…1062)

Co-authored-by: rv-jenkins <admin@runtimeverification.com>
Latest commit cd9ba88 Jan 28, 2020
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.idea keep simple methods in one line Dec 2, 2015
debian kast --gen-parser prototype (#1003) Jan 9, 2020
haskell-backend Update dependencies (#1043) Jan 28, 2020
java-backend Delete a bunch of outdated and dead code (#1059) Jan 27, 2020
k-distribution Update dependencies (#1043) Jan 28, 2020
kernel Delete a bunch of outdated and dead code (#1059) Jan 27, 2020
kore Check for duplicate module names (#1024) Jan 15, 2020
ktree More KRead stuff, plus renaming KoreParser (#540) Jun 12, 2019
llvm-backend llvm-backend/src/main/native/llvm-backend: update submodule (#1060) Jan 28, 2020
ocaml-backend kernel: KProveOptions: --concrete-rules is now implemented in front-e… Jan 16, 2020
src kast --gen-parser prototype (#1003) Jan 9, 2020
.gitattributes fix newlines of kserver on windows Jan 25, 2016
.gitignore Update llvm backend and remove rust dependency (#738) Sep 3, 2019
.gitmodules Build Haskell backend as a submodule, hook into Maven (#228) Jan 30, 2019
CHANGELOG.md fix bug with parsing of NaN and Infinity in modules with identifiers (#… Jan 23, 2019
CODEOWNERS dwightguth is a code owner of documentation (#825) Oct 7, 2019
Dockerfile.arch pyk code for working with K coverage logs (#971) Dec 13, 2019
Dockerfile.debian kast --gen-parser prototype (#1003) Jan 9, 2020
Jenkinsfile Makefile system: tweaks to make it compatible with global --debug opt… Jan 20, 2020
LICENSE.md fix bug with parsing of NaN and Infinity in modules with identifiers (#… Jan 23, 2019
PKGBUILD bison depends on gettext but doesn't declare that dependency on arch (#… Jan 28, 2020
README.md kast --gen-parser prototype (#1003) Jan 9, 2020
install-k Update dependencies + Debian Buster (#640) Jul 25, 2019
kframework.install Revert "Packaging updates (#655)" Jul 31, 2019
pending-documentation.md Update pending-documentation (#963) Jan 15, 2020
pom.xml Update to latest llvm backend (#838) Oct 16, 2019

README.md

Join the chat at https://gitter.im/kframework/k

This is a readme file for the developers.

Prerequisites

In short:

On Ubuntu:

git submodule update --init --recursive
sudo apt-get install build-essential m4 openjdk-8-jdk libgmp-dev libmpfr-dev pkg-config flex bison z3 libz3-dev maven opam python3 cmake gcc clang-8 lld-8 llvm-8-tools zlib1g-dev libboost-test-dev libyaml-dev libjemalloc-dev
curl -sSL https://get.haskellstack.org/ | sh

On Arch (from source):

git submodule update --init --recursive
sudo pacman -S git maven jdk-openjdk cmake boost libyaml jemalloc clang llvm lld zlib gmp mpfr z3 opam curl stack base-devel base python
export PATH=$PATH:/usr/bin/core_perl
makepkg
sudo pacman -U kframework-5.0.0-1-x86_64.pkg.tar.xz

If you install this list of dependencies, continue directly to the Install section.

Java Development Kit (required JDK8 version 8u45 or higher)

Linux:

  • Download from package manager (e.g. sudo apt-get install openjdk-8-jdk)

Mac/Windows:

  • Download the JDK here

To make sure that everything works you should be able to call java -version and javac -version from a Terminal.

Apache Maven

Linux:

  • Download from package manager (e.g. sudo apt-get install maven)

Mac:

Windows:

  • Go to http://maven.apache.org/download.cgi and download the zip with the binary distribution. Unzip it in your desired location and follow the installation instructions on the webpage.

Maven usually requires setting an environment variable JAVA_HOME pointing to the installation directory of the JDK (not to be mistaken with JRE).

You can test if it works by calling mvn -version in a Terminal. This will provide the information about the JDK Maven is using, in case it is the wrong one.

Haskell Stack

To install, go to https://docs.haskellstack.org/en/stable/README/ and follow the instructions. You may need to do stack upgrade to ensure the latest version of Haskell Stack.

Miscellaneous

Also required:

These can all be installed from your package manager.

Install

Checkout the directory of this README in your desired location and call mvn package from the main directory to build the distribution. For convenient usage, you can update your $PATH with k-distribution/target/release/k/bin (strongly recommended, but optional).

You are also encouraged to set the environment variable MAVEN_OPTS to -XX:+TieredCompilation, which will significantly speed up the incremental build process.

After running mvn package for the first time, you should run k-distribution/target/release/k/bin/k-configure-opam; eval `opam config env` . This performs first-time setup of the OCAML backend.

Installing on fresh Windows Subsystem for Linux

  1. Install the Ubuntu package from the Windows Store, which as of now is an alias for the Ubuntu LTS 18.04 package. During installation you will be asked to create a new user.

  2. Download the latest K distribution for Ubuntu Bionic from https://github.com/kframework/k/releases to a temporary directory, for example d:\temp

  3. Open linux bash. For example by running:

ubuntu1804
  1. Run the following commands:

    $ sudo apt-get update

    $ cd <download dir>. In our example download dir is /mnt/d/temp

    $ sudo apt-get install ./kframework_5.0.0_amd64_bionic.deb This will install ~1.4GB of dependencies and will take some time. K will be installed to /usr/lib/kframework

  2. Copy the tutorial to some work directory, for example /mnt/d/k-tutorial. Otherwise, you won't be able to run the examples from default installation dir if you are not root:

$ cp -R /usr/lib/kframework/tutorial /mnt/d/k-tutorial
  1. Now you can try to run some programs:
$ cd /mnt/d/k-tutorial/2_languages/1_simple/1_untyped
$ make kompile
$ krun tests/diverse/factorial.simple

IDE Setup

General

You should run K from the k-distribution project, because it is the only project to have the complete classpath and therefore all backends.

Eclipse

N.B. the Eclipse internal compiler may generate false compilation errors (there are bugs in its support of Scala mixed compilation). We recommend using IntelliJ IDEA if at all possible.

To autogenerate an Eclipse project for K, run mvn install -DskipKTest; mvn eclipse:eclipse on the command line, and then go into each of the kore and tiny directories and run sbt eclipse. Then start eclipse and go to File->Import->General->Existing projects into workspace, and select the directory of the installation. You should only add the leaves to the workspace, because eclipse does not support hierarchical projects.

IntelliJ IDEA

IntelliJ IDEA comes with built-in maven integration. For more information, refer to the IntelliJ IDEA wiki

Run test suite

To completely test the current version of the K framework, run mvn verify. This normally takes roughly 30 minutes on a fast machine. If you are interested only in running the unit tests and checkstyle goals, run mvn verify -DskipKTest to skip the lengthy ktest execution.

Changing the KORE data structures

If you need to change the KORE data structures (unless you are a K core developer, you probably do not), see Guide-for-changing-the-KORE-data-structures.

Build the final release directory/archives

Call mvn install in the base directory. This will attach an artifact to the local maven repository containing a zip and tar.gz of the distribution.

The functionality to create a tagged release is currently incomplete.

Compiling definitions and running programs

Assuming k-distribution/target/release/k/bin is in your path, you can compile definitions using the kompile command. To execute a program you can use krun.

For running either program in the debugger, use the main class org.kframework.main.Main with an additional argument -kompile or -krun added before other command line arguments, and use the classpath from the k-distribution module.

Troubleshooting

Common error messages:

  • Error: JAVA_HOME not found in your environment. Please set the JAVA_HOME variable in your environment to match the location of your Java installation.

    • Make sure JAVA_HOME points to the JDK and not the JRE directory.
  • [WARNING] Cannot get the branch information from the git repository: Detecting the current branch failed: 'git' is not recognized as an internal or external command, operable program or batch file.

    • git might not be installed on your system. Make sure that you can execute git from the command line.
  • 1) Error injecting constructor, java.lang.Error: Unresolved compilation problems: The import org.kframework.parser.outer.Outer cannot be resolved Outer cannot be resolved

    • You may run into this issue if target/generated-sources/javacc is not added to the build path of your IDE. Generally this is solved by regenerating your project / re-syncing it with the pom.xml.
  • [ERROR] Failed to execute goal org.apache.maven.plugins:maven-compiler-plugin:3.1:compile (default-compile) on project k-core: Fatal error compiling: invalid target release: 1.8 -> [Help 1]

    • You either do not have Java 8 installed, or $JAVA_HOME does not point to a Java 8 JDK.

If something unexpected happens and the project fails to build, try mvn clean and rebuild the entire project. Generally speaking, however, the project should build incrementally without needing to be cleaned first.

If you are doing work with snapshot dependencies, you can update them to the latest version by running maven with the -U flag.

If you are configuring artifacts in a repository and need to purge the local repository's cache of artifacts, you can run mvn dependency:purge-local-repository.

If tests fail but you want to run the build anyway to see what happens, you can use mvn package -DskipTests.

If you still cannot build, please contact a K developer.

You can’t perform that action at this time.