> ## Documentation Index
> Fetch the complete documentation index at: https://docs.theformalera.com/llms.txt
> Use this file to discover all available pages before exploring further.

# Local Hub

> A Spec Hub in a directory, for development, offline CI and air-gapped mirrors.

## A directory mirror

```bash theme={"system"}
uv run theformalera-hub keygen -o publisher.pem
uv run theformalera-hub publish --specs specs --store hub-data --version 1.0.0 --key publisher.pem
```

Point projects at it with `THEFORMALERA_HUB` (or `hub = "file:///…"` in `theformalera.toml`):

```bash theme={"system"}
export THEFORMALERA_HUB=file://$PWD/hub-data
export THEFORMALERA_MATHLIB=$PWD/specs        # reuse this workspace's Mathlib build
cd examples/acme-qwen3.8-27b-h100 && theformalera pull && theformalera verify
```

With a `file://` Hub:

* no token is needed; `THEFORMALERA_ORG` names your organisation (default `local-org`) and `THEFORMALERA_PLAN` your plan (default `enterprise`);
* the lemma libraries are directories in the store; deposits go to `lemmas/inbox/` and are admitted by `theformalera-hub lemmas admit`;
* cloud verification is not available: use `runner = "local"`.

> [!WARNING]
>
> `theformalera.lock` pins package digests. A lock written against one Hub only works with a Hub that serves the same package. After pointing a project at a different Hub, run `theformalera pull --update`, or delete the lock and pull again.

## Run the API

```bash theme={"system"}
uv run theformalera-hub serve --store hub-data --host 0.0.0.0 --port 8700
```

Then set `hub = "http://<host>:8700"` in projects. Issue tokens with:

```bash theme={"system"}
uv run theformalera-hub token --store hub-data --tenant acme --plan team
```

```text theme={"system"}
tfe_…
```

For cloud-style solving, run one or more workers next to it. They take jobs from the store's queue and run the engine:

```bash theme={"system"}
uv run theformalera-hub worker --store hub-data --specs specs
```

## Render the website

```bash theme={"system"}
uv run theformalera-hub site --store hub-data -o site
uv run python -m http.server -d site 8080
```

The site has a page per model (Lean definitions, rendered formulas, the compute graph and the trust status), a page per node, and a page per lemma.


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.