OptEnvConf

Configure Lean 4 programs via command-line options, environment variables, and configuration files.

Reimplementation of the Haskell opt-env-conf library.

Features

• Three configuration sources with clear priority: CLI args > env vars > config file > defaults
• deriving ParseConfig -- generate parsers automatically from structure definitions
• Declarative builder DSL for defining settings manually
• Automatic help generation (--help)
• Config schema output (--render-config-schema, --render-json-schema)
• Subcommand support
• Composable parsers via Functor, Applicative, and Alternative
• Prefixing (subArgs, subEnv, subConfig, subAll) for nested settings
• JSON config file loading via withConfig

Quick Start

Add to your lakefile.toml:

[[require]]
name = "OptEnvConf"
path = "path/to/opt-env-conf"  # or use git

Then define a parser. The simplest approach is deriving ParseConfig:

import OptEnvConf
open OptEnvConf

structure Config where
  /-- Server host -/
  host : String := "localhost"
  /-- Server port -/
  port : Nat := 8080
  /-- Verbose output -/
  verbose : Bool := false
  deriving ParseConfig

def main (args : List String) : IO Unit := do
  let config : Config ← runSettingsParser ParseConfig.parser "myapp" "1.0.0" args
  IO.println s!"Listening on {config.host}:{config.port}"

This generates --host, --port, --verbose CLI options, HOST, PORT, VERBOSE env vars, and host, port, verbose config file keys -- all with help text from docstrings and defaults from field values.

$ myapp --help
myapp 1.0.0

Usage: myapp [--host <STRING>] [--port <NAT>] [--verbose]

Options:
  --host STRING               Server host  (env: HOST; conf: host) [default: localhost]
  --port NAT                  Server port  (env: PORT; conf: port) [default: 8080]
  --verbose                   Verbose output  (env: VERBOSE; conf: verbose) [default: false]
  ...

Deriving ParseConfig

deriving ParseConfig on a structure auto-generates a parser based on:

Structure feature	Generated parser
Field name myField	--my-field flag, MY_FIELD env var, my-field config key
Docstring /-- ... -/	Help text
Default value := val	Default
String, Nat, Int, Float	--key VALUE option
Bool	--key switch
Option α	Optional (omittable)
List α	Repeatable
Nested struct with ParseConfig	Prefixed via subAll (e.g. --db-host, DB_HOST, db.host)

Nested structures

Structures that derive ParseConfig compose automatically:

structure DbSettings where
  /-- Database hostname -/
  host : String := "localhost"
  /-- Database port -/
  port : Nat := 5432
  deriving ParseConfig

structure AppSettings where
  /-- Log level -/
  logLevel : String := "info"
  /-- Enable verbose output -/
  verbose : Bool := false
  /-- Database connection settings -/
  db : DbSettings
  /-- Optional description -/
  description : Option String
  deriving ParseConfig

This produces CLI flags --log-level, --verbose, --db-host, --db-port, --description, with corresponding env vars (LOG_LEVEL, VERBOSE, DB_HOST, DB_PORT, DESCRIPTION) and config file keys.

Custom ParseableField instances

The derive handler uses the ParseableField typeclass to know how to parse leaf types. Built-in instances exist for String, Nat, Int, Float, and Bool. You can add your own:

instance : ParseableField MyEnum where
  reader := ⟨fun s => match s with
    | "a" => .ok .a | "b" => .ok .b
    | _ => .error ("Expected a or b, got: " ++ s)⟩
  jsonDecode
    | .str "a" => .ok .a | .str "b" => .ok .b
    | _ => .error "Expected \"a\" or \"b\""
  schemaType := .string
  metavar_ := "a|b"

Manual Builder DSL

For full control, you can write parsers manually using the builder DSL. Each setting takes a list of builders:

Builder	Description
help "text"	Documentation string
metavar "NAME"	Placeholder in help output
reader Reader.str	Parse from string (also: .nat, .int, .bool)
argument	Parse as positional argument
option	Parse as --key value option
switch val	Flag that activates with the given value
long "name"	Long option --name
short 'c'	Short option -c
env "VAR"	Environment variable
conf "key"	JSON config file key (requires Lean.FromJson)
confWith "key" decode schemaType	Config key with custom decoder
value v	Default value
hidden	Hide from documentation
name "camelCase"	Shorthand for option + long + env + conf with case conversion

Priority Order

When a setting has multiple sources, they are tried in this order:

1. Positional argument (if argument is set)
2. Switch (if switch is set and flag is present)
3. Command-line option (if option is set)
4. Environment variable (if env is set) -- reads from process environment via IO.getEnv
5. Config file value (if conf/confWith is set)
6. Default value (if value is set)

Combinators

-- Functor / Applicative / Alternative
f <$> parser           -- map
parserF <*> parserA    -- sequence
parser1 <|> parser2    -- try first, fallback to second

-- Repetition
Parser.many' p         -- zero or more
Parser.some' p         -- one or more
Parser.optional p      -- Option α

-- Validation
checkMapEither f p     -- validate/transform with pure function
checkMapIO f p         -- validate/transform with IO
mapIO f p              -- apply IO action to result

-- Prefixing for nested settings
subArgs "prefix-" p    -- prefix CLI option names
subEnv "PREFIX_" p     -- prefix env var names
subConfig "prefix" p   -- prefix config keys
subAll "prefix" p      -- prefix all three (with case conversion)

-- Commands
commands [
  command "create" "Create something" createParser,
  command "delete" "Delete something" deleteParser
]

JSON Config Files

Use withConfig to load a JSON config file:

def configLoader : Parser (Option Lean.Json) :=
  mapIO (fun path? => match path? with
    | some p => readJsonConfigFile p
    | none => pure none)
  (Parser.optional (setting [
    reader Reader.str, option, long "config", short 'c',
    env "APP_CONFIG", metavar "FILE"
  ]))

def fullParser : Parser MyConfig :=
  withConfig configLoader mySettingsParser

Settings with conf/confWith will then read from the loaded JSON.

Built-in Flags

runSettingsParser automatically handles:

Flag	Description
--help, -h	Print help page
--version	Print version
--render-config-schema	Print config schema (human-readable)
--render-json-schema	Print JSON Schema for config file

Editor Integration for Config Files

The --render-json-schema flag outputs a JSON Schema that editors can use for validation, completion, and hover documentation when editing your application's config file.

Generating the schema

./myapp --render-json-schema > myapp-config-schema.json

VS Code

Install the YAML extension (for YAML configs) or use the built-in JSON support.

Add to your .vscode/settings.json:

{
  // For JSON config files
  "json.schemas": [
    {
      "fileMatch": ["myapp-config.json"],
      "url": "./myapp-config-schema.json"
    }
  ],
  // For YAML config files (requires redhat.vscode-yaml extension)
  "yaml.schemas": {
    "./myapp-config-schema.json": "myapp-config.yaml"
  }
}

Alternatively, add a $schema key directly in your JSON config file:

{
  "$schema": "./myapp-config-schema.json",
  "log-level": "debug"
}

Neovim

With nvim-lspconfig + jsonls:

require('lspconfig').jsonls.setup {
  settings = {
    json = {
      schemas = {
        {
          fileMatch = { "myapp-config.json" },
          url = "./myapp-config-schema.json",
        },
      },
    },
  },
}

With nvim-lspconfig + yamlls:

require('lspconfig').yamlls.setup {
  settings = {
    yaml = {
      schemas = {
        ["./myapp-config-schema.json"] = "myapp-config.yaml",
      },
    },
  },
}

With SchemaStore.nvim (if you publish your schema):

If you publish the schema to SchemaStore, both editors pick it up automatically — no per-project configuration needed.

Examples

See the examples/ directory:

• examples/derive/ -- deriving ParseConfig with nested structures, optional fields
• examples/simple/ -- Manual DSL: positional argument, options, switch, env var
• examples/rich/ -- Manual DSL: subcommands, config file, nested settings

Build and run an example:

lake build derive-example
.lake/build/bin/derive-example --help
.lake/build/bin/derive-example --db-host mydb --db-port 3306 --verbose

Architecture

The library is structured as:

Module	Purpose
OptEnvConf.Derive	deriving ParseConfig handler, ParseableField and ParseConfig typeclasses
OptEnvConf.Reader	String-to-value parsing functions
OptEnvConf.Types	Core types: Setting, Parser, ParseEnv, ParseError, DocTree
OptEnvConf.Builder	DSL for constructing Settings
OptEnvConf.Args	CLI argument tokenization and consumption
OptEnvConf.Parser_	Parser combinators and execution engine
OptEnvConf.Run	Public API, help/schema rendering, runSettingsParser

Parser α is a structure containing:

• runFn : ParseEnv → IO (ParseResult α) -- the execution function
• doc : DocTree -- the documentation tree (used for --help and schema output)