Getting Started

Sireum can be retrieved using installers, packaged binaries, or from source. The main advantage of using the source distribution is that updates can be done incrementally while the binary distribution requires complete re-installation. On the other hand, source distribution requires more setup. The source distribution should be used by Sireum developers and code contributors, while users are recommended to use the installer scripts, or download from Sireum’s GitHub Releases.

Note that, the latest pre-built binary installed by the scripts might be behind the latest source commit, but it does not require source compilation (faster). The installer’s pre-built binary is more frequently updated than the GitHub release binary distribution, and it is what is used to build Sireum itself at every commit.

Download

Using Installer Scripts

You can set up Sireum by downloading and running its initialization script as follows (curl is required; DIR can be set to another path for Sireum home bin directory, best if the path does not contain any whitespace).

Latest Release

(DIR=Sireum && export SIREUM_V=4.20240814.304e87b && rm -fR $DIR && mkdir -p $DIR/bin && cd $DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$SIREUM_V/bin/init.sh && bash init.sh)

cmd /V /C "set DIR=Sireum&& set SIREUM_V=4.20240814.304e87b&& (if exist !DIR! rd /S /Q !DIR!) && md !DIR!\bin && cd !DIR!\bin && curl -JLso init.bat https://raw.githubusercontent.com/sireum/kekinian/!SIREUM_V!/bin/init.bat && init.bat"

For K-State CIS 301 & 706/801, Fall 2024

(DIR=Sireum && export SIREUM_V=4.20240814.304e87b && rm -fR $DIR && mkdir -p $DIR/bin && cd $DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$SIREUM_V/bin/init.sh && bash init.sh)

cmd /V /C "set DIR=Sireum&& set SIREUM_V=4.20240814.304e87b&& (if exist !DIR! rd /S /Q !DIR!) && md !DIR!\bin && cd !DIR!\bin && curl -JLso init.bat https://raw.githubusercontent.com/sireum/kekinian/!SIREUM_V!/bin/init.bat && init.bat"

Latest Development Build

(DIR=Sireum && export SIREUM_V=master && rm -fR $DIR && mkdir -p $DIR/bin && cd $DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$SIREUM_V/bin/init.sh && bash init.sh)

cmd /V /C "set DIR=Sireum&& set SIREUM_V=master&& (if exist !DIR! rd /S /Q !DIR!) && md !DIR!\bin && cd !DIR!\bin && curl -JLso init.bat https://raw.githubusercontent.com/sireum/kekinian/!SIREUM_V!/bin/init.bat && init.bat"

Notes

Note that in the case where some files are not downloaded properly (e.g., due to network issues), you can delete the offending file(s) in the sireum folder of your user home’s Downloads folder (or, entirely delete the Downloads sireum folder). Also note that this installation approach is using GitHub anonymous connection, thus subject to rate limiting. To avoid the limit, set the GITHUB_TOKEN environment variable to one of your GitHub tokens.

To use a specific version of Sireum, replace master with a release version (>= 4.202208*) listed at https://github.com/sireum/kekinian/releases in the command line above.

Set the SIREUM_HOME env var to the Sireum installation path, then proceed to Using Sireum.

Packaged Binaries

The packaged binary distribution files are available at: https://github.com/sireum/kekinian/releases

Sireum binary distribution files are 7z self-extracting archives (SFX) with command-line installers to (optionally) configure where Sireum should be installed. The files can also be extracted using a program capable of uncompressing 7z archive such as 7-zip.

On macOS, you might need to “un-quarantine” the downloaded self-extracting executable before running it:

xattr -rd com.apple.quarantine <PATH-TO>/sireum-mac-*.7z.sfx

Set the SIREUM_HOME env var to the Sireum installation path, then proceed to Using Sireum.

Git Source Distribution

Requirements

macOS: curl and git
Linux (amd64, aarch64): curl and git
Windows 10, either:
- Using a NTFS partition with Developer Mode enabled, long-path enabled, and git (Git For Windows, MSYS2, or Cygwin) with its core.longpaths config set to true; or
- WSL2 (Linux requirements apply)

Note that Sireum stores small, pre-built binary dependencies in its repositories. Virus analysis results are provided in the respective submodule repositories for macOS, Linux, and Windows.

Setup

In a console terminal:

git clone --recursive https://github.com/sireum/kekinian Sireum
Sireum/bin/build.cmd setup  # for non-POSIX shell, prefix with sh

git clone --recursive https://github.com/sireum/kekinian Sireum
Sireum\bin\build.cmd setup

The above install Sireum command-line interface (CLI) and its IntelliJ-based Integrated Verification Environment (IVE), as well as their dependencies. Set the SIREUM_HOME env var to the Sireum path above.

To update later on, simply do a git pull --recurse-submodules and re-run build.cmd. Note that after a setup update, it is best to invalidate IntelliJ’s cache files and restart by using IntelliJ’s File -> Invalidate Caches... menu item and select Clear all file system cache and Local History.

Notes

Occasionally, there might be new API used in build.cmd that is available in the pre-built binary online but not in your local copy. This issue happens because build.cmd uses Sireum itself, hence it is a bootstrapping issue. This issue typically manifests by build.cmd failing to compile/execute due to missing methods/classes. In that case, first delete your local sireum.jar (and build.cmd.com, if any) in the bin directory and then re-run build.cmd setup.
If building Sireum somehow failed still, try cleaning the repo:
${SIREUM_HOME}/bin/clean.sh
%SIREUM_HOME%\bin\clean.bat
The clean scripts remove all Sireum-related cache directories and revert any changes and delete new files in the local git repository.

