STELF project file Reference

A stelf.toml file is a TOML document that describes the groups (theories) in a STELF project and how they relate to one another. It sits at the root of your project directory.

A file contains any number of groups, declared using TOML’s array-of-tables syntax ([[group]]), and an optional interactive key naming the default group to load at the REPL.

# Optional: the group loaded by default at the REPL
interactive = "myproject"

[[group]]
name         = "myproject"
main         = "src/main.stelf"
src          = ["src"]
dependencies = ["base"]

---

Groups

Each [[group]] block defines one theory. A file may declare multiple groups.

name

Required. The name of the group, used to refer to it as a dependency from other groups.

A name is a STELF identifier: a sequence of one or more characters that are not whitespace or brackets (()[]{}"). The escape prefix %%. allows special characters to appear inside an identifier.

[[group]]
name = "peano"
# ...

[[group]]
name = "peano%%.(nat)"   # name contains "(nat)" via escape
# ...

main

Required. Path to the entry-point file for this group. When the group is imported as a dependency, this file is loaded first; it is responsible for opening (re-exporting) the other files in the group.

[[group]]
name = "peano"
main = "src/peano.stelf"
# ...

src

Optional. An array of directory paths that form the load-path roots for this group. STELF searches these directories when resolving file references within the group. Omission equivalent to ["."]

[[group]]
name = "peano"
main = "src/peano.stelf"
src  = ["src", "src/util"]
# ...

• Directorysrc/ - peano.stelf - nat.stelf - util/ - helpers.stelf - stelf.toml

  • …

dependencies

Optional. An array of dependencies this group needs. Each entry can be written in one of four forms — see Dependencies below. Omission equivalent to []

[[group]]
name         = "peano"
main         = "src/peano.stelf"
src          = ["src"]
dependencies = ["base", "logic"]

local

Optional, default false. When true, this group is private: it cannot be used as a dependency by other groups and can only be loaded directly at the REPL or CLI. Useful for top-level development scripts or scratch files.

[[group]]
name  = "scratch"
main  = "scratch.stelf"
src   = ["."]
local = true
dependencies = ["peano"]

---

Dependencies

Each entry in a dependencies array can take one of four forms.

Shorthand

The simplest form: just a name string. Equivalent to a local dependency with only name set — STELF looks for a group with that name in the current stelf.toml file.

dependencies = ["base", "logic"]

Local

References a group defined in a .toml file on disk. Written as an inline table (or an array-of-tables entry).

Field	Required	Description
name	Yes	The name of the group in the target file
path	No	Path to the .toml file. Defaults to the current file
alias	No	The namespace name used in this project. Defaults to name

dependencies = [
    # Another group in this same stelf.toml
    { name = "base" },

    # A group in a different file
    { name = "helpers", path = "lib/helpers.toml" },

    # Imported under a different namespace
    { name = "helpers", path = "lib/helpers.toml", alias = "h" },
]

• Directorylib/

  • helpers.toml
  • Directoryhelpers/

    • …
  • …
• Directorysrc/

  • main.stelf
• stelf.toml

Installed

References a system-installed package by name. The package manager locates and loads it from the system.

Field	Required	Description
name	Yes	The canonical name of the installed package
alias	No	The namespace name used in this project. Defaults to name

dependencies = [
    { name = "twelf-base" },
    { name = "twelf-base", alias = "base" },   # imported as "base"
]

Note

Installed dependencies are recognized by the presence of a name field and the absence of a path, url, or action field.

External

Downloads a dependency from a URL, saves it to a local directory, then treats the downloaded content as another dependency.

Field	Required	Description
url	Yes	The URL to download from
path	Yes	Local directory to download into
action	Yes	A dependency spec applied to the downloaded content

dependencies = [
    {
        url    = "https://example.com/base-lib.tar.gz",
        path   = "vendor/base",
        action = "base-lib",      # shorthand: look for "base-lib" group in the downloaded content
    },
]

• Directoryvendor/ - base/ - stelf.toml - src/ - … - src/ - main.stelf - stelf.toml

  • …

The action field is itself a full dependency spec (any of the four forms), applied with the downloaded directory as the working root.

---

The interactive key

Optional. Names the group to load by default when starting the REPL without specifying a group on the command line.

interactive = "myproject"

Without this key, the user must name a group explicitly:

stelf repl --group myproject

This key has no effect on how the file behaves when it is used as a dependency from another project.

---

Complete example

A project with two groups — a library and a top-level development script that depends on it — plus an external dependency.

interactive = "dev"

[[group]]
name         = "peano"
main         = "src/peano.stelf"
src          = ["src"]
dependencies = [
    "base",
    { name = "logic", path = "vendor/logic/stelf.toml" },
]

[[group]]
name         = "dev"
main         = "dev.stelf"
src          = ["."]
local        = true
dependencies = [
    "peano",
    {
        url    = "https://example.com/test-harness.tar.gz",
        path   = "vendor/test-harness",
        action = "test-harness",
    },
]

• Directorysrc/ - peano.stelf - nat.stelf - vendor/ - logic/ - stelf.toml - … - test-harness/ - stelf.toml - … - dev.stelf - stelf.toml

  • …