-
Notifications
You must be signed in to change notification settings - Fork 10
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
57b4b98
commit a6b4849
Showing
1 changed file
with
25 additions
and
1 deletion.
There are no files selected for viewing
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1 +1,25 @@ | ||
# lean-graph | ||
# lean-graph | ||
|
||
A simple tool to create import graphs of lake packages. | ||
|
||
|
||
## Requirements | ||
|
||
For creating different output formats than `.dot` (for example to create a `.pdf` file), you should have `graphviz` installed. | ||
|
||
## Usage | ||
|
||
You can import this in any lean projects by the following line to your `lakefile.lean`: | ||
|
||
```lean | ||
require importGraph from git "https://github.com/leanprover-community/lean-graph" @ "main" | ||
``` | ||
|
||
After running `lake update -R importGraph` in your project, you can create import graphs with | ||
|
||
```bash | ||
lake exe graph | ||
``` | ||
|
||
A typical command is `lake exe graph --reduce --to MyModule my_graph.pdf` where `MyModule` follows the same module naming you would use to `import` it in lean. | ||
See `lake exe graph --help` for more options. |