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"]