Skip to content

Commit a031ec6

Browse files
authored
feat: client-side for module hierarchy (#620)
This PR adds client-side support for a new module hierarchy component in VS Code that can be used to navigate both the import tree of a module and the imported-by tree of a module. Specifically, it adds a new module hierarchy tree view and 'Module Hierarchy: Show Module Hierarchy' and 'Module Hierarchy: Show Inverse Module Hierarchy' commands to display it for the current file. Companion PR at [leanprover/lean4#8654](leanprover/lean4#8654). ![Imports](https://github.com/user-attachments/assets/74e052e9-cf1a-443e-b429-239c34a61d11) ![Imported by](https://github.com/user-attachments/assets/fe223337-06b3-474a-bf94-2421fccc1dfd) This PR also changes all commands of the extension to exclude the `Category:` prefix from menus.
1 parent 9384651 commit a031ec6

14 files changed

+592
-121
lines changed

README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ After installing this extension, a 'Welcome' page with a setup guide should open
1010
- Setting up a Lean 4 project
1111
- Troubleshooting issues
1212

13-
If the setup guide does not open automatically, you can still open it manually by opening an empty file, clicking on the ∀-symbol in the top right and selecting 'Documentation…' > 'Docs: Show Setup Guide'.
13+
If the setup guide does not open automatically, you can still open it manually by opening an empty file, clicking on the ∀-symbol in the top right and selecting 'Documentation…' > 'Show Setup Guide'.
1414

1515
![Setup guide with instructions for how to re-open the setup guide manually](https://github.com/leanprover/vscode-lean4/raw/HEAD/vscode-lean4/images/setup_guide.png)
1616

vscode-lean4/README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ After installing this extension, a 'Welcome' page with a setup guide should open
1010
- Setting up a Lean 4 project
1111
- Troubleshooting issues
1212

13-
If the setup guide does not open automatically, you can still open it manually by opening an empty file, clicking on the ∀-symbol in the top right and selecting 'Documentation…' > 'Docs: Show Setup Guide'.
13+
If the setup guide does not open automatically, you can still open it manually by opening an empty file, clicking on the ∀-symbol in the top right and selecting 'Documentation…' > 'Show Setup Guide'.
1414

1515
![Setup guide with instructions for how to re-open the setup guide manually](https://github.com/leanprover/vscode-lean4/raw/HEAD/vscode-lean4/images/setup_guide.png)
1616

1.45 KB
Loading

vscode-lean4/media/guide-help.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ If you encounter this issue, you can try disabling your antivirus, re-run the co
77

88
## Collecting VS Code Output
99
If you are encountering an issue with Lean or this VS Code extension, copying the output from the 'Troubleshooting: Show Setup Information' and 'Troubleshooting: Show Output' commands can be helpful for others who are trying to help you.
10-
You can run these commands by clicking on the ∀-symbol in the top right and selecting 'Troubleshooting: Show Setup Information' and 'Troubleshooting: Show Output'.
10+
You can run these commands by clicking on the ∀-symbol in the top right and selecting 'Show Setup Information' and 'Show Output'.
1111

1212
![Troubleshooting](troubleshooting.png)
1313

vscode-lean4/media/guide-setupProject.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
## Creating a Project
22
Below, you will find links that create new projects or download projects for you. After creating or downloading a project, you can re-open the project in the future by clicking the ∀-symbol in the top right, choosing 'Open Project…' > 'Open Local Project…' and selecting the project you created. If possible, you should avoid creating projects on network drives or in directories indexed by cloud storage, e.g. OneDrive.
3-
Completing the project creation process and choosing to open the new project will close this guide. You can re-open it later by clicking the ∀-symbol in the top right and selecting 'Documentation…' > 'Docs: Show Setup Guide'.
3+
Completing the project creation process and choosing to open the new project will close this guide. You can re-open it later by clicking the ∀-symbol in the top right and selecting 'Documentation…' > 'Show Setup Guide'.
44

55
![∀-symbol buttons](open-local-project_show-setup_buttons.png)
66

@@ -10,7 +10,7 @@ If you want to create a new project, click on one of the following:
1010
Dependencies can be added by modifying 'lakefile.lean' in the newly created project as described [here](https://github.com/leanprover/lean4/blob/master/src/lake/README.md#adding-dependencies). You may want to add [Lean's standard library](https://github.com/leanprover/std4) to the list of dependencies.
1111
- [Create a new project using Mathlib](command:lean4.project.createMathlibProject)
1212
The created project will depend on [Mathlib](https://github.com/leanprover-community/mathlib4), the math library of Lean 4. This option is suitable if you want to use Lean 4 for a math formalization project.
13-
To update Mathlib after creating the project, you can click the ∀-symbol in the top right and choose 'Project Actions…' > 'Project: Update Dependency…'.
13+
To update Mathlib after creating the project, you can click the ∀-symbol in the top right and choose 'Project Actions…' > 'Update Dependency…'.
1414

1515
If you want to open an existing project, click on one of the following:
1616
- [Download an existing project](command:lean4.project.clone)
136 Bytes
Loading
1.03 KB
Loading
-7.65 KB
Loading

vscode-lean4/package.json

Lines changed: 204 additions & 107 deletions
Large diffs are not rendered by default.

vscode-lean4/src/extension.ts

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ import { displayInternalErrorsIn } from './utils/internalErrors'
2626
import { registerLeanCommandRunner } from './utils/leanCmdRunner'
2727
import { lean, registerLeanEditorProvider } from './utils/leanEditorProvider'
2828
import { LeanInstaller } from './utils/leanInstaller'
29+
import { ModuleTreeViewProvider } from './utils/moduleTreeViewProvider'
2930
import {
3031
displayActiveStickyNotification,
3132
displayModalNotification,
@@ -207,6 +208,8 @@ async function activateLean4Features(
207208
clientProvider,
208209
)
209210

211+
context.subscriptions.push(await ModuleTreeViewProvider.init(clientProvider))
212+
210213
await setLeanFeatureSetActive(true)
211214

212215
return { clientProvider, infoProvider, projectOperationProvider }

0 commit comments

Comments
 (0)