otty / apps

All apps/Agda

Agda

agda

A dependently typed functional programming language.

Runs as agda|macOS, Linux, Windows|agda.readthedocs.io

Open form in Otty otty.toml

Sync rules

What travels, what stays, what never leaves

Agda in your home directory Every rule on this page, by file

· defaults Sync

/Users/octocat/agda/standard-library/standard-library.agda-libmachine-local

Each machine keeps its own copy of these.

· defaults Sync

/Users/octocat/agda/standard-library/standard-library.agda-libmachine-local

Each machine keeps its own copy of these.

Only what the catalog names. A directory that syncs brings everything inside it except what is listed as excluded here.

apps/agda/otty.tomlThe file this page is generated from

id = "agda"

name = "Agda"

homepage = "https://agda.readthedocs.io"

description = "A dependently typed functional programming language."

executables = ["agda"]

[dotfiles]

# The official Agda manual documents AGDA_DIR/defaults and

# AGDA_DIR/libraries. AGDA_DIR defaults to ~/.config/agda on Unix-like

# systems, falls back to ~/.agda for compatibility, and uses %APPDATA%/agda

# on Windows. The two files contain the user's library registrations and

# default libraries.

# https://agda.readthedocs.io/en/latest/tools/package-system.html

paths = [

"~/.config/agda/defaults",

"~/.config/agda/libraries",

"~/.agda/defaults",

"~/.agda/libraries",

"%APPDATA%/agda/defaults",

"%APPDATA%/agda/libraries",

]

secret = []

# The libraries file records absolute library paths, which are local to the

# machine that installed each Agda library.

[[dotfiles.machine_lines]]

file = [

"~/.config/agda/libraries",

"~/.agda/libraries",

"%APPDATA%/agda/libraries",

]

match = { prefix = ["/"] }

scope = "backup"

[commands]

format = 1

label = "Type-check an Agda file"

description = "Type-check an Agda module with a few common options and optionally generate HTML, LaTeX or Vim highlighting. Compiler backends, interaction mode and the many pragma-style flags are left out."

quality = "ai-draft"

parser = { end_of_options = "--", interleave = "permute", long_equals = true, short_attached = false, short_bundles = false }

[[commands.source]]

id = "docs"

kind = "manual"

url = "https://agda.readthedocs.io/en/latest/tools/command-line-options.html"

revision = "latest 2026-10"

evidence = """

--html

Generate HTML files with highlighted source code

--latex

Generate LaTeX with highlighted source code

--vim

Generate Vim highlighting files.

--include-path={DIR}, -i {DIR}

Look for imports in DIR. This option can be given multiple times.

--library={DIR}, -l {LIB}

Use library LIB.

--library-file={FILE}

Use FILE instead of the standard libraries file.

--safe

Disable postulates, unsafe OPTIONS pragmas and primTrustMe.

--without-K

--allow-unsolved-metas

Succeed and create interface file regardless of unsolved meta variables

--only-scope-checking

--dependency-graph={FILE}

Generate a Dot file FILE with a module dependency graph.

--ignore-interfaces

Don't read interface files (re-type check everything

"""

[[commands.field]]

id = "file"

label = "Agda file"

type = "path"

position = 0

path = { kind = "file", role = "input" }

sources = ["docs"]

[[commands.field]]

id = "safe"

label = "Safe mode"

type = "boolean"

option = ["--safe"]

sources = ["docs"]

[[commands.field]]

id = "without_k"

label = "Without K"

type = "boolean"

option = ["--without-K"]

sources = ["docs"]

[[commands.field]]

id = "allow_unsolved_metas"

label = "Allow unsolved metas"

type = "boolean"

option = ["--allow-unsolved-metas"]

sources = ["docs"]

[[commands.field]]

id = "include_path"

label = "Import search directories"

type = "path"

option = ["--include-path"]

multiple = true

path = { kind = "directory", role = "input" }

sources = ["docs"]

[[commands.field]]

id = "library"

label = "Libraries"

type = "string"

option = ["--library"]

multiple = true

sources = ["docs"]

[[commands.field]]

id = "library_file"

label = "Libraries file"

type = "path"

option = ["--library-file"]

path = { kind = "file", role = "input" }

sources = ["docs"]

[[commands.field]]

id = "html"

label = "Generate HTML"

type = "boolean"

option = ["--html"]

sources = ["docs"]

[[commands.field]]

id = "latex"

label = "Generate LaTeX"

type = "boolean"

option = ["--latex"]

sources = ["docs"]

[[commands.field]]

id = "vim"

label = "Generate Vim highlighting"

type = "boolean"

option = ["--vim"]

sources = ["docs"]

[[commands.field]]

id = "dependency_graph"

label = "Dependency graph (Dot file)"

type = "path"

option = ["--dependency-graph"]

path = { kind = "file", role = "output" }

effect = "overwrite"

sources = ["docs"]

[[commands.field]]

id = "only_scope_checking"

label = "Only scope-check"

type = "boolean"

option = ["--only-scope-checking"]

sources = ["docs"]

[[commands.field]]

id = "ignore_interfaces"

label = "Ignore interface files"

type = "boolean"

option = ["--ignore-interfaces"]

sources = ["docs"]

[[commands.task]]

id = "check"

label = "Type-check"

fields = ["file", "safe", "include_path", "library"]

required = ["file"]

[[commands.task]]

id = "html_docs"

label = "Generate HTML"

fields = ["file", "html", "include_path", "library"]

required = ["file", "html"]

set = { html = [true] }

[[commands.group]]

id = "basic"

label = "Basic"

fields = ["file", "safe", "without_k", "allow_unsolved_metas", "include_path", "library", "html"]

[[commands.group]]

id = "advanced"

label = "Advanced"

fields = ["library_file", "latex", "vim", "dependency_graph", "only_scope_checking", "ignore_interfaces"]

Use it with your dotfile manager

Same data, in the shape your tool already reads

Opens Otty and adds this tool to what it syncs

Opens otty://sync/add/agda. Otty ships with this catalog, so the link only has to name the tool — nothing is downloaded.

Every one of these is generated from the same rules as this page. None of them splits / and / for you — that part is Otty’s own sync, or a template you write by hand.