Skip to content

Building Instructions

Garmelon edited this page Dec 8, 2022 · 30 revisions


Mathematica JLink is required for building KeYmaera X.

The build file uses default paths to the Mathematica JLink JAR that come with Mathematica on MacOS and Mathematica 10 (see file If those are not suitable for your setup, create a file in the same directory as (project root) and provide the location of JLink.jar with a property


Several example paths are listed in

Mathematica 12.2+

Incompatible for running on Ubuntu due to a backwards-incompatible change in the JLink native library code. (See Issue 72.) You will get an error like:

Error: {PATH_TO_JVM}: symbol lookup error: {PATH_TO_JLINK}: undefined symbol: uuid_generate

A temporary workaround follows:

  1. Locate using find / -type f -iname "libuuid*", for example in /lib/x86_64-linux-gnu/
  2. Then start KeYmaera X as follows: export LD_PRELOAD={path to}; java -jar keymaerax.jar

IDE Setup (Optional)

Development Environment Setup

How to Build

  1. Install Java JDK 1.8 from or from

  2. Install the Scala Build Tool (SBT) Version 1.3.7 on your system. It is available here: If you are using IntelliJ, this comes with the Scala plugin.

  3. Clone KeYmaera X from into a folder <keymaerax-root> of your choice

  4. Create a folder named keymaerax-projects in <keymaerax-root>/keymaerax-webui/src/main/resources. Clone the examples from into <keymaerax-root>/keymaerax-webui/src/main/resources/keymaerax-projects

  5. Compile KeYmaera X with the Scala Build Tool: from the root of the repository <keymaerax-root> (the directory containing build.sbt), run sbt compile

  6. Reinitialize the lemma database by deleting the KeYmaera X cache in your home directory and run the lemma initialization as follows:

    rm -rf ~/.keymaerax/cache
    sbt "testOnly"
  7. Optional: test your installation by running the full regression test suite:

    sbt test -l

How to Run

The web user interface of KeYmaera X can be started as follows:

sbt clean assembly
java -jar keymaerax.jar

The KeYmaera X core proof checker can be started as follows:

sbt "project core" clean assembly
# install Z3 in ~/.keymaerax/
java -jar keymaerax-core.jar -setup
java -jar keymaerax-core.jar -prove path/to/archive.kyx

If the jar does not start because of an error no manifest found, then first run sbt clean. In case of errors about invalid or corrupt jarfile, please update Java to a newer version.

To find out how to use KeYmaera X from command line instead of the web user interface, run:

java keymaerax.jar -help

API documentation is provided at while local documentation will be generated in the directory target/scala-2.12/unidoc with:

sbt unidoc

How to Test

Before running any tests, start KeYmaera X, configure it correctly from the web user interface, and make sure it is operational. The full but lengthy test suite can be run from command line, e.g., by

sbt test -l 

Leaving out slow tests can be run, e.g., by

sbt "testOnly -- -l -l -l -l"

A quicker smoke test suite can be run from command line, e.g., by

sbt "testOnly -- -n -n"

Selectively running individual test cases within the sbt interactive mode:

sbt>  test-only *USubst*

Or, run on a more fine-grained level within a class use object MyTest extends Tag("MyTest")

object MyTest extends Tag("MyTest")
it should "do something useful" taggedAs(MyTest) in {....}
it should "do anything useful" taggedAs(MyTest) in {....}
it should "do more good" taggedAs(MoreTest) in {....}

Then in sbt interactive mode run

sbt>  test-only -- -n "MyTest MoreTest"

To inline scala console output alongside the test suite information, first do:

sbt>  set logBuffered in Test := false

IntelliJ IDEA can also run the test suite (see #IntelliJ IDEA).

Further introduction to the testing framework is here:

FAQ: Build Problems

SBT Version

The build error

error: not found: value AssemblyPlugin (or one of many others, e.g., ScalaUnidoc, MergeStrategy, ...)

indicates that the installed SBT version might be too recent. In the build output look for line

[info] welcome to sbt

to inspect the SBT version. It should read 0.13.17. More recent SBT versions are not supported.

Class file version mismatch

A class version mismatch upon running keymaerax.jar indicates that the compiler used for building the jar is incompatible with the Java runtime used for executing:

Exception in thread "main" java.lang.UnsupportedClassVersionError: ... has been 
compiled by a more recent version of the Java Runtime (class file version X), 
this version of the Java Runtime only recognizes class file versions up to Y

Consult the major version number of the class file format to find out which version (X) is needed to run the jar file.

Oracle JDK 1.8.0_281

Building with Oracle JDK 1.8.0_281 succeeds, but running the resulting jar with the same JDK reports a class version mismatch error.

Exception in thread "main" java.lang.UnsupportedClassVersionError: ... has been 
compiled by a more recent version of the Java Runtime (class file version 59.0), 
this version of the Java Runtime only recognizes class file versions up to 52.0

To fix this problem, either switch to an earlier minor version of Oracle JDK 1.8 for building, or switch to Java 15 for running the jar.

JDK 11

Build will fail on JDK 11 with the error message value toList is not a member of[String]. This is because of a method from the JDK hides a scala function (


Mathematica 12.1 is incompatible for building and fails with errors similar to:

MathematicaLink.scala:377:20: overloaded method constructor Expr with alternatives

To fix this error, build with JLink.jar from up to Mathematica/Wolfram Engine 12.0, then run with Mathematica 12.1.

Mathematica 12.2 is incompatible for both building and running due to a backwards-incompatible change in the JLink native library code.

SBT Memory

If, at any time, you run into problems during the compilation process, use sbt clean for a fresh start to remove stale files. If the problems persist, use sbt clean followed by sbt reload. On a few computers you may have to edit your environment variables, e.g., ~/.bashrc or ~/.profile to include something like

export SBT_OPTS="-Xss20M -Xms8000M"

Extended build instructions and solutions to other common sbt problems:

Version conflict(s) in library dependencies

The following build warning is a version conflict in akka-http that is believed to be harmless, see

[warn] Found version conflict(s) in library dependencies; some are suspected to be binary incompatible:
[warn] * org.scala-lang.modules:scala-xml_2.12:1.1.1 is selected over 1.0.6
[warn]     +- com.typesafe.akka:akka-http-xml_2.12:10.1.8 ()     (depends on 1.1.1)
[warn]     +- org.scala-lang:scala-compiler:2.12.8               (depends on 1.0.6)

Running the Interpreter

Short solution:

sbt clean; sbt compile; scala -classpath target/Scala<version>/Classes/

Explanation: SBT creates class files in target/scala/classes, where is the Scala version specified in build.sbt (e.g. scala-2.12). This is your classpath. Note that tests are in a different location, so you won't have tests from within the interpreter.

Common Errors

The Ubuntu Encrypted Home Directory Problem

Scala doesn't play well with encrypted home directories on Ubuntu. I have no idea how to fix this. My work-around is to work from a directory outside of my home directory (e.g., I cloned the source into /var/keymaera).

Here's the sort of error text you will see when trying to sbt compile:

[info] Set current project to keymaera4 (in build file:/home/nfulton/Dropbox/research/KeYmaera4/) [info] Updating {file:/home/nfulton/Dropbox/research/KeYmaera4/}keymaera4... [info] Resolving org.fusesource.jansi#jansi;1.4 ... [info] Done updating. [info] Compiling 15 Scala sources to /home/nfulton/Dropbox/research/KeYmaera4/target/scala-2.10/classes... [error] [error] while compiling: /home/nfulton/Dropbox/research/KeYmaera4/src/main/scala/edu/cmu/cs/ls/keymaera/tests/TermTests.scala [error] during phase: jvm [error] library version: version 2.10.4 [error] compiler version: version 2.10.4 [error] reconstructed args: -bootclasspath /usr/lib/jvm/java-7-openjdk-amd64/jre/lib/resources.jar:/usr/lib/jvm/java-7-openjdk-amd64/jre/lib/rt.jar:/usr/lib/jvm/java-7-openjdk-amd64/jre/lib/sunrsasign.jar:/usr/lib/jvm/java-7-openjdk-amd64/jre/lib/jsse.jar:/usr/lib/jvm/java-7-openjdk-amd64/jre/lib/jce.jar:/usr/lib/jvm/java-7-openjdk-amd64/jre/lib/charsets.jar:/usr/lib/jvm/java-7-openjdk-amd64/jre/lib/netx.jar:/usr/lib/jvm/java-7-openjdk-amd64/jre/lib/plugin.jar:/usr/lib/jvm/java-7-openjdk-amd64/jre/lib/rhino.jar:/usr/lib/jvm/java-7-openjdk-amd64/jre/lib/jfr.jar:/usr/lib/jvm/java-7-openjdk-amd64/jre/classes:/home/nfulton/.ivy2/cache/org.scala-lang/scala-library/jars/scala-library-2.10.4.jar -classpath /home/nfulton/Dropbox/research/KeYmaera4/target/scala-2.10/classes:/home/nfulton/.ivy2/cache/org.scala-lang/scala-swing/jars/scala-swing-2.10.4.jar [error] [error] last tree to typer: TypeTree(class Byte) [error] symbol: class Byte in package scala (flags: final abstract) [error] symbol definition: final abstract class Byte extends [error] tpe: Byte [error] symbol owners: class Byte -> package scala [error] context owners: anonymous class anonfun$print -> package tests [error] [error] == Enclosing template or block == [error] [error] Template( // val <local $anonfun>: ,$print [error] "scala.runtime.AbstractFunction1", "scala.Serializable" // parents [error] ValDef( [error] private [error] "_" [error] [error] [error] ) [error] // 3 statements [error] DefDef( // final def apply(p: String [error] final [error] "apply" [error] [] [error] // 1 parameter list [error] ValDef( // p: [error] [error] "p" [error] // [error] [error] ) [error] // tree.tpe=String [error] Apply( // def print(p: String in object TermTests, tree.tpe=String [error] TermTests.this."print" // def print(p: String in object TermTests, tree.tpe=(p: [error] "p" // p:, [error] ) [error] ) [error] DefDef( // final def apply(v1: Object): Object [error] final [error] "apply" [error] [] [error] // 1 parameter list [error] ValDef( // v1: Object [error] [error] "v1" [error] // tree.tpe=Object [error] [error] ) [error] // tree.tpe=Object [error] Apply( // final def apply(p: String, tree.tpe=String [error] TermTests$$anonfun$print.this."apply" // final def apply(p: String, tree.tpe=(p: [error] Apply( // final def $asInstanceOfT0 >: ? <: ?: T0 in class Object, [error] TypeApply( // final def $asInstanceOfT0 >: ? <: ?: T0 in class Object, tree.tpe=() [error] "v1"."$asInstanceOf" // final def $asInstanceOfT0 >: ? <: ?: T0 in class Object, tree.tpe=T0 >: ? <: ?T0 [error] // [error] ) [error] Nil [error] ) [error] ) [error] ) [error] DefDef( // def ():$print [error] [error] "" [error] [] [error] List(Nil) [error] //$print [error] Block( // tree.tpe=Unit [error] Apply( // def (): scala.runtime.AbstractFunction1 in class AbstractFunction1, tree.tpe=scala.runtime.AbstractFunction1 [error] TermTests$$anonfun$print.super."" // def (): scala.runtime.AbstractFunction1 in class AbstractFunction1, tree.tpe=()scala.runtime.AbstractFunction1 [error] Nil [error] ) [error] () [error] ) [error] ) [error] ) [error] [error] == Expanded type of tree == [error] [error] TypeRef(TypeSymbol(final abstract class Byte extends )) [error] [error] uncaught exception during compilation: [error] File name too long [error] two errors found [error] (compile:compile) Compilation failed