Add search guide documentation#49
Open
skylabs-Usama wants to merge 1 commit into
Open
Conversation
SEARCH_GUIDE.md is intended to explain the code to someone unfamiliar with the framework, demonstrate a dry run and also show how to trace success and failure paths.
skylabs-Usama
requested review from
MSS444,
ehtesham-zahoor,
gmalecha-at-skylabs and
sky-rayan
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | 3a1b852 |
| fmdeps/BRiCk/ | main | 05404ad |
| fmdeps/auto/ | main | ed3ad10 |
| fmdeps/auto-docs/ | main | b22de96 |
| bluerock/NOVA/ | skylabs-proof | 220d4a8 |
| bluerock/bhv/ | skylabs-main | 2a6d6bf |
| fmdeps/brick-libcpp/ | main | f36c2bf |
| fmdeps/ci/ | main | 753057b |
| fmdeps/vendored/elpi/ | skylabs-master | aa4475f |
| fmdeps/fm-ci/ | main | cfedfa4 |
| fmdeps/fm-tools/ | main | 6e85551 |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | 291c63e |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | b803c5e |
| fmdeps/vendored/rocq/ | skylabs-master | 6d192b5 |
| fmdeps/vendored/rocq-elpi/ | skylabs-master | e7c8227 |
| fmdeps/vendored/rocq-equations/ | skylabs-main | 737fdf9 |
| fmdeps/vendored/rocq-ext-lib/ | skylabs-master | 8172052 |
| fmdeps/vendored/rocq-iris/ | skylabs-master | 51c753a |
| fmdeps/vendored/rocq-lsp/ | skylabs-main | a8b7272 |
| fmdeps/vendored/rocq-stdlib/ | skylabs-master | 10bd9d7 |
| fmdeps/vendored/rocq-stdpp/ | skylabs-master | 8307c10 |
| fmdeps/skylabs-fm/ | main | 0a313b6 |
| fmdeps/vendored/vsrocq/ | skylabs-main | 39c9c5b |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 121991.5 | 121991.5 | +0.0 | total |
| +0.00% | 24270.5 | 24270.5 | +0.0 | ├ translation units |
| +0.00% | 97721.0 | 97721.0 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 121991.5 | 121991.5 | +0.0 | total |
| +0.00% | 24270.5 | 24270.5 | +0.0 | ├ translation units |
| +0.00% | 97721.0 | 97721.0 | +0.0 | └ proofs and tests |
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | 3a1b852 |
| fmdeps/BRiCk/ | main | 05404ad |
| fmdeps/auto/ | main | ed3ad10 |
| fmdeps/auto-docs/ | main | b22de96 |
| bluerock/NOVA/ | skylabs-proof | 220d4a8 |
| bluerock/bhv/ | skylabs-main | 2a6d6bf |
| fmdeps/brick-libcpp/ | main | f36c2bf |
| fmdeps/ci/ | main | 753057b |
| fmdeps/vendored/elpi/ | skylabs-master | aa4475f |
| fmdeps/fm-ci/ | main | cfedfa4 |
| fmdeps/fm-tools/ | main | 6e85551 |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | 291c63e |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | b803c5e |
| fmdeps/vendored/rocq/ | skylabs-master | 6d192b5 |
| fmdeps/vendored/rocq-elpi/ | skylabs-master | e7c8227 |
| fmdeps/vendored/rocq-equations/ | skylabs-main | 737fdf9 |
| fmdeps/vendored/rocq-ext-lib/ | skylabs-master | 8172052 |
| fmdeps/vendored/rocq-iris/ | skylabs-master | 51c753a |
| fmdeps/vendored/rocq-lsp/ | skylabs-main | a8b7272 |
| fmdeps/vendored/rocq-stdlib/ | skylabs-master | 10bd9d7 |
| fmdeps/vendored/rocq-stdpp/ | skylabs-master | 8307c10 |
| fmdeps/skylabs-fm/ | main | 0a313b6 |
| fmdeps/vendored/vsrocq/ | skylabs-main | 39c9c5b |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 121991.5 | 121991.5 | +0.0 | total |
| +0.00% | 24270.5 | 24270.5 | +0.0 | ├ translation units |
| +0.00% | 97721.0 | 97721.0 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 121991.5 | 121991.5 | +0.0 | total |
| +0.00% | 24270.5 | 24270.5 | +0.0 | ├ translation units |
| +0.00% | 97721.0 | 97721.0 | +0.0 | └ proofs and tests |
skylabs-Usama
commented
Dec 29, 2025
| | **Action** | "How do I execute this action?" | Run `cursor.insert_command("auto.")` | | ||
| | **Frontier** | "Which pending states should I explore next?" | Priority queue ordered by score | | ||
| | **Guidance** | "How promising is this state?" | Fewer remaining goals = better | | ||
| | **Node** | "What's the history of this search path?" | Tracks parent chain, depth, action keys | |
| @@ -0,0 +1,342 @@ | |||
| # Search Module Guide | |||
|
|
|||
Contributor
There was a problem hiding this comment.
This information might be better to put inside the README.md file since it explains how to use the library.
Comment on lines
+159
to
+178
| ## Key Behaviors | ||
|
|
||
| ### SingleDepth Clears on Depth Increase | ||
|
|
||
| When a node at depth N+1 is pushed and `max_depth` is N: | ||
| - The entire frontier is **cleared** | ||
| - Only depth N+1 nodes survive | ||
| - This is the "beam" behavior—discard shallower nodes | ||
|
|
||
| ### PQueue Orders by Score | ||
|
|
||
| - Lower score = higher priority (explored first) | ||
| - Ties broken by insertion order | ||
| - Guidance provides the scoring function | ||
|
|
||
| ### SavingSolutions Tracks Winners | ||
|
|
||
| - Checks `is_solution()` on every push | ||
| - If `stop_on_first_solution=True`, stops search immediately | ||
| - Otherwise, collects all solutions found |
Contributor
There was a problem hiding this comment.
These probably belong in the code.
Comment on lines
+206
to
+223
| ### Running a Search | ||
|
|
||
| ```python | ||
| from rocq_pipeline.search.search.beam import BeamSearch | ||
| from rocq_pipeline.search.rocq.actions import RocqTacticAction | ||
| from rocq_pipeline.search.rocq.manip import RocqManipulator | ||
|
|
||
| search = BeamSearch( | ||
| strategy=my_strategy, | ||
| is_solved=lambda cursor: cursor.current_goal() is None, | ||
| beam_width=5, | ||
| explore_width=10, | ||
| max_depth=50, | ||
| stop_on_first_solution=True, | ||
| freshen=RocqManipulator(), | ||
| ) | ||
|
|
||
| solutions = search.search(initial_cursor) |
Contributor
There was a problem hiding this comment.
We should put these examples inside the source code so that they are type checked. Otherwise, they are likely to bit-rot as the code evolves.
Comment on lines
+287
to
+311
| To capture the complete search tree including failures, use OpenTelemetry-style tracing in `search.py`: | ||
|
|
||
| ```python | ||
| # In search.py process() function | ||
|
|
||
| with trace_context("search_action") as span: | ||
| span.set_attribute("parent.id", id(candidate)) | ||
| span.set_attribute("parent.depth", candidate.depth) | ||
| span.set_attribute("action.key", action_key) | ||
|
|
||
| fresh_state = smanip.copy(candidate.state) | ||
| try: | ||
| next_state = action.interact(fresh_state) | ||
| new_node = Node(next_state, candidate, action_key=action_key) | ||
| worklist.push(new_node, parent) | ||
|
|
||
| span.set_attribute("success", True) | ||
| span.set_attribute("child.id", id(new_node)) | ||
|
|
||
| except Action.Failed as e: | ||
| smanip.dispose(fresh_state) | ||
|
|
||
| span.set_attribute("success", False) | ||
| span.set_attribute("error", e.message or "") | ||
| ``` |
Contributor
There was a problem hiding this comment.
The code should be updated to actually include this. I started this here: #56
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
SEARCH_GUIDE.md is intended to explain the code to someone unfamiliar with the framework, demonstrate a dry run and also show how to trace success and failure paths.
Important if anyone wants to start using this code.
Goals:
Needs to be short enough to read quickly and still know enough about what each component does.