After cleaning, re-run git pull --recurse-submodules (possibly multiple times until it reaches a good fix-point where git status indicates that its working tree is clean) and build.cmd setup.

If all else fails, try recursively re-clone Sireum.

Installing FMIDE+HAMR

${SIREUM_HOME}/bin/install/fmide.cmd

%SIREUM_HOME%\bin\sireum\fmide.cmd

Installing CLion, Coq, Isabelle, CompCert, and Other Tools

${SIREUM_HOME}/bin/install/acl2.cmd             # https://www.cs.utexas.edu/users/moore/acl2/
${SIREUM_HOME}/bin/install/alt-ergo.cmd         # https://alt-ergo.ocamlpro.com/
${SIREUM_HOME}/bin/install/antlrworks.cmd       # https://slang.sireum.org/tools/pg/
${SIREUM_HOME}/bin/install/brave.cmd            # https://brave.com/
${SIREUM_HOME}/bin/install/clion.cmd            # https://www.jetbrains.com/clion/
${SIREUM_HOME}/bin/install/compcert.cmd         # https://compcert.org/
${SIREUM_HOME}/bin/install/coq.cmd              # https://coq.inria.fr/
${SIREUM_HOME}/bin/install/graal.cmd            # https://www.oracle.com/java/graalvm/
${SIREUM_HOME}/bin/install/graal-openjdk.cmd    # https://www.graalvm.org/
${SIREUM_HOME}/bin/install/isabelle.cmd         # https://isabelle.in.tum.de/
${SIREUM_HOME}/bin/install/rust.cmd             # https://www.rust-lang.org/
${SIREUM_HOME}/bin/install/vscodium.cmd         # https://vscodium.com/

%SIREUM_HOME%\bin\sireum\antlrworks.cmd         & :: https://slang.sireum.org/tools/pg/
%SIREUM_HOME%\bin\sireum\brave.cmd              & :: https://brave.com/
%SIREUM_HOME%\bin\sireum\clion.cmd              & :: https://www.jetbrains.com/clion/
%SIREUM_HOME%\bin\sireum\graal.cmd              & :: https://www.graalvm.org/
%SIREUM_HOME%\bin\sireum\graal-openjdk.cmd      & :: https://www.graalvm.org/
%SIREUM_HOME%\bin\sireum\isabelle.cmd           & :: https://isabelle.in.tum.de/
%SIREUM_HOME%\bin\sireum\rust.cmd               & :: https://www.rust-lang.org/
%SIREUM_HOME%\bin\sireum\vscodium.cmd           & :: https://vscodium.com/

Using Sireum

To launch the Sireum CLI, IVE, or FMIDE+HAMR:

${SIREUM_HOME}/bin/sireum                      # CLI
open ${SIREUM_HOME}/bin/mac/idea/IVE.app       # IVE
open ${SIREUM_HOME}/bin/mac/fmide.app          # FMIDE+HAMR (see above for installation)

${SIREUM_HOME}/bin/sireum                      # CLI
${SIREUM_HOME}/bin/linux/idea/bin/IVE.sh       # IVE
${SIREUM_HOME}/bin/linux/fmide/fmide           # FMIDE+HAMR (see above for installation)

${SIREUM_HOME}/bin/sireum                      # CLI
${SIREUM_HOME}/bin/linux/arm/idea/bin/IVE.sh   # IVE

%SIREUM_HOME%\bin\sireum.bat                   & :: CLI
%SIREUM_HOME%\bin\win\idea\bin\IVE.exe         & :: IVE
start /B %SIREUM_HOME%\bin\win\fmide\fmide.exe & :: FMIDE+HAMR (see above for installation)

It is best to remove the JAVA_HOME environment variable before launching IVE.

To try out your installation:

git clone https://github.com/sireum/logika-examples
${SIREUM_HOME}/bin/sireum proyek ive logika-examples

git clone https://github.com/sireum/logika-examples
%SIREUM_HOME%\bin\sireum.bat proyek ive logika-examples

Then, open the logika-examples directory in IVE and see Logika in action on some of the .sc example files.

See Sireum Documentation for more information.

Native Executable

It is recommended to compile Sireum (and Slash build scripts) to native in certain situations in order to avoid JVM boot up time.

First, install GraalVM native-image’s prerequisites (note: native-image for Windows requires Visual Studio Community/Enterprise); then, to build Sireum native executable:

${SIREUM_HOME}/bin/sireum --native

call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvars64.bat"
%SIREUM_HOME%\bin\sireum --native

call "C:\Program Files (x86)\Microsoft Visual Studio\2019\Community\VC\Auxiliary\Build\vcvars64.bat"
%SIREUM_HOME%\bin\sireum --native

call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Auxiliary\Build\vcvars64.bat"
%SIREUM_HOME%\bin\sireum --native

The compiled native binary is located at:

${SIREUM_HOME}/bin/mac/sireum

${SIREUM_HOME}/bin/linux/sireum

${SIREUM_HOME}/bin/linux/arm/sireum

%SIREUM_HOME%\bin\win\sireum.exe

Note that once the native version is available (and has a newer timestamp), sireum and sireum.bat in bin call the native version.