docs: align set_goal docs with append semantics (W-405)

README.md

@@ -64,7 +64,7 @@ assert repl.get_num_goals(s4) == 0
 | Method | Behavior |
 |---|---|
 | `Repl(module="Lean")` | import a module (dot-separated names, or a `.lean` file path whose top-level commands are elaborated) into a fresh environment |
-| `Repl.set_goal(type_str)` | parse + elaborate a term as the root goal type; returns state 0 |
+| `Repl.set_goal(type_str)` | parse + elaborate a term as a new root goal state (existing states unaffected); returns the new state's id (`0` for the first call in a fresh session) |
 | `Repl.run_tac(state, tactic, goal_idx=0)` | apply a tactic to the `goal_idx`-th goal; unworked goals are preserved in the new state |
 | `Repl.run_tacs(state, tactics, goal_idx=0)` | apply a tactic sequence in order, one call end to end; returns the final state id |
 | `Repl.try_run_tac(state, tactic, goal_idx=0)` | non-raising `run_tac`: returns `(state_id, success)` — the new state and `True` on success, the source state and `False` on failure (no state appended); the session stays usable. The core idiom for proof-search / RL loops |

python/leotower/__init__.py

@@ -135,7 +135,11 @@ def __init__(self, module: str = "Lean"):
 
     # -- state management ---------------------------------------------------
     def set_goal(self, type_str: str) -> int:
-        """Set the root goal from a term string; returns state 0."""
+        """Create a new root goal state from a term string.
+
+        Existing states are unaffected; returns the new state's id (``0``
+        for the first call in a fresh session).
+        """
         try:
             return self._repl.set_goal(type_str)
         except RuntimeError as e:

src/lib.rs

@@ -265,11 +265,12 @@ impl Repl {
         .map_err(to_py_err)
     }
 
-    /// Set the root goal from a term string. The type is elaborated by
-    /// Lean's real elaborator through the `suffices` tactic: create a `True`
-    /// goal and replace it with `type_str` (`suffices h : t from True.intro`
-    /// — the `from` proof is `True.intro`, the target type is the new goal).
-    /// Returns state 0.
+    /// Create a new root goal state from a term string. The type is
+    /// elaborated by Lean's real elaborator through the `suffices` tactic:
+    /// create a `True` goal and replace it with `type_str` (`suffices h : t
+    /// from True.intro` — the `from` proof is `True.intro`, the target type
+    /// is the new goal). Existing states are unaffected; returns the new
+    /// state's id (0 for the first call in a fresh session).
     fn set_goal(&mut self, type_str: &str) -> PyResult<u64> {
         leo3::with_lean(|lean| -> LeanResult<u64> {
             let mut metam = self.rebind(lean)?;

tests/test_repl.py

@@ -71,6 +71,35 @@ def test_set_goal_and_queries():
     assert "⊢" in pp
 
 
+def test_set_goal_appends_independent_root_states():
+    """set_goal appends a new root state per call: a second call in the
+    same session returns the next id (1), not 0, and the two root states
+    stay independent — proving one does not touch the other."""
+    repl = Repl()
+    s0 = repl.set_goal(ADD_COMM)
+    assert s0 == 0
+    s1 = repl.set_goal("2 + 2 = 4")
+    assert s1 == 1
+    assert repl.num_states() == 2
+    # Each root state keeps its own goal; the first is untouched by the
+    # second set_goal.
+    assert repl.get_num_goals(s0) == 1
+    assert "n + m = m + n" in repl.get_goal_pp(s0)
+    assert repl.get_num_goals(s1) == 1
+    assert "2 + 2 = 4" in repl.get_goal_pp(s1)
+    # The states are independent: proving s1 leaves s0 fully intact.
+    s2 = repl.run_tac(s1, "rfl")
+    assert repl.get_num_goals(s2) == 0
+    assert repl.get_num_goals(s0) == 1
+    assert "n + m = m + n" in repl.get_goal_pp(s0)
+    # A third call appends again (state 3 — run_tac above took state 2),
+    # still independent of the rest.
+    s3 = repl.set_goal("True")
+    assert s3 == 3
+    assert repl.num_states() == 4
+    assert repl.get_num_goals(s3) == 1
+
+
 def test_run_tac_steps():
     repl = Repl()
     s0 = repl.set_goal(ADD_COMM)