← Command reference · lean-pkg palomar · CLI overview

lean-pkg palomar port-modules

plan (dry run, default) or –write the mechanical port of the package’s tracked .lean files to Lean’s module system; never commits.

Usage

lean-pkg palomar port-modules [--dry-run] [--write] [--agent AGENT] [common flags] NAME

[common flags]: --json, --commit, --push, --no-commit, also accepted before the command name; see the CLI overview.

Arguments and flags

Argument or flag Description
NAME  
--dry-run the default: print the per-file plan and the unified diff; write nothing
--write apply the plan to a clean working tree (a dirty tree is refused); never commits, never writes the registry
--agent AGENT with –write: the lease holder, when the package is leased

Details

Form What it does Key flags
palomar port-modules NAME the mechanical port of the package’s tracked .lean files to Lean’s module system, which Palomar requires (palomar check: source.module_required). Reads git objects at HEAD; a dry run by default (--dry-run): a per-file report and a unified diff, nothing written. Per file without a module header: module inserted as the first command (after leading blanks and ordinary comments; before a /-! -/ or /-- -/, which are commands), each header import X rewritten to public import X (meta import X to public meta import X; import all, private and public forms kept, never public import all), the body after the imports (and after the module docstrings that follow them) wrapped in public section … end (no end when a namespace/section is still open at the end of the file). A module-headed file is skipped, so a second run is a no-op. Refused per file, with the reason: a prelude file (port it by hand), a file that is not UTF-8, a symlink. Reported for review, never auto-fixed (review [CODE], lines of the ported file): expose (a def that another file unfolds with unfold, delta, simp [d], rw [d], d.eq_def, or reduces on a line with rfl/decide: add @[expose]; abbrev and instances are already exposed), private (a private name in a public statement is an unknown identifier), meta (#eval, native_decide, initialize: code from another module needs a meta import), imports-non-module (a module cannot import a non-module file or dependency), scope-balance. Only the package’s files: .lake/, lake-packages/, nested Lake projects and path dependencies are excluded and lakefile.lean is exempt. --write applies the plan to a clean working tree (a modified or untracked path, a refused file, or a foreign live lease without --agent HOLDER refuses, exit 1, nothing written); it never commits and never writes the registry, and prints the follow-ups: lake build, the @[expose] review, lean-pkg palomar check NAME after the commit, and for a gated package a new gate (the sources changed). Exit 0, or 1 when a file is refused. --json: {ok, name, dry_run, written[], commit, project_path, files[{path, action port|skip|refused, reason, edits[], reviews[{code, line, detail}]}], counts{port, skip, refused, review}, expose[], excluded[], vendored_dirs[], outside_package, diff, follow_ups[]} [--dry-run \| --write] [--agent A]

JSON output

Top-level keys of --json, as recorded in the golden contract (tests/golden/json-keys.json):