doc: hide deps from the public lean-beam surface (#10)

* doc: hide deps from the public lean-beam surface

* doc: clarify deps alias risk

Author: ejgallego

Beam/Cli.lean

@@ -1451,7 +1451,6 @@ private def usage : String :=
     "  beam [--root PATH] [--socket PATH | --port N] lean-run-with <path> <handle-json|-|--handle-file <path>> [--stdin | --text-file <path> | -- <text...> | <text...>]",
     "  beam [--root PATH] [--socket PATH | --port N] lean-run-with-linear <path> <handle-json|-|--handle-file <path>> [--stdin | --text-file <path> | -- <text...> | <text...>]",
     "  beam [--root PATH] [--socket PATH | --port N] lean-release <path> <handle-json|-|--handle-file <path>>",
-    "  beam [--root PATH] [--socket PATH | --port N] lean-deps <path>",
     "  beam [--root PATH] [--socket PATH | --port N] lean-sync <path> [+full]",
     "  beam [--root PATH] [--socket PATH | --port N] lean-refresh <path> [+full]",
     "  beam [--root PATH] [--socket PATH | --port N] lean-save <path> [+full]",
@@ -1495,6 +1494,7 @@ private def printExperimentalInfo (home : System.FilePath) : IO Unit := do
   IO.println s!"Experimental expert commands live in {doc}"
   IO.println "This is an unstable broker escape hatch, not part of the stable runAt contract."
   IO.println "Current experimental entry point: lean-request-at"
+  IO.println "Unsupported or broken compatibility aliases may still exist for tests; they are not part of the supported or experimental surface."
 
 private def runLeanRunAt
     (home : System.FilePath)

docs/experimental.md

@@ -8,6 +8,11 @@ broker-side conveniences for debugging and exploration.
 `lean-beam request-at` is an unstable broker escape hatch for expert debugging. It does not widen the
 stable `runAt` contract.
 
+Some unsupported or broken compatibility extensions may still exist in the tree for tests or local
+maintainer workflows. Treat those as implementation leftovers, not as experimental API candidates.
+The current example is the hidden `lean-deps` compatibility alias: you can use it at your own risk
+to extract full deps, but there are no guarantees and the information is likely broken.
+
 ## `lean-beam request-at`
 
 `lean-beam request-at` forwards a small whitelisted set of standard Lean LSP requests against the current

scripts/lean-beam

@@ -18,7 +18,6 @@ usage:
   lean-beam [--root PATH] [--socket PATH | --port N] run-with <path> <handle-json|-|--handle-file <path>> [--stdin | --text-file <path> | -- <text...> | <text...>]
   lean-beam [--root PATH] [--socket PATH | --port N] run-with-linear <path> <handle-json|-|--handle-file <path>> [--stdin | --text-file <path> | -- <text...> | <text...>]
   lean-beam [--root PATH] [--socket PATH | --port N] release <path> <handle-json|-|--handle-file <path>>
-  lean-beam [--root PATH] [--socket PATH | --port N] deps <path>
   lean-beam [--root PATH] [--socket PATH | --port N] sync <path> [+full]
   lean-beam [--root PATH] [--socket PATH | --port N] refresh <path> [+full]
   lean-beam [--root PATH] [--socket PATH | --port N] save <path> [+full]

skills/lean-beam/SKILL.md

@@ -42,7 +42,7 @@ Supported command families:
 
 - bootstrap the Lean backend: `lean-beam ensure`
 - inspect existing code or proof state: `lean-beam hover`, `lean-beam goals-prev`, `lean-beam goals-after`
-- inspect file, dependency, or daemon state: `lean-beam deps`, `lean-beam open-files`, `lean-beam doctor`, `lean-beam stats`,
+- inspect file or daemon state: `lean-beam open-files`, `lean-beam doctor`, `lean-beam stats`,
   `lean-beam reset-stats`
 - try one isolated speculative Lean snippet: `lean-beam run-at`
 - continue from one exact speculative state: `lean-beam run-at-handle`, `lean-beam run-with`,
@@ -54,7 +54,7 @@ What to treat as the default public skill surface:
 
 - default and stable enough for normal use: `lean-beam hover`, `lean-beam goals-prev`, `lean-beam goals-after`,
   `lean-beam run-at`, `lean-beam sync`, `lean-beam refresh`
-- narrower but supported wrapper surface: `lean-beam deps`, `lean-beam open-files`, `lean-beam doctor`,
+- narrower but supported wrapper surface: `lean-beam open-files`, `lean-beam doctor`,
   `lean-beam stats`, `lean-beam reset-stats`, `lean-beam save`, `lean-beam close-save`
 - alpha support APIs: `lean-beam run-at-handle`, `lean-beam run-with`, `lean-beam run-with-linear`,
   `lean-beam release`, `lean-beam-search`

skills/lean-beam/references/workflow-details.md

@@ -51,12 +51,6 @@ printf '%s\n' "$HANDLE_JSON" | lean-beam-search playout "Foo.lean" "exact trivia
 printf '%s\n' "$HANDLE_JSON" | lean-beam-search release "Foo.lean"
 ```
 
-Inspect dependency order for multi-file edits:
-
-```bash
-lean-beam deps "Foo.lean"
-```
-
 Inspect Lean type/term information at a specific position:
 
 ```bash
@@ -101,7 +95,7 @@ What is not a valid checkpoint target:
 
 ## Source-File And Execution Model
 
-- `lean-beam run-at` and `lean-beam deps` do not edit `Foo.lean`
+- `lean-beam run-at` does not edit `Foo.lean`
 - `lean-beam hover` is the stable read-only semantic inspection command for an existing position
 - `lean-beam goals-prev` and `lean-beam goals-after` are the stable read-only proof-state
   inspection commands for an existing tactic position
@@ -210,7 +204,6 @@ lean-beam refresh "T.lean"
 
 Practical boundary:
 
-- use `lean-beam deps "T.lean"` to inspect direct imports when choosing likely upstream modules
 - this is a targeted recovery loop, not a full dependency scheduler
 - if retries keep walking additional modules, or if you need final workspace trust, stop and run
   `lake build`
@@ -244,8 +237,6 @@ itself to prove the dependency cone is fresh.
 
 ```bash
 lean-beam ensure
-lean-beam deps "B.lean"
-
 # make a real edit in A.lean and save the source file to disk
 lean-beam sync "A.lean"
 lean-beam run-at "B.lean" 12 2 "#check someNameFromA"

tests/test-beam-wrapper.sh

@@ -745,35 +745,35 @@ EOF
   cd "$tmp3"
   deps_out="$("$beam_script" lean-deps SaveSmoke/A.lean)"
   if [ "$(RUNAT_JSON_PAYLOAD="$deps_out" read_json_text_field ok)" != "true" ]; then
-    echo "expected wrapper lean-deps to succeed despite unrelated broken files" >&2
+    echo "expected hidden lean-deps compatibility alias to succeed despite unrelated broken files" >&2
     printf '%s\n' "$deps_out" >&2
     exit 1
   fi
   if ! printf '%s\n' "$deps_out" | grep -q '"name": "SaveSmoke.B"'; then
-    echo "expected lean-deps imports to include SaveSmoke.B" >&2
+    echo "expected hidden lean-deps compatibility alias imports to include SaveSmoke.B" >&2
     printf '%s\n' "$deps_out" >&2
     exit 1
   fi
   if ! printf '%s\n' "$deps_out" | grep -q '"name": "SaveSmoke"'; then
-    echo "expected lean-deps importedBy to include SaveSmoke" >&2
+    echo "expected hidden lean-deps compatibility alias importedBy to include SaveSmoke" >&2
     printf '%s\n' "$deps_out" >&2
     exit 1
   fi
   stats_out="$("$beam_script" stats)"
   if [ "$(RUNAT_JSON_PAYLOAD="$stats_out" read_json_text_field result.sessions.lean.active)" != "false" ]; then
-    echo "expected lean-deps not to start a live Lean session" >&2
+    echo "expected hidden lean-deps compatibility alias not to start a live Lean session" >&2
     printf '%s\n' "$stats_out" >&2
     exit 1
   fi
   session_starts="$(RUNAT_JSON_PAYLOAD="$stats_out" read_json_text_field result.byBackend.lean.sessionStarts)"
   if [ "${session_starts:-0}" -ne 0 ]; then
-    echo "expected lean-deps not to start any Lean sessions" >&2
+    echo "expected hidden lean-deps compatibility alias not to start any Lean sessions" >&2
     printf '%s\n' "$stats_out" >&2
     exit 1
   fi
   deps_count="$(RUNAT_JSON_PAYLOAD="$stats_out" read_json_text_field result.byBackend.lean.ops.deps.count)"
   if [ "${deps_count:-0}" -lt 1 ]; then
-    echo "expected lean-deps stats to record at least one deps request" >&2
+    echo "expected hidden lean-deps compatibility alias stats to record at least one deps request" >&2
     printf '%s\n' "$stats_out" >&2
     exit 1
   fi