Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Getting Started

To start creating Lilo specification files, you need two things:

  • The SpecForge server (via docker)
  • The VSCode extension

SpecForge Server (via Docker)

Obtaining the Docker Image

Setup (One-time)

  1. Save the provided JSON key somewhere, e.g.: some_dir/key.json.
  2. Run this command at the working directory to authenticate with Google Artifact Registry:
cat key.json | docker login -u _json_key --password-stdin https://asia-northeast1-docker.pkg.dev

Docker will now use this key to pull from Imiron's docker image registry.

Updating the Image (upon new release)

To pull the latest image, run:

docker compose pull

Configuration

The provided docker-compose.yml file is configured to run the SpecForge server.

By default, the SpecForge server runs on port 8080.

For using LLM-based features such as natural-language based spec generation and error explanation, you need an OpenAI API key (which can be obtained from the OpenAI website).

To use an API key, set the environment variable OPENAI_KEY in your shell or replace the following line with the actual key in the docker-compose.yml file:

- OPENAI_KEY=${OPENAI_KEY}
Without an OpenAI API key, LLM-based SpecForge features would be unavailable.

Running the Server

To run SpecForge you just need Docker Compose, which is most likely already available if you installed Docker itself. With docker-compose.yml in current directory run:

docker compose up --abort-on-container-exit

The flag --abort-on-container-exit is recommended so that the container fails fast on startup errors.

You can verify that the server is up by navigating to http://localhost:8080/health, which should show the appropriate version information.

Lilo Language Extension for VSCode

The Lilo Language Extension for VSCode provides

  • Syntax Highlighting, Typechecking and Autocompletion for .lilo files
  • Satisfiability and Redundancy checking for specifications
  • Support for visualizing monitoring results in Python notebooks

Installation

To install the extension, locate the lilo-language-x.x.x.vsix file, and install it in one of the following ways:

  • Open the extensions tab (Ctrl+Shift+X or Cmd+Shift+X), click on the three dots at the top right, and select Install from VSIX...
  • Open the command palette (Ctrl+Shift+P or Cmd+Shift+P), type Extensions: Install from VSIX..., and select the .vsix file

Usage and Configuration

  • For the extension to work, the SpecForge server must be running (see above).
  • The URI corresponding to the server can be configured if necessary using the extension settings.

Once the extension is installed and the server is running, it should automatically be working on .lilo files, and in relevant Python notebooks.

Python SDK

The Python SDK is a python library which can be used to interact with SpecForge tools programmatically from within Python programs, including notebooks.

The Python SDK is packaged as a wheel file with the name specforge_sdk-x.x.x-py3-none-any.whl. It can be installed directly using pip, or defined as a dependency via a build envionment such as poetry or uv.

See the documentation on the Python SDK for more details.