feat: Add per-node subgraph generation for dependency graphs#88
Open
Blackfeather007 wants to merge 10 commits intoPatrickMassot:masterfrom
Open
feat: Add per-node subgraph generation for dependency graphs#88Blackfeather007 wants to merge 10 commits intoPatrickMassot:masterfrom
Blackfeather007 wants to merge 10 commits intoPatrickMassot:masterfrom
Conversation
- Add monkey patching to extend DepGraph class with subgraph() method
- Generate individual subgraph HTML files for each node showing its dependencies
- Add SUBGRAPH_LINK_TPL to display subgraph links in node modals
- Support querying subgraphs via URL (subgraph_{node_id}.html)
- All changes are contained within leanblueprint package, no modifications to plastexdepgraph
- Add checks for dependency graph existence before processing - Add detailed logging to help diagnose issues - Fix options access by getting from document.userdata instead of closure - Add traceback logging for better error debugging - Log number of graphs found, nodes processed, and files generated
- Remove verbose debug print statements - Remove detailed section-by-section logging - Keep only essential info: graph count, node count, and generated file count - Simplify error handling to single warning message
Feature/subgraph generation
- Add --subgraph option to 'leanblueprint web' command - Only generate subgraph HTML files when --subgraph flag is provided - Use environment variable LEANBLUEPRINT_SUBGRAPH to pass flag to ProcessOptions - Default behavior (without flag) does not generate subgraphs
feat: Add --subgraph flag to web command
fix: parser and trivial graph
|
I was looking for this feature! I hope that it get merged soon... |
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
3 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.
Summary
This PR adds a subgraph generation feature that creates individual dependency graph pages for each node, showing the node and all its ancestors (dependencies).
Features
subgraph()method toDepGraphclass that returns a new graph containing a node and all its ancestorssubgraph_<node_id>.html) for each node in the dependency graphUsage
or
Remark
This is just a small feature I developed in my formalization project to make the theorems I'm interested in clearer. Hope this helps. 😄