LIVE features mimic the typical features one would expect in a modern IDE.
Syntax highlighting and error/warning reporting similar to most Integrated Development Environments (IDEs) for popular programming languages.
Convenient keyboard shortcuts for inserting logical symbols that works for any editor file types.
Verification engine running in the background to check proofs as you type.
Can be used in conjunction with IntelliJ’s
.sc files) or its Scala editor (
.scala files) to benefit from IntelliJ IDE features
(e.g., the screenshot above illustrates how LIVE works with the Scala Worksheet).
It is recommended to use the sireum-ive distribution, which includes LIVE; if you do skip to Optional Settings.
Alternatively, you can install the Sireum v3 IntelliJ plugin in your IntelliJ installation (see Installing, Updating and Uninstalling Repository Plugins).
LIVE requires IntelliJ (15 or above; it is recommended to install the Scala plugin); please take a look at its system requirements and follow the installation instructions for your respective operating system.
In Windows and some Linux distributions, you need to add
-Dfile.encoding=UTF-8 in IntelliJ
This step is optional as opening any Logika files retrieved during LIVE Examples will cause IntelliJ to suggest you to install the Sireum v3 IntelliJ plugin. Thus, you can choose to skip directly to LIVE Examples (but you might want to take a look at Optional Settings first).
As a reference, below are the instructions to manually install LIVE from JetBrains’ plugin repositories.
First, open IntelliJ’s
⌘, in macOS):
sireum in the search text field of the newly displayed window.
Install and then click
Once restarted, LIVE adds a
Logika sub-menu under the
IntelliJ Tools menu.
By default, LIVE is configured to also work with
.sc files; Scala Worksheet is an excellent tool for learning Scala.
.sc files allow one to test and prove Logika programs using the same editor.
You can configure LIVE to also work with
.scala files to
benefit from, for example, its code-folding feature, which is handy for hiding
proof claims that have been verified.
Logika does not accept margin characters that can be stripped for its proof statements that use multi-line strings. By default, IntelliJ is configured to insert margin characters and strip/insert margin on copy and paste. It is best to disable these features when working with Logika (see Working with Strings in Scala).
The IntelliJ Scala plugin defines some code inspections that are beneficial when
programming Scala programs. A couple of these code inspections produce spurious
warnings for Logika programs.
Thus, it is best to disable them when working on Logika programs.
The two code inspections can be found in the
IntelliJ’s Editor Inspections
Comparing unrelated types:
Logika uses arbitrary-precision integers (
scala.BigInt, which is aliased as
in Logika) instead of using 32-bit
IntelliJ gives a spurious warning when a variable of type
Z (the alias) is
compared with an
Int literal (it does not give such warning if
BigInt is used
directly, but that is not supported in Logika).
Logika requires an explicit
return keyword when a method returns a value (which
can only be done at the end of the method, thus, in Scala, it is unnecessary).
When working with Logika math Unicode symbols (see LIVE Shortcuts), it is best to use a font that is also (mostly) fixed-width for those symbols.
In macOS, the Menlo font is fixed-width for Logika math symbols.
For Linux and Windows (and even macOS), Meslo is a good font to use; it is also an excellent font for programming or other purposes where a fixed-width font is desirable.
See the IntelliJ’s doc for changing your editor font.
IntelliJ will notify you whenever there is a newer version of LIVE. If accepted and LIVE is updated, you may also need to update Sireum v3.
LIVE detects when there is a new version of Sireum v3 when IntelliJ is launched. In such case, it displays the following notification:
To update, see Installation.
LIVE tries to detect when Sireum v3 has not been updated after LIVE is updated. In such case, it would present a one-time reminder that you need to update Sireum.
For more information, see Updating Logika.
If this is your first time opening the project, you need to
configure the project SDK
(note: the SDK Type should be Java SDK), and point it to the
(which was created during the process of :ref:` installing Logika <getting-started>`).
Opening any of the
.logika files would:
Syntax highlight the file document as shown in the screenshot at the top of this page.
The syntax highlighting uses IntelliJ’s Language Defaults editor color settings.
Cause LIVE to ask for the Sireum v3 installation directory (if it cannot infer Sireum v3 location).
Just point it to
SIREUM_HOME (see Getting Started).
If LIVE cannot confirm that the selected directory contains a working Sireum v3 installation, it will display the following:
See Sireum LIVE Configuration to adjust the settings.
Display the Logika status icon the bottom-right corner of the IntelliJ project window status bar:
The presence of the Logika status icon indicates that the Logika server is running/waiting in the background.
Clicking on the status icon will bring up a dialog that asks whether the server should be shutdown:
Yes will terminate the server and cause the status icon to disappear.
Display a notification at the top-right corner that the
.logika example is
That is, opening a
.logika file (or a
.lgk file) cause Logika to
automatically work on the file document.
As you edit the file, Logika will continually analyze it and give various
feedback such as syntax error marking (see Effects),
(LIVE waits a certain amount of time after the file content is modified before
calling Logika; this “idle” wait time period can be configured).
LIVE can also be configured to work with other file types.
Note that opening any configured files other than
does not automatically cause LIVE to directly verify and monitor such files.
Instead one needs to explicitly invoke Logika once.
Once invoked, LIVE will continue to monitor changes to the file document
If the editor is closed and reopened, Logika needs to be explicitly invoked once again.
There are three ways to explicitly bring Logika to LIVE:
Using a shortcut.
Note that these LIVE actions to verify file documents are only available for
.lgk and other file types that have been registered in Sireum LIVE Configuration.
Logika symbols can be converted to ASCII or Unicode by triggering the menu items
Convert to ASCII/
Convert to Unicode
or by right-clicking on the editor and selecting
Convert to ASCII/
Convert to Unicode
as shown in the screenshots above.
LIVE provides two main shortcuts:
For invoking Logika to analyze an opened file document.
The default keyboard shortcut is Shift-Command-L (
is set using one of the
Mac OS X Keymaps (i.e., the keymap name
Mac OS X); otherwise, it is Shift-Control-L (
This shortcut is only available for file types that have been registered in Sireum LIVE Configuration.
For inserting math Unicode symbols relevant for Logika. There are two keystrokes needed for a symbol insertion:
The first keystroke is Shift-Command/Control-Semicolon (
The second keystroke depends on which symbol to insert; below is a table of the shortcut, Unicode symbol and hexadecimal code, and its equivalent ASCII characters accepted by Logika.
Logika ASCII Equivalents
These symbol shortcuts are available for use in any text editor for any file types.
The keystrokes for the above shortcuts are the default keystrokes; they can be configured in IntelliJ’s Keymap settings.
For all settings, the associated setting labels give a tooltip that describes the corresponding settings when mouse hovered. In some settings, checks are implemented to ensure validity of the settings. An invalid setting is indicated by coloring the corresponding label red; in such case, mouse hovering the input widget may give a description of the expected format.
This setting can be used to (re-) enter the Sireum v3 directory, either
by typing the absolute path to the directory or by using a file browser dialog
that can be opened by clicking the
The entered path is checked to see whether it contains a working Sireum v3 installation.
Sireum tools such as Logika does not run directly inside the Java Virtual Machine (VM) instance that IntelliJ runs on. Instead, a VM is spawned, for example, for the Logika server in the background.
This setting can be used to provide some VM arguments when spawning the VM.
Each argument is separated by space(s) and each should start with a dash (
By default, the JVM stack size is set to 2Mb.
In the case where invalid VM arguments are specified, it would prevent spawning the Logika server; the plugin detects this situation and will revert the configuration to previous settings.
Additional environment variables can be specified in the text area.
SIREUM_HOME is set to the Sireum v3 directory and cannot be overriden;
it is required by Sireum tools to work properly
(e.g., it is how Logika finds where Z3 is installed).
The expected format is a key-value pair separated by an equal sign (
=) per line.
The key has to satisfy the following regular expression
(i.e., a letter or an underscore, followed by zero or more letters, digits, or underscores).
Some of the options such as auto mode, checking satisfiability, and timeout are described in Logika Command-Line Configuration. Below are the additional settings for LIVE.
The checkbox indicates whether LIVE should syntax highlight file documents.
The text field provides a way to configure which file types (based on their extension name) that LIVE actions should be enabled.
By default, only Scala Worksheet
.sc files are configured.
One can add other files such as
The expected format is the file extension names separated by semicolon (whitespaces are ignored).
This underwave effect checkbox controls how location-aware errors and warnings are marked in the editor. When selected, it uses the (more subtle) underwave effect typically used by IDEs to indicate ill-formed programs such as the following (compare it with the LIVE screenshot at the top of this page that does not use the underwave effect):
While more subtle, it comes with a red gutter icon on left hand side of the editor to help accentuate the marking.
Regardless of which one, the error stripe on the right hand side also indicates the marking.
Mouse hovering on any of the marker visualization will show a tooltip of the marker message.
This setting is used to turn on/off the Logika automatic background analysis as file documents are modified.
When turned off, the idle time is disabled (ignored), and one has to explicitly invoke Logika manually to verify file documents.
If selected, the idle time can be configured on how many milliseconds LIVE should wait after a file document is modified before sending it to the background Logika server for analysis.
Verifying programs can be challenging. To help with the process, Logika can generate some hints on the kind of program state claims can be made. If the hint generation is enabled, LIVE will mark locations where hints are available by using a bulb gutter editor icon. If clicked, it will open a view that presents the before/pre and after/post claims of the corresponding program location. For example,
when the bulb gutter icon associated with
a(x) = a(x) * a(x) at line 16 is clicked,
LIVE opens a window on the right hand side of the editor that displays
the available pre/post claims that can be used as premises.
When incription is enabled, LIVE will mark locations where external tools are employed by using a bolt gutter editor icon. If clicked, it will open a view that presents the incantations used for the corresponding summoning. For example (using Auto Mode),
when the second bolt gutter icon associated with
a(x) = a(x) * a(x - 1) at line 16 is clicked,
LIVE opens a window on the right hand side of the editor that displays
a list of proof obligations that were checked and then selects the third one
where the run-time check verification condition (VC) cannot be deduced;
the text area below the list displays the associated summoning incantations
(i.e., Z3 script) for the failed deduction.
Logika will attempt to simplify summonings by reducing the number of facts for proving a claim based on their relevance.