[Merged by Bors] - feat(ImportGraph): add option to exclude tactics#6153
[Merged by Bors] - feat(ImportGraph): add option to exclude tactics#6153joneugster wants to merge 10 commits intomasterfrom
Conversation
|
bors d+ (Obviously wait until the earlier PR has been updated and approved! :-) |
|
✌️ joneugster can now approve this pull request. To approve and merge a pull request, simply reply with |
|
This PR/issue depends on: |
|
@semorrison in case you'd like to skim over the modifications I made while resolving merge conflicts:
|
|
I'm slightly concerned that someone somewhere will try to use |
|
bors merge |
Add an option `lake exe graph --excludeMeta` which removes all nodes that start with `Mathlib.[Tactic|Lean|Util]`
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
That's why I added the French quotes at least. I considered something like |
Add an option `lake exe graph --excludeMeta` which removes all nodes that start with `Mathlib.[Tactic|Lean|Util]`
Add an option `lake exe graph --excludeMeta` which removes all nodes that start with `Mathlib.[Tactic|Lean|Util]`
Add an option
lake exe graph --excludeMetawhich removes all nodes that start withMathlib.[Tactic|Lean|Util]Implementation note: in replacement of all deleted nodes it adds a single node
Mathlib.Tacticswhich is added as import to any node importing a deleted node. To avoid loops, this new node does not receive any imports from any other Mathlib files:For example, there are imports
Mathlib.Tactic.X → Mathlib.Init.Logic → Mathlib.Tactic.Y, so my approach now is to only displayMathlib.Tactics → Mathlib.Init.Logic