Getting Started
Sireum is available as pre-built binaries/installers 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
Binary Distributions
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):
(DIR=Sireum && 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"
Note: Windows 11 users should download from GitHub Releases
Note that this installation approach is using GitHub anonymous connection, thus subject to rate limiting.
To remove 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.202211*) or
commit tip SHA (without the 4.
prefix) listed at https://github.com/sireum/init/releases
in the command line above.
GitHub Releases
The 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).
On macOS, you might need to “un-quarantine” the self-extracting executable:
xattr -rd com.apple.quarantine <PATH-TO>/sireum-dev-mac.sfx
If you want to ensure that the downloaded files are genuine, download the appropriate Minisign signature file for the specific platform, then run:
minisign -P RWShRZe/1tMRHAcQ2162Wq5FhU2ptktJdQxzUxvK0MwVjDYRC4JY87Fb -VHm <installer-file>
Set the SIREUM_HOME
env var to the Sireum installation path, then proceed to Using Sireum.
Git Source Distribution
Requirements
-
macOS:
curl
andgit
-
Linux (amd64, aarch64):
curl
andgit
-
Windows 10, either:
-
Using a NTFS partition with Developer Mode enabled, long-path enabled, and
git
(Git For Windows, MSYS2, or Cygwin) with itscore.longpaths
config set totrue
; 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 becausebuild.cmd
uses Sireum itself, hence it is a bootstrapping issue. This issue typically manifests bybuild.cmd
failing to compile/execute due to missing methods/classes. In that case, first delete your localsireum.jar
(andbuild.cmd.com
, if any) in thebin
directory and then re-runbuild.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 wheregit status
indicates that its working tree is clean) andbuild.cmd setup
.If all else fails, try recursively re-clone Sireum.
Native Executable
It is recommended to compile Sireum (and Slash build scripts) to native as it removes 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/build.cmd native
call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvars64.bat"
%SIREUM_HOME%\bin\build.cmd native
call "C:\Program Files (x86)\Microsoft Visual Studio\2019\Community\VC\Auxiliary\Build\vcvars64.bat"
%SIREUM_HOME%\bin\build.cmd native
call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Auxiliary\Build\vcvars64.bat"
%SIREUM_HOME%\bin\build.cmd native
The compiled native binary is located at:
${SIREUM_HOME}/bin/mac/sireum
${SIREUM_HOME}/bin/linux/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.
This is also similar for build.cmd
in bin
.
Remote Development Setup (Experimental)
IntelliJ Ultimate now supports remote development from a Linux server reachable using ssh, and Sireum IVE can be set up on top of it:
-
Use JetBrains Gateway to install an IntelliJ Ultimate instance in the Linux server.
Note that the supported instance version of IntelliJ should be compatible with what is listed in version.properties with property key
org.sireum.version.idea
property key). If the listed property value is20XX.Y.Z
or20XX.Y
, then you need to IntelliJ Ultimate build that starts withXXY
. -
Connect to the server and install Sireum:
git clone --recursive https://github.com/sireum/kekinian Sireum Sireum/bin/build.cmd setup-server
-
Open the
Sireum
path above with JetBrains Gateway/Client.
Installing FMIDE+HAMR
${SIREUM_HOME}/bin/install/fmide.cmd
%SIREUM_HOME%\bin\sireum\fmide.cmd
Installing CLion, Coq, Isabelle 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/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.graalvm.org/
${SIREUM_HOME}/bin/install/isabelle.cmd # https://isabelle.in.tum.de/
%SIREUM_HOME%\bin\sireum\antlrworks.cmd & :: https://slang.sireum.org/tools/pg/
%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\isabelle.cmd & :: https://isabelle.in.tum.de/
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
${SIREUM_HOME}/bin/sireum # CLI
${SIREUM_HOME}/bin/linux/idea/bin/IVE.sh # IVE
${SIREUM_HOME}/bin/linux/fmide/fmide # FMIDE+HAMR
${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 Sireum Documentation for more information.