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 latest packaged binary release, (or using the installer scripts for older releases). The package binary release includes a Sireum native executable that voids JVM boot-up time.
Download
Packaged Binaries
Latest Release
https://github.com/sireum/kekinian/releases/tag/4.20241122.a3b711d
VSCodium-based IVE
DISTRO=codeive sh -c "$(curl -fsSL https://github.com/sireum/kekinian/releases/download/4.20241122.a3b711d/install.cmd)"
cmd /V/C "set DISTRO=codeive&& curl -JLOs https://github.com/sireum/kekinian/releases/download/4.20241122.a3b711d/install.cmd && install.cmd && del /q/f install.cmd"
Both VSCodium-based and IntelliJ-based IVEs
DISTRO=ive sh -c "$(curl -fsSL https://github.com/sireum/kekinian/releases/download/4.20241122.a3b711d/install.cmd)"
cmd /V/C "set DISTRO=ive&& curl -JLOs https://github.com/sireum/kekinian/releases/download/4.20241122.a3b711d/install.cmd && install.cmd && del /q/f install.cmd"
Latest Development Build
https://github.com/sireum/kekinian/releases/tag/dev
VSCodium-based IVE
DISTRO=codeive sh -c "$(curl -fsSL https://github.com/sireum/kekinian/releases/download/dev/install.cmd)"
cmd /V/C "set DISTRO=codeive&& curl -JLOs https://github.com/sireum/kekinian/releases/download/dev/install.cmd && install.cmd && del /q/f install.cmd"
Both VSCodium-based and IntelliJ-based IVEs
DISTRO=ive sh -c "$(curl -fsSL https://github.com/sireum/kekinian/releases/download/dev/install.cmd)"
cmd /V/C "set DISTRO=ive&& curl -JLOs https://github.com/sireum/kekinian/releases/download/dev/install.cmd && install.cmd && del /q/f install.cmd"
The sireum-ive
binary distribution files include both the IntelliJ-based and the VSCodium-based IVE,
while the sireum-codeive
only includes the latter.
The sireum-cli
files are compressed native executables built for specific platforms.
Both sireum-ive
and sireum-codeive
include the sireum-cli
native executable.
Notes
-
On Linux that enables
binfmt_misc
to automatically launch Windows executables using WINE (e.g., Ubuntu desktops), Sireum performs better ifbinfmt_misc
is configured to enable the αcτµαlly pδrταblε εxεcµταblε (APE) Loader:sudo wget -O /usr/bin/ape https://cosmo.zip/pub/cosmos/bin/ape-$(uname -m).elf sudo chmod +x /usr/bin/ape sudo sh -c "echo ':APE:M::MZqFpD::/usr/bin/ape:' >/proc/sys/fs/binfmt_misc/register" sudo sh -c "echo ':APE-jart:M::jartsr::/usr/bin/ape:' >/proc/sys/fs/binfmt_misc/register"
or, by disabling
binfmt_misc
completely:sudo sh -c 'echo -1 > /proc/sys/fs/binfmt_misc/cli' sudo sh -c 'echo -1 > /proc/sys/fs/binfmt_misc/status'
-
On Windows WSL, you need to disable
binfmt_misc
interop:sudo sh -c "echo -1 >/proc/sys/fs/binfmt_misc/WSLInterop"
Set the SIREUM_HOME
env var to the Sireum installation path, then proceed to Using Sireum.
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 directory).
To use a specific version of Sireum, set SIREUM_V
with a release version
listed at https://github.com/sireum/kekinian/releases in the command lines below.
Latest Release
(DIR=Sireum && export SIREUM_V=4.20241122.a3b711d && 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.20241122.a3b711d&& (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"
Set the SIREUM_HOME
env var to the Sireum installation path, then proceed to Using Sireum.
Please see the notes section if the installation failed.
For K-State CIS 301 & 706/801, Fall 2024
(DIR=Sireum && export SIREUM_V=4.20241017.f6e1eff && 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.20241017.f6e1eff&& (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"
Set the SIREUM_HOME
env var to the Sireum installation path, then proceed to Using Sireum.
Please see the notes section if the installation failed.
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"
Set the SIREUM_HOME
env var to the Sireum installation path, then proceed to Using Sireum.
Please see the notes section if the installation failed.
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.
If the installation keeps failing, please use the packaged binaries described above.
Moreover, please take a look at the packaged binaries notes section.
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.
If the installation keeps failing, please use the packaged binaries described above.
Moreover, please take a look at the packaged binaries notes section.
Vagrant Linux Virtual Machine (VM)
A Linux VM containing a Sireum source build can be provisioned using Vagrant and Sireum’s Vagrantfile:
https://github.com/sireum/resources/tree/master/vagrant
You can download the contents of the directory by using the following link: https://downgit.github.io/#/home?url=https://github.com/sireum/resources/tree/master/vagrant
Installing FMIDE+HAMR
"${SIREUM_HOME}/bin/install/fmide.cmd"
"%SIREUM_HOME%\bin\install\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/rustrover.cmd" # https://www.jetbrains.com/rust/
"%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\graal.cmd" & :: https://www.graalvm.org/
"%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\rustrover.cmd" & :: https://www.jetbrains.com/rust/
Using Sireum
To launch the Sireum CLI, IVE, or FMIDE+HAMR:
"${SIREUM_HOME}/bin/sireum" # CLI
open "${SIREUM_HOME}/bin/mac/idea/IVE.app" # IntelliJ-based IVE
open "${SIREUM_HOME}/bin/mac/vscodium/CodeIVE.app" # VSCodium-based IVE
"${SIREUM_HOME}/bin/sireum" # CLI
open "${SIREUM_HOME}/bin/mac/idea/IVE.app" # IntelliJ-based IVE
open "${SIREUM_HOME}/bin/mac/vscodium/CodeIVE.app" # VSCodium-based 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" # IntelliJ-based IVE
"${SIREUM_HOME}/bin/linux/vscodium/bin/codeive" # VSCodium-based 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" # IntelliJ-based IVE
"${SIREUM_HOME}/bin/linux/arm/vscodium/bin/codeive" # VSCodium-based IVE
"%SIREUM_HOME%\bin\sireum.bat" & :: CLI
"%SIREUM_HOME%\bin\win\idea\bin\IVE.exe" & :: IntelliJ-based IVE
"%SIREUM_HOME%\bin\win\vscodium\bin\codeive.cmd" & :: VSCodium-based IVE
start /B "%SIREUM_HOME%\bin\win\fmide\fmide.exe" & :: FMIDE+HAMR (see above for installation)
%SIREUM_HOME%\bin\sireum.bat" & :: CLI
%SIREUM_HOME%\bin\win\idea\bin\IVE.exe" & :: IntelliJ-based IVE
%SIREUM_HOME%\bin\win\vscodium\bin\codeive.cmd" & :: VSCodium-based IVE
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
logika-examples/bin/verify.cmd
"${SIREUM_HOME}/bin/sireum" proyek ive logika-examples # For IntelliJ-based IVE
"${SIREUM_HOME}/bin/sireum" proyek export logika-examples # For VSCodium-based IVE
git clone https://github.com/sireum/logika-examples
logika-examples\bin\verify.cmd
"%SIREUM_HOME%\bin\sireum.bat" proyek ive logika-examples & :: For IntelliJ-based IVE
"%SIREUM_HOME%\bin\sireum.bat" proyek export logika-examples & :: For VSCodium-based IVE
Then, open the logika-examples
directory in IVE/CodeIVE 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. The packaged binary releases include natively compiled Sireum. For other installation methods, below is the instruction on how to compile Sireum to native.
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.bat" --native
call "C:\Program Files (x86)\Microsoft Visual Studio\2019\Community\VC\Auxiliary\Build\vcvars64.bat"
"%SIREUM_HOME%\bin\sireum.bat" --native
call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Auxiliary\Build\vcvars64.bat"
"%SIREUM_HOME%\bin\sireum.bat" --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.