Development Environment Setup - LS-Lab/KeYmaeraX-release Wiki
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 Development Environment
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
sbt compile
"File name too long" when running 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.