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 default.properties). If those are not suitable for your setup, create a file local.properties in the same directory as default.properties (project root) and provide the location of JLink.jar with a property

mathematica.jlink.path=YOUR_LOCAL_PATH_TO_JLINKJAR

Several example paths are listed in Readme.md

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 libuuid.so using find / -type f -iname "libuuid*", for example in /lib/x86_64-linux-gnu/libuuid.so.1.3.0.
2. Then start KeYmaera X as follows: export LD_PRELOAD={path to libuuid.so}; java -jar keymaerax.jar

Development Environment Setup

1. Install Java JDK 1.8 from http://www.java.com/getjava/ or from https://openjdk.java.net/

2. Install the Scala Build Tool (SBT) Version 1.3.7 on your system. It is available here: http://www.scala-sbt.org/ If you are using IntelliJ, this comes with the Scala plugin. http://www.scala-sbt.org/release/docs/Getting-Started/Setup.html

3. Clone KeYmaera X from github.com/LS-Lab/KeYmaeraX-Release 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 github.com/LS-Lab/KeYmaeraX-projects 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 edu.cmu.cs.ls.keymaerax.btactics.DerivedAxiomsTests"
   

7. Optional: test your installation by running the full regression test suite:

   sbt test -l edu.cmu.cs.ls.keymaerax.tags.IgnoreInBuildTest

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 http://keymaeraX.org/scaladoc while local documentation will be generated in the directory target/scala-2.12/unidoc with:

sbt unidoc

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 edu.cmu.cs.ls.keymaerax.tags.IgnoreInBuildTest 

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

sbt "testOnly -- -l edu.cmu.cs.ls.keymaerax.tags.SlowTest -l edu.cmu.cs.ls.keymaerax.tags.ExtremeTest -l edu.cmu.cs.ls.keymaerax.tags.IgnoreInBuildTest -l edu.cmu.cs.ls.keymaerax.tags.TodoTest"

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

sbt "testOnly -- -n edu.cmu.cs.ls.keymaerax.tags.SummaryTest -n edu.cmu.cs.ls.keymaerax.tags.CheckinTest"

Selectively running individual test cases within the sbt interactive mode:

sbt
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: https://github.com/LS-Lab/KeYmaeraX-Release/wiki/How-to-Add-Tests http://www.scalatest.org/user_guide

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.

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.

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.

Build will fail on JDK 11 with the error message value toList is not a member of java.util.stream.Stream[String]. This is because of a method from the JDK hides a scala function (https://github.com/scala/bug/issues/11125).

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.

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:

https://github.com/LS-Lab/KeYmaeraX-Release/wiki/Building-Instructions

The following build warning is a version conflict in akka-http that is believed to be harmless, see https://github.com/akka/akka-http/issues/2055.

[warn] Found version conflict(s) in library dependencies; some are suspected to be binary incompatible:
[warn] 
[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)

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.

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>: , tree.tpe=edu.cmu.cs.ls.keymaera.tests.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: edu.cmu.cs.ls.keymaera.core.ProofNode): String [error] final [error] "apply" [error] [] [error] // 1 parameter list [error] ValDef( // p: edu.cmu.cs.ls.keymaera.core.ProofNode [error] [error] "p" [error] // tree.tpe=edu.cmu.cs.ls.keymaera.core.ProofNode [error] [error] ) [error] // tree.tpe=String [error] Apply( // def print(p: edu.cmu.cs.ls.keymaera.core.ProofNode): String in object TermTests, tree.tpe=String [error] TermTests.this."print" // def print(p: edu.cmu.cs.ls.keymaera.core.ProofNode): String in object TermTests, tree.tpe=(p: edu.cmu.cs.ls.keymaera.core.ProofNode)String [error] "p" // p: edu.cmu.cs.ls.keymaera.core.ProofNode, tree.tpe=edu.cmu.cs.ls.keymaera.core.ProofNode [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: edu.cmu.cs.ls.keymaera.core.ProofNode): String, tree.tpe=String [error] TermTests$$anonfun$print.this."apply" // final def apply(p: edu.cmu.cs.ls.keymaera.core.ProofNode): String, tree.tpe=(p: edu.cmu.cs.ls.keymaera.core.ProofNode)String [error] Apply( // final def $asInstanceOfT0 >: ? <: ?: T0 in class Object, tree.tpe=edu.cmu.cs.ls.keymaera.core.ProofNode [error] TypeApply( // final def $asInstanceOfT0 >: ? <: ?: T0 in class Object, tree.tpe=()edu.cmu.cs.ls.keymaera.core.ProofNode [error] "v1"."$asInstanceOf" // final def $asInstanceOfT0 >: ? <: ?: T0 in class Object, tree.tpe=T0 >: ? <: ?T0 [error] // tree.tpe=edu.cmu.cs.ls.keymaera.core.ProofNode [error] ) [error] Nil [error] ) [error] ) [error] ) [error] DefDef( // def (): edu.cmu.cs.ls.keymaera.tests.anonfun$print [error] [error] "" [error] [] [error] List(Nil) [error] // tree.tpe=edu.cmu.cs.ls.keymaera.tests.anonfun$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: java.io.IOException [error] File name too long [error] two errors found [error] (compile:compile) Compilation failed