This folder contains scripts and Vagrantfile to setup environment for CASE tools, either:

• in a dedicated Linux machine, or

• by automatically provisioning a Linux VM using VirtualBox and Vagrant.

Once setup (instructions below), all CASE tools/artifacts are installed in ~/CASE (can be overriden by specifying BASE_DIR env var; please see Vagrantfile for other environment variables that can be overriden). In the Vagrant provisioned VM, additional tools and scripts are installed in ~/bin. To run FMIDE:

fmide&

The above will launch fmide installed in ~/CASE/Sireum/bin/linux/fmide.

If you are interested to also setup FMIDE and HAMR directly in your machine running either Windows, Linux, or macOS, please see the instructions at the bottom of this page.

• Debian 11.1 [.iso]

Run the following (and subsequent commands) in your local repo's case-env directory (or download the folder here):

bash snapshot.sh
NO_SEL4_BOX=true bash case-setup.sh

See Post Setup below for additional instructions (note: replace ~/bin with the path to the bin directory in your local repo/folder case-env).

• VirtualBox 6.1.8 or above

• Vagrant 2.2.7 or above

By default, the VM is configured with 4 cores, 8GB RAM, and 64MB video memory. These settings can be changed in Vagrantfile or in the built VM after provisioning. The VM disk size is derived from the base box bento/debian-11, which is 64GB.

Run the following (and subsequent commands) in your local repo's case-env directory (or download the folder here):

• Windows

  setup.bat

• macOS/Linux

  bash setup.sh

Note that the setup is fully automatic and it might take around 2 hours or so to complete (dependent on network speed). During the setup process, there is no need to interact with Vagrant or the VirtualBox VM until the process is done. A successful setup is typically indicated with a X11 GUI login screen being launched.

Once Vagrant finished setting up the VM with a X11 GUI login screen presented, log in using vagrant for both the username and the password in the Linux VM login GUI.

Then, optionally, logout/shutdown the VM and take a VM snapshot (to allow for rolling back later) and re-start it from VirtualBox.

If there is an error when running the setup script (e.g., internet connection is down during provisioning), destroy the VM before re-launching the setup script. To destroy the VM:

vagrant destroy

See Post Setup below for additional instructions.

• To update FMIDE, simply (re-)run the following in the VM:

  $SIREUM_HOME/bin/install/fmide.cmd ( fixed | latest )

• To update Sireum:

  ~/bin/sireum-install.sh <INIT_RELEASE> <COMMIT>

  where:

  • <INIT_RELEASE> is SIREUM_INIT_V in case-setup.sh (use latest for the latest version)

  • <COMMIT> is SIREUM_V in case-setup.sh (use master for the latest version)

  If the installation somehow did not finish (e.g., due to a network issue), remove the problematic file in Sireum's cache directory (~/Downloads/sireum) and re-run the above.

• To update seL4 and friends (cache, etc.):

  bash ~/bin/sel4-cache.sh <SEL4-MANIFEST-COMMIT> # desired version as commit SHA of https://github.com/seL4/sel4test-manifest
  bash ~/bin/camkes-cache.sh <CAMKES_MANIFEST_COMMIT> # desired version as commit SHA of https://github.com/seL4/camkes-manifest

• To install the IntelliJ-based Sireum IVE (for HAMR Slang component development, etc.):

  $SIREUM_HOME/bin/build.cmd setup

  Then, to launch it:

  $SIREUM_HOME/bin/linux/idea/bin/IVE.sh&

• To install CLion C/C++ IDE (for browsing HAMR generated C code, etc.; license required/free 30-day evaluation):

  $SIREUM_HOME/bin/install/clion.cmd

  Then, to launch it:

  $SIREUM_HOME/bin/linux/clion/bin/clion.sh&

• To install CompCert (including Coq):

  $SIREUM_HOME/bin/install/compcert.cmd

• Windows:

  git clone https://github.com/sireum/kekinian Sireum
  cd Sireum
  git checkout <commit> & REM^; SHA commit of https://github.com/sireum/kekinian, see SIREUM_V in case-setup.sh; optional step
  git submodule update --init --recursive
  bin\build.cmd setup
  bin\install\fmide.cmd latest
  start /B bin\win\fmide\fmide.exe

• Linux:

  git clone https://github.com/sireum/kekinian Sireum
  cd Sireum
  git checkout <commit> # SHA commit of https://github.com/sireum/kekinian, see SIREUM_V in case-setup.sh; optional step
  git submodule update --init --recursive
  bin/build.cmd setup
  bin/install/fmide.cmd latest
  bin/linux/fmide/fmide&

• macOS:

  git clone https://github.com/sireum/kekinian Sireum
  cd Sireum
  git checkout <commit> # SHA commit of https://github.com/sireum/kekinian, see SIREUM_V in case-setup.sh; optional step
  git submodule update --init --recursive
  bin/build.cmd setup
  bin/install/fmide.cmd latest
  open bin/mac/fmide.app