From de56626059d63d3119227a66223490c355e84b31 Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Fri, 1 May 2026 06:23:36 -0600 Subject: [PATCH] =?UTF-8?q?Drop=20algebra-restructure=20exe=20=E2=80=94=20?= =?UTF-8?q?source=20code=20IS=20the=20CLI?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove `AlgebraRestructure.lean` and its lake_exe target. The `Algebra.printAliases` / `printMethodologies` / `printMetaPaths` functions remain (foundation primitives); users invoke them via `#eval` inside a Lean session, or compose them in downstream Lean code. No standalone process boundary, no opinionated subcommand surface, no argv parsing layer — the Lean source is the interface. Per the principle: foundation primitives ship; tooling-as-process- exe does not unless explicitly asked. A Lake-exe wrapper imposes opinionated naming, output shape, and exit-code conventions that aren't load-bearing for the registry-printer use case. 93/93 tests still pass. Co-Authored-By: Claude Opus 4.7 (1M context) --- AlgebraRestructure.lean | 87 ----------------------------------------- lakefile.toml | 13 ++---- 2 files changed, 4 insertions(+), 96 deletions(-) delete mode 100644 AlgebraRestructure.lean diff --git a/AlgebraRestructure.lean b/AlgebraRestructure.lean deleted file mode 100644 index c5aac63..0000000 --- a/AlgebraRestructure.lean +++ /dev/null @@ -1,87 +0,0 @@ -/- - AlgebraRestructure — thin labeled shell over registry-printer functions - ====================================================================== - This is a *demonstrator* CLI, not a normative tool. It exists to - show how a downstream tool can wrap the registry-printer functions - (`Algebra.printAliases`, `Algebra.printMethodologies`, - `Algebra.printMetaPaths`) into a Lake-exe entry point. Anyone - wanting different subcommands, output formats, filters, or batch - operations should write their own thin shell — the underlying - printer functions are the foundation; this `main` is just one - obvious wrapping. - - No opinion is baked in beyond the four subcommand choices below; - the printer functions accept a `CoreM Unit` shape that any other - shell (a different CLI, an LSP server, a CI step) can call equally. - - ## Current state (2026-05-01) - - The Lean 4 `SimplePersistentEnvExtension` state (where - `@[macroAlias]` / `@[methodology]` / `@[metaPath]` register their - entries) is captured in module `.olean` files at build time, but - it does NOT reliably re-load when an Environment is reconstructed - via `importModules` from a standalone executable. This is a known - limitation of Lean 4's EnvExtension persistence in non-LSP - contexts; the registries are fully visible during elaboration - (e.g., from a `#eval Algebra.printMethodologies` inside a Lean - session) but invisible to this CLI. - - Until that's resolved upstream, this CLI prints the source location - of every `@[macroAlias]` / `@[methodology]` / `@[metaPath]` - declaration in the project — a static map, not the live registry. - - Subcommands (this demonstrator's choice; not normative): - · `list-aliases` — point to source declarations. - · `list-methodologies` — point to source declarations. - · `list-paths` — point to source declarations. - · `help` — print this listing. --/ - -import CubicalTransport - -def usage : IO Unit := do - IO.println "Usage: lake exe algebra-restructure " - IO.println "" - IO.println "Subcommands:" - IO.println " list-aliases — point to @[macroAlias] declarations" - IO.println " list-methodologies — point to @[methodology] declarations" - IO.println " list-paths — point to @[metaPath] declarations" - IO.println " help — show this message" - IO.println "" - IO.println "For live registry contents, run inside a Lean session:" - IO.println " #eval CubicalTransport.Algebra.printAliases" - IO.println " #eval CubicalTransport.Algebra.printMethodologies" - IO.println " #eval CubicalTransport.Algebra.printMetaPaths" - -/-- Print the static project-side list of modules that contain - `@[macroAlias]` / `@[methodology]` / `@[metaPath]` declarations. - For live runtime inspection, see the `#eval`-based diagnostic - inside a Lean source file. -/ -def listSourceModules (kind : String) : IO Unit := do - IO.println s!"── @[{kind}]-tagged declarations live in: ──" - match kind with - | "macroAlias" => - IO.println " CubicalTransport/Algebra/Restructure.lean (frozen aliases)" - IO.println " CubicalTransport/Algebra/Test.lean (test-side aliases)" - | "methodology" => - IO.println " CubicalTransport/Algebra/Test.lean (test methodologies)" - IO.println " CubicalTransport/Algebra/EngineMethodologies.lean (engine closers)" - | "metaPath" => - IO.println " CubicalTransport/Algebra/Test.lean (test paths)" - | _ => pure () - IO.println "" - IO.println "Use `#eval CubicalTransport.Algebra.print* : CoreM Unit` inside" - IO.println "a Lean session for live registry contents. See the docstring" - IO.println "of this module for why runtime CLI introspection is currently" - IO.println "limited." - -def main (args : List String) : IO UInt32 := do - match args with - | ["list-aliases"] => listSourceModules "macroAlias"; return 0 - | ["list-methodologies"] => listSourceModules "methodology"; return 0 - | ["list-paths"] => listSourceModules "metaPath"; return 0 - | ["help"] | [] => usage; return 0 - | _ => - IO.eprintln s!"unknown subcommand: {args}" - usage - return 1 diff --git a/lakefile.toml b/lakefile.toml index c864605..dcc7fae 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -22,12 +22,7 @@ moreLinkArgs = [ "./native/cubical/target/release/libtopolei_cubical.a", ] -[[lean_exe]] -name = "algebra-restructure" -root = "AlgebraRestructure" -# Phase B/C/D' headless CLI for the restructure algebra -# (ALGEBRA_PLAN §5.3 No-LSP fallback). Subcommands print the -# @[macroAlias] / @[methodology] / @[metaPath] registries. -moreLinkArgs = [ - "./native/cubical/target/release/libtopolei_cubical.a", -] +## No standalone `algebra-restructure` exe. +## The source code IS the CLI: `#eval Algebra.printMethodologies` (etc.) +## inside a Lean session shows the live registry; downstream tooling +## composes the same printer functions however it likes.