Development Environment Setup

Platform-Agnostic Instructions

First, install all dependencies. A development environment for KeYmaera X depends on:

• The JRE
• The JDK
• Scala
• The Scala Build Tool (SBT), available here: http://www.scala-sbt.org/
• Mathematica

Second, you will need to set your JLINK_JAR_LOCATION environmental variable to the location of Mathematica's JLink.jar.

Third, if you are not using a Mac or if you installed Mathematica to a non-default location, copy default.properties to local.properties and then modify the path in local.properties

• On Linux use mathematica.jlink.path=/usr/local/Wolfram/Mathematica/10.0/SystemFiles/Links/JLink/JLink.jar or similar.
• On MacOS, use mathematica.jlink.path=/Applications/Mathematica.app/Contents/SystemFiles/Links/JLink/JLink.jar or similar.
• On Windows, use mathematica.jlink.path=C:/Program Files/Wolfram Research/Mathematica/13.0/SystemFiles/Links/Jlink/Jlink.jar or similar.

After installing all dependencies and setting your environmental variable and local.properties, we strongly recommend installing the IntelliJ IDE and its Scala plugin.

Ubuntu-specific Instructions

First, install the JRE, the JDK, Scala, and the Scala Build Tool (SBT)

sudo apt-get install default-jre default-jdk scala
echo "deb https://dl.bintray.com/sbt/debian /" | sudo tee -a /etc/apt/sources.list.d/sbt.list;
sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv 642AC823;
sudo apt-get update;
sudo apt-get install sbt

Second, Download, install, and activate Mathematica. (CMU students, staff, and faculty may download Mathematica from CMU.)

Third, set the JLINK_JAR_LOCATION environmental variable in your .bashrc file and then source your .bashrc. To do so, add the line export JLINK_JAR_LOCATION="/usr/local/Wolfram/Mathematica/10.0/SystemFiles/Links/JLink/JLink.jar" to your .bashrc and then run . .bashrc

Fourth, create a file called local.properties and on Linux insert mathematica.jlink.path=/usr/local/Wolfram/Mathematica/10.0/SystemFiles/Links/JLink/JLink.jar or similar.

To test your installation, from the root of the repository (the directory containing build.sbt), run sbt compile

IntelliJ Idea 2022.1 Development Environment

• Download and install IntelliJ
• Start IntelliJ
• On the start screen: click Plugins and install the Scala plugin (restart the IDE)

Project setup

• When the start screen is visible: click File->New->Project from Existing Sources (do not use New Project from the start screen)
• Select the directory with the KeYmaeraX-release sources
• Select Import project from external model
• Select sbt from the list
• Pick any project name, e.g., KeYmaeraX-release
• Select a JDK version 1.8
  • also select 1.8 in Intelli/J Settings -> Build, Execution, Deployment -> Compiler -> Scala Compile Server -> JVM -> JDK
  • The setting is incorrect when errors such as scalac: Error: java.lang.RuntimeException: /packages cannot be represented as URI occur.
• Click Create

IntelliJ IDEA Development Environment (Old)

If you choose to use the IntelliJ IDEA development environment, install it:

• Install IntelliJ IDEA
• Install the Scala plugin for IntelliJ (the IntelliJ installer will ask you if you want to do this)

Project Setup

• Make sure you have defined the JLINK_JAR_LOCATION environment variable (see FAQ).
• Create a new Scala project, backed by SBT (File->New->Project... on the dialog select Scala->sbt then follow the dialog instructions)
• Select a JDK as your project SDK, add a new one if not previously added
• Check update automatically (not checked by default), so that updates to build.sbt are reflected automatically in the project. You may also want to check the "Download and compile sources" options.
• If the bundled version of sbt is not working for you, you can specify your own version here.

Create a new run configuration of type Application for the KeYmaera X Web UI.

• Main class: edu.cmu.cs.ls.keymaerax.hydra.NonSSLBoot
• Set the working directory to the project path
• Use the classpath of your project module
• Check "Single instance only"
• Make sure the JVM option -Xss20M is included in the run configuration.

Test Cases

• Right click on project folder keymaerax-webui/src/test to mark this directory as Test Sources Root.
• Make sure the JVM option -Xss20M is included in the run configuration.
• Right click on the test folder to run all its ScalaTests.

Tagged Test Suite: Run Configurations Drop-down in Toolbar -> Edit Configurations -> Add Configuration (ScalaTest) -> Select "All in package" for Test Kind -> Under "Test options" enter: -n edu.cmu.cs.ls.keymaerax.tags.CheckinTest -n edu.cmu.cs.ls.keymaerax.tags.SummaryTest -l edu.cmu.cs.ls.keymaerax.tags.ObsoleteTest (or any other string from TestTags.scala) -> Select "keymaerax" as SDK and classpath of module -> Apply/OK

Enabling logging

• Run with -Dlog4j.<level> where <level> is replaced with the desired log level (fatal, error, warn, info, debug, all)

IntelliJ FAQ

If, at any time, you run into problems during the compilation process in IntelliJ, check the File->Project Structure->Modules->core->Dependencies to make sure the appropriate files such as SBT: unmanaged-jars are checked. This is necessary for IntelliJ to find JLink.jar. IntelliJ keeps forgetting about it, so you may have to check repeatedly. If the problems persist, do File->Invalidate Caches / Restart.

Common Errors

"File name too long" when running sbt compile

This is a known issue that occurs when trying to run sbt compile on projects with large file names on a project located in an encrypted home directory. The easiest work-around is to create a new user account that does not have an encrypted home directory, or else place your KeYmaera X project somewhere outside of your home directory.

Something about JLINK_JAR_LOCATION

Make sure you've set the JLINK_JAR_LOCATION environmental variable. If you have set this variable but problems persist, try logging out and logging back in to ensure that your .bashrc gets sourced.