cli

Author: denisecase

CHANGELOG.md

@@ -187,6 +187,8 @@ git tag -d vX.Z.Y
 git push origin :refs/tags/vX.Z.Y
 ```
 
+## Links
+
 [Unreleased]: https://github.com/structural-explainability/se-theory-neutral-substrate/compare/v0.5.0...HEAD
 [0.5.0]: https://github.com/structural-explainability/se-theory-neutral-substrate/compare/v0.3.0...v0.5.0
 [0.4.0]: https://github.com/structural-explainability/se-theory-neutral-substrate/compare/v0.3.0...v0.4.0

README.md

@@ -82,6 +82,9 @@ import NeutralSubstrate
 
 ## Build
 
+Use VS Code Menu:
+View / Command Palette / `Developer: Reload Window` to refresh.
+
 ```shell
 elan self update
 lake update
@@ -135,21 +138,20 @@ uvx pre-commit run --all-files
 git add -A
 uvx pre-commit run --all-files
 
-uv run se-manifest-validate
-uv run se-manifest-validate --strict
-uv run se-manifest-validate --require-tag
-
-uv run se-manifest-version-sync
-
+# OPTIONAL:
 # Scaffold reference/ artifacts from Lean 4 source.
-# Adds stubs for new symbols. Preserves existing descriptions and cite_ids.
-uv run se-ref-scaffold
+# Adds stubs for new symbols.
+# Preserves existing descriptions, names, and cite_ids.
 uv run se-ref-scaffold --dry-run
+uv run se-ref-scaffold
+
+# OPTIONAL OVERWRITE:
+# Use carefully. Re-derives scaffolded fields and may overwrite
+# existing descriptions, names, and cite_ids.
 uv run se-ref-scaffold --overwrite
 
-# Validate reference/ artifacts against Lean 4 source. Writes nothing.
-uv run se-ref-validate
-uv run se-ref-validate --strict
+# IMPORTANT: Run checks
+uv run se-validate --strict
 
 # do chores
 uv run python -m pyright

pyproject.toml

@@ -40,7 +40,8 @@ docs = [
 ]
 
 [project.scripts]
-se-manifest-validate = "se_theory_neutral_substrate.cli:validate_main"
+se-validate = "se_theory_neutral_substrate.cli:validate_main"
+se-manifest-schema-validate = "se_theory_neutral_substrate.cli:schema_validate_main"
 se-manifest-version-sync = "se_theory_neutral_substrate.cli:sync_main"
 se-ref-scaffold = "se_theory_neutral_substrate.cli:ref_scaffold_main"
 se-ref-validate = "se_theory_neutral_substrate.cli:ref_validate_main"

src/se_theory_neutral_substrate/cli.py

@@ -1,34 +1,31 @@
-"""cli.py - Command-line interface for se-manifest-schema.
+"""cli.py - Command-line interface for se-theory-identity-regimes.
 
-Parses arguments and dispatches to orchestrate.py or sync.py.
-Owns nothing except argument parsing and error handling.
-All logic lives in orchestrate.py and sync.py.
+Parses arguments and dispatches to repository validation, manifest-schema
+validation, version sync, and reference artifact tooling.
 
 Entry points:
-  uv run se-manifest-validate
-  uv run se-manifest-validate --strict
-  uv run se-manifest-validate --require-tag
+  uv run se-validate
+  uv run se-validate --strict
+  uv run se-validate --require-tag
+
+  uv run se-manifest-schema-validate
+  uv run se-manifest-schema-validate --strict
+  uv run se-manifest-schema-validate --require-tag
 
   uv run se-manifest-version-sync
 
-  uv run se-ref-scaffold
   uv run se-ref-scaffold --dry-run
+  uv run se-ref-scaffold
   uv run se-ref-scaffold --overwrite
 
   uv run se-ref-validate
   uv run se-ref-validate --strict
-
-Call chain:
-  __main__.py -> cli.main()
-              -> orchestrate.run_validate()  (sync_all called internally)
-              -> sync.sync_all()             (sync only, no validation)
-              -> reference.run_scaffold()     (scaffold + validate reference/)
-              -> reference.run_ref_validate() (validate reference/ only)
 """
 
 import argparse
 import sys
 
+from se_manifest_schema.orchestrate import run_validate as run_validate_manifest
 from se_manifest_schema.sync import sync_all
 
 from se_theory_neutral_substrate.orchestrate import run_validate
@@ -43,9 +40,10 @@ def build_parser() -> argparse.ArgumentParser:
     )
     subparsers = parser.add_subparsers(dest="command")
 
+    # -- validate ------------------------------------------------------------
     validate_parser = subparsers.add_parser(
         "validate",
-        help="Sync and validate manifest-schema.toml and SE_MANIFEST.toml.",
+        help="Run full repository validation.",
     )
     validate_parser.add_argument(
         "--strict",
@@ -58,12 +56,29 @@ def build_parser() -> argparse.ArgumentParser:
         help="Require CITATION.cff version to match current git tag.",
     )
 
+    # -- schema-validate -----------------------------------------------------
+    schema_validate_parser = subparsers.add_parser(
+        "schema-validate",
+        help="Validate only the manifest schema layer.",
+    )
+    schema_validate_parser.add_argument(
+        "--strict",
+        action="store_true",
+        help="Treat warnings as errors.",
+    )
+    schema_validate_parser.add_argument(
+        "--require-tag",
+        action="store_true",
+        help="Require CITATION.cff version to match current git tag.",
+    )
+
+    # -- sync ----------------------------------------------------------------
     subparsers.add_parser(
         "sync",
         help="Sync pyproject.toml fallback-version from CITATION.cff version.",
     )
 
-    # -- ref-scaffold -------------------------------------------------------------
+    # -- ref-scaffold --------------------------------------------------------
     ref_scaffold_parser = subparsers.add_parser(
         "ref-scaffold",
         help=(
@@ -83,7 +98,7 @@ def build_parser() -> argparse.ArgumentParser:
         help="Overwrite existing descriptions, names, and cite_ids with re-derived values.",
     )
 
-    # -- ref-validate ---------------------------------------------------------
+    # -- ref-validate --------------------------------------------------------
     ref_validate_parser = subparsers.add_parser(
         "ref-validate",
         help=(
@@ -94,19 +109,24 @@ def build_parser() -> argparse.ArgumentParser:
     ref_validate_parser.add_argument(
         "--strict",
         action="store_true",
-        help="Treat warnings (orphaned symbols, missing stubs) as errors.",
+        help="Treat warnings as errors.",
     )
 
     return parser
 
 
 def validate_main() -> int:
-    """Validate the manifest schema and sync if needed. Returns 0 on success, 1 on error."""
+    """Run full repository validation. Returns 0 on success, 1 on error."""
     return main(["validate"] + sys.argv[1:])
 
 
+def schema_validate_main() -> int:
+    """Validate only the manifest schema layer. Returns 0 on success, 1 on error."""
+    return main(["schema-validate"] + sys.argv[1:])
+
+
 def sync_main() -> int:
-    """Sync the manifest schema. Returns 0 on success, 1 on error."""
+    """Sync version metadata. Returns 0 on success, 1 on error."""
     return main(["sync"] + sys.argv[1:])
 
 
@@ -124,7 +144,7 @@ def main(argv: list[str] | None = None) -> int:
     """Run the command-line interface.
 
     Returns:
-        0 on success, 1 on error, 2 if no command given.
+        0 on success, 1 on error, 2 if no command is given.
     """
     parser = build_parser()
     args = parser.parse_args(argv)
@@ -135,14 +155,23 @@ def main(argv: list[str] | None = None) -> int:
                 strict=args.strict,
                 require_tag=args.require_tag,
             )
+
+        if args.command == "schema-validate":
+            return run_validate_manifest(
+                strict=args.strict,
+                require_tag=args.require_tag,
+            )
+
         if args.command == "sync":
             sync_all()
             return 0
+
         if args.command == "ref-scaffold":
             return run_scaffold(
                 dry_run=args.dry_run,
                 overwrite=args.overwrite,
             )
+
         if args.command == "ref-validate":
             return run_ref_validate(
                 strict=args.strict,

src/se_theory_neutral_substrate/reference.py

@@ -123,6 +123,42 @@ def _infer_core_module(surface_module: str) -> str:
     return surface_module.replace("Surface", "Core")
 
 
+def _path_to_module(path: Path, lean_root: Path) -> str:
+    rel = path.relative_to(lean_root).with_suffix("")
+    return ".".join(rel.parts)
+
+
+def _infer_core_modules(surface_module: str, lean_root: Path) -> list[str]:
+    """Infer Core modules under the surface namespace.
+
+    Supports both layouts:
+
+    - MyLib/Core.lean -> MyLib.Core
+    - MyLib/Profile/Core.lean -> MyLib.Profile.Core
+    - MyLib/Transform/Core.lean -> MyLib.Transform.Core
+
+    The root Core.lean file is sorted first when present, followed by
+    nested Core.lean files in deterministic path order.
+    """
+    if not surface_module.endswith(".Surface"):
+        return []
+
+    root_module = surface_module.removesuffix(".Surface")
+    root_dir = lean_root.joinpath(*root_module.split("."))
+
+    if not root_dir.exists():
+        return []
+
+    core_files = sorted(root_dir.rglob("Core.lean"))
+
+    root_core = root_dir / "Core.lean"
+    if root_core in core_files:
+        core_files.remove(root_core)
+        core_files.insert(0, root_core)
+
+    return [_path_to_module(path, lean_root) for path in core_files]
+
+
 def _kind_to_section(artifact_kind: str) -> str:
     """'substrate-type-registry' -> 'type', 'se-theorem-registry' -> 'theorem'."""
     without_suffix = artifact_kind.removesuffix("-registry")
@@ -303,9 +339,13 @@ def _process_artifact(
         source_modules = _source_modules_in_registry(existing_data)
     if not source_modules:
         surface = existing_data.get("surface_module", index_surface_module)
-        derived = _infer_core_module(surface)
-        source_modules = [derived]
-        result.note(f"source module inferred: {derived}")
+        source_modules = _infer_core_modules(surface, lean_root)
+        if source_modules:
+            result.note("source modules inferred: " + ", ".join(source_modules))
+        else:
+            derived = surface.replace("Surface", "Core")
+            source_modules = [derived]
+            result.note(f"source module inferred: {derived}")
 
     # Scan Lean files
     all_decls: list[LeanDecl] = []