litex-lang 0.9.75-beta

A simple formal proof language and verifier, learnable in 2 hours
Documentation
# Install Litex

Jiachen Shen and The Litex Team, 2026-05-06. Email: litexlang@outlook.com

Try all snippets in browser: https://litexlang.com/doc/Setup

Markdown source: https://github.com/litexlang/golitex/blob/main/docs/Setup.md


## Run Litex online

To quickly try Litex, use the Playground on the official website:

- https://litexlang.com

You can run Litex code there and translate Litex code into LaTeX.

## Install and run Litex locally

Release assets are published at:

- https://github.com/litexlang/golitex/releases

---

## macOS (Homebrew)

Install:

```bash
brew install litexlang/tap/litex
```

Upgrade:

```bash
brew update
brew upgrade litexlang/tap/litex
```

If upgrade fails or is too slow on your machine, use:

```bash
brew uninstall litex
brew install litexlang/tap/litex
```

---

## Linux (Ubuntu/Debian)

Install latest release automatically (amd64):

```bash
tag=$(curl -fsSL https://api.github.com/repos/litexlang/golitex/releases/latest | grep '"tag_name"' | sed -E 's/.*"([^"]+)".*/\1/')
wget "https://github.com/litexlang/golitex/releases/download/${tag}/litex_${tag}_amd64.deb"
sudo dpkg -i "litex_${tag}_amd64.deb"
```

If you want a fixed tag, replace `<tag>` manually:

```bash
wget "https://github.com/litexlang/golitex/releases/download/<tag>/litex_<tag>_amd64.deb"
sudo dpkg -i "litex_<tag>_amd64.deb"
```

If needed, fix dependencies:

```bash
sudo apt-get install -f
```

### Upgrade Litex on Linux

If you installed from the `.deb` in Releases, upgrade by downloading the latest tag and installing
it again (this replaces the older version):

```bash
tag=$(curl -fsSL https://api.github.com/repos/litexlang/golitex/releases/latest | grep '"tag_name"' | sed -E 's/.*"([^"]+)".*/\1/')
wget "https://github.com/litexlang/golitex/releases/download/${tag}/litex_${tag}_amd64.deb"
sudo dpkg -i "litex_${tag}_amd64.deb"
```

Then verify:

```bash
litex -version
```

---

## Windows

### Option A (recommended): one command in PowerShell

Run this command in **PowerShell**:

```powershell
$ErrorActionPreference = 'Stop'
$repo = 'litexlang/golitex'
$tag = (Invoke-RestMethod -Uri "https://api.github.com/repos/$repo/releases/latest" -Headers @{ 'User-Agent' = 'litex-install' }).tag_name
$name = "litex_${tag}_windows_amd64.exe"
$url = "https://github.com/$repo/releases/download/$tag/$name"
$dir = Join-Path $env:LOCALAPPDATA 'litex'
$exe = Join-Path $dir 'litex.exe'

New-Item -ItemType Directory -Force -Path $dir | Out-Null
Invoke-WebRequest -Uri $url -OutFile $exe

$userPath = [Environment]::GetEnvironmentVariable('Path', 'User')
if (-not $userPath) { $userPath = '' }
if ($userPath -notlike "*$dir*") {
    $newPath = if ($userPath) { "$userPath;$dir" } else { $dir }
    [Environment]::SetEnvironmentVariable('Path', $newPath, 'User')
}

$env:Path = "$dir;$env:Path"
Write-Host "Installed: $exe"
Write-Host "Open a new terminal and run: litex -version"
```

What this command changes on the user machine:

1. Downloads `litex_<tag>_windows_amd64.exe` from GitHub Releases.
2. Writes one file to `%LOCALAPPDATA%\litex\litex.exe`.
3. Appends `%LOCALAPPDATA%\litex` to the **User** `Path` environment variable.
4. Updates `Path` in the current PowerShell session.

It does **not** install services or edit firewall settings.

After running the command:

1. Open a **new** terminal window.
2. Run:

```powershell
litex -version
```

Now users can run `litex` directly in terminal.

If you want a fixed tag (for example a beta tag), use:

```powershell
$ErrorActionPreference = 'Stop'
$tag = '0.9.73-beta'
$repo = 'litexlang/golitex'
$name = "litex_${tag}_windows_amd64.exe"
$url = "https://github.com/$repo/releases/download/$tag/$name"
$dir = Join-Path $env:LOCALAPPDATA 'litex'
$exe = Join-Path $dir 'litex.exe'

New-Item -ItemType Directory -Force -Path $dir | Out-Null
Invoke-WebRequest -Uri $url -OutFile $exe

$userPath = [Environment]::GetEnvironmentVariable('Path', 'User')
if (-not $userPath) { $userPath = '' }
if ($userPath -notlike "*$dir*") {
    $newPath = if ($userPath) { "$userPath;$dir" } else { $dir }
    [Environment]::SetEnvironmentVariable('Path', $newPath, 'User')
}

$env:Path = "$dir;$env:Path"
litex -version
```

### Upgrade Litex on Windows

If you installed by **Option A** (PowerShell one-command install), run the same command again.
It downloads the newer `litex.exe`, overwrites `%LOCALAPPDATA%\litex\litex.exe`, and keeps your
existing user `Path` entry:

```powershell
$ErrorActionPreference = 'Stop'
$repo = 'litexlang/golitex'
$tag = (Invoke-RestMethod -Uri "https://api.github.com/repos/$repo/releases/latest" -Headers @{ 'User-Agent' = 'litex-install' }).tag_name
$name = "litex_${tag}_windows_amd64.exe"
$url = "https://github.com/$repo/releases/download/$tag/$name"
$dir = Join-Path $env:LOCALAPPDATA 'litex'
$exe = Join-Path $dir 'litex.exe'
New-Item -ItemType Directory -Force -Path $dir | Out-Null
Invoke-WebRequest -Uri $url -OutFile $exe
$userPath = [Environment]::GetEnvironmentVariable('Path', 'User')
if (-not $userPath) { $userPath = '' }
if ($userPath -notlike "*$dir*") {
    $newPath = if ($userPath) { "$userPath;$dir" } else { $dir }
    [Environment]::SetEnvironmentVariable('Path', $newPath, 'User')
}
$env:Path = "$dir;$env:Path"
litex -version
```

---

## Run Litex on your machine

Start REPL:

```bash
litex
```

Typical successful output:

```text
Litex-beta - Type your code or 'exit' to quit
Warning: not yet ready for production use.
>>>
```

Run a `.lit` file:

```bash
litex -f "your_file.lit"
```

Run Litex source directly:

```bash
litex -e "1 + 1 = 2"
```

---

## Command-line options

In examples, the executable is written as:

```text
litex [OPTION...]
```

Basic behavior:

- **No arguments**: starts the interactive REPL.
- **With options**: runs code, files, repositories, or helper commands as described below.
- **Unknown options**: print an error message and exit.

| Option | Description |
|--------|-------------|
| `-help` | Print help and exit. |
| `-version` | Print the Litex version and exit. |
| `-e <code>` | Run a Litex source string. |
| `-f <file>` | Run a file. The path may be relative to the current working directory or absolute. |
| `-r <repo>` | Same as running `<repo>/main.lit`. Place `main.lit` at the repo root. |
| `-latex` | Enter LaTeX-related mode. |
| `-latex -f <file>` | Compile a file to LaTeX, when available. |
| `-latex -e <code>` | Compile a source string to LaTeX, when available. |
| `-fmt <code>` | Format Litex code, when available. |
| `-install <module>` | Install a module, when available. |
| `-uninstall <module>` | Uninstall a module, when available. |
| `-list` | List installed modules, when available. |
| `-update <module>` | Update a module, when available. |
| `-tutorial` | Run the tutorial, when available. |

Options like `-e`, `-f`, `-r`, `-fmt`, `-install`, `-uninstall`, and `-update` require a value that does not start with `-` immediately after the flag. After `-latex`, you may use sub-options `-f`, `-e`, or `-r` with their arguments.

Hint: if your Litex code contains spaces, newlines, or shell-sensitive characters, wrap it in quotes when using `-e`, or put it in a `.lit` file and run it with `-f`.

---

## Command output format

For commands that execute Litex source, such as `-e`, `-f`, and `-r`, Litex prints one JSON object for each executed statement.

If the whole run succeeds:

- The output contains one JSON object per user statement, separated by newlines; each object describes that statement's outcome.
- Each successful statement object has `"result": "success"`.
- The last JSON object for your source is the last statement that ran successfully.

This is useful when another program wants to call Litex and inspect whether a proof or computation succeeded.

Example success output looks like this. The exact output may differ by version:

```json
{
  "result": "success",
  "type": "Fact",
  "line": 1,
  "source": "~/tmp.lit",
  "stmt": "1 + 1 = 2",
  "infer_facts": [],
  "inside_results": []
}
```

If an error occurs, Litex prints an error JSON object. The important fields are usually:

- `"result": "error"`
- `"error_type"`: the broad kind of error, such as parse, verify, or runtime error
- `"message"`: the human-readable reason
- `"previous_error"`: more context, if the error was caused by another error

Hint: programs that call Litex should check the JSON output, not only the process exit code.

Example error output looks like this. The exact output may differ by version:

```json
{
  "error_type": "VerifyError",
  "result": "error",
  "line": 1,
  "source": "~/tmp.lit",
  "message": "1 = 0",
  "previous_error": {
    "error_type": "UnknownError",
    "result": "error",
    "line": 1,
    "source": "~/tmp.lit",
    "message": "1 = 0",
    "previous_error": null
  }
}
```

---

## Commands that may still be unavailable

Some helper commands, such as LaTeX output, formatting, module management, or tutorial mode, may be unavailable in a particular build. When a command is not available, Litex may print a plain-text placeholder message instead of the JSON stream used for source execution.