max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Elab
History
Marc Huisinga 91b5e19833
feat: server-side for module hierarchy (#8654) 
This PR adds server-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 implements new
requests `$/lean/prepareModuleHierarchy`,
`$/lean/moduleHierarchy/imports` and
`$/lean/moduleHierarchy/importedBy`. These requests are not supported by
standard LSP. Companion PR at
[leanprover/vscode-lean4#620](https://github.com/leanprover/vscode-lean4/pull/620).


![Imports](https://github.com/user-attachments/assets/5ef650e7-3b0e-4a33-9ecb-f442bff88006)
![Imported
by](https://github.com/user-attachments/assets/d98e7a2c-3c4f-4509-afdf-08134a97aa78)

### Breaking changes
This PR augments the .ilean format with the direct imports of a file in
order to implement the `$/lean/moduleHierarchy/importedBy` request and
bumps the .ilean format version.
2025-06-11 08:02:18 +00:00
..
Deriving feat: do not export private declarations (#8337) 2025-06-02 08:01:08 +00:00
InfoTree feat: signature help (#8511) 2025-06-03 17:26:33 +00:00
PreDefinition feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
Quotation feat: reserved names (#3675) 2024-03-15 00:33:22 +00:00
Tactic chore: fix spelling mistakes (#8711) 2025-06-10 20:24:28 +00:00
App.lean fix: invalid field notation error for mvar (#8259) 2025-06-01 03:02:04 +00:00
Arg.lean chore: rename Array.back to back! (#5897) 2024-10-31 09:18:18 +00:00
Attributes.lean chore: fix linter errors (#4502) 2024-06-19 18:24:08 +00:00
AutoBound.lean doc: fix option name (#5150) 2024-08-25 07:16:44 +00:00
AuxDef.lean feat: create private aux decls in private contexts 2025-06-03 15:53:05 +02:00
BinderPredicates.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Binders.lean feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
BindersUtil.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
BuiltinCommand.lean feat: do not export private declarations (#8337) 2025-06-02 08:01:08 +00:00
BuiltinEvalCommand.lean feat: do not export private declarations (#8337) 2025-06-02 08:01:08 +00:00
BuiltinNotation.lean feat: debug_assert! (#7256) 2025-03-03 16:34:44 +00:00
BuiltinTerm.lean feat: do not export private declarations (#8337) 2025-06-02 08:01:08 +00:00
Calc.lean chore: add missing diff-exposing in type/value mismatch errors (#6484) 2024-12-31 17:47:12 +00:00
CheckTactic.lean chore: add missing diff-exposing in type/value mismatch errors (#6484) 2024-12-31 17:47:12 +00:00
Command.lean feat: revamp aux decl name generation (#8363) 2025-05-16 14:57:18 +00:00
ComputedFields.lean feat: do not export def bodies by default (#8221) 2025-05-15 12:16:54 +00:00
Config.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Declaration.lean fix: unknown identifier ranges (#8362) 2025-05-22 10:05:31 +00:00
DeclarationRange.lean feat: inlay hints for auto-implicits (#6768) 2025-02-04 17:36:49 +00:00
DeclModifiers.lean chore: do not interpret meta as noncomputable (#8668) 2025-06-07 09:45:04 +00:00
DeclNameGen.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
DeclUtil.lean feat: localize universe metavariable errors at let bindings and fun binders (#5402) 2024-09-24 05:30:42 +00:00
DefView.lean feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
Deriving.lean feat: upstream ToExpr deriving handler from Mathlib (#6473) 2024-12-31 15:11:53 +00:00
Do.lean chore: fixes after rebootstrap 2025-06-04 18:26:05 +02:00
ElabRules.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Eval.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Exception.lean feat: incremental elaboration of definition headers, bodies, and tactics (#3940) 2024-05-22 13:23:30 +00:00
Extra.lean fix: unknown identifier ranges (#8362) 2025-05-22 10:05:31 +00:00
Frontend.lean feat: server-side for module hierarchy (#8654) 2025-06-11 08:02:18 +00:00
GenInjective.lean feat: reserved names (#3675) 2024-03-15 00:33:22 +00:00
GuardMsgs.lean feat: make guard_msgs.diff=true the default (#8596) 2025-06-03 15:13:15 +00:00
Import.lean feat: server-side for module hierarchy (#8654) 2025-06-11 08:02:18 +00:00
Inductive.lean feat: improve inductive type parameter error messages (#8338) 2025-05-19 17:03:49 +00:00
InfoTree.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
InfoTrees.lean feat: allow async elab tasks to contribute to info trees reported to linters and request handlers (#7457) 2025-03-13 15:09:00 +00:00
InheritDoc.lean feat: language reference links and examples in docstrings (#7240) 2025-03-12 09:17:27 +00:00
LetRec.lean feat: language reference links and examples in docstrings (#7240) 2025-03-12 09:17:27 +00:00
Level.lean chore: rename Array.back to back! (#5897) 2024-10-31 09:18:18 +00:00
Macro.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
MacroArgUtil.lean feat: quotations for parser aliases (#4307) 2024-05-30 09:22:22 +00:00
MacroRules.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Match.lean feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
MatchAltView.lean feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
MatchExpr.lean perf: match_expr join points (#3580) 2024-03-03 18:15:49 +00:00
Mixfix.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
MutualDef.lean feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
MutualInductive.lean feat: do not export private declarations (#8337) 2025-06-02 08:01:08 +00:00
Notation.lean chore: use Array.findFinIdx? where it is better than findIdx? (#6184) 2024-11-23 07:22:31 +00:00
Open.lean chore: avoid runtime array bounds checks (#6134) 2024-11-21 05:04:52 +00:00
ParseImportsFast.lean feat: lake: use lean --setup (#8447) 2025-06-08 17:42:45 +00:00
PatternVar.lean feat: improve error messages in invalid match alternatives (#8368) 2025-05-19 17:40:41 +00:00
PreDefinition.lean feat: generate f.eq_unfold lemmas (#5141) 2024-08-29 16:47:40 +00:00
Print.lean feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
Quotation.lean feat: deprecate Array.mkArray in favour of Array.replicate 2025-03-24 08:25:00 +01:00
RecAppSyntax.lean chore: fix spelling mistakes in src/Lean/Elab/ (#5435) 2024-09-23 21:58:16 +00:00
RecommendedSpelling.lean feat: recommended_spelling command (#6869) 2025-02-03 11:15:52 +00:00
SetOption.lean chore: generalize some type classes (#7611) 2025-04-07 01:10:19 +00:00
StructInst.lean feat: := private instance syntax 2025-05-28 10:18:04 +02:00
Structure.lean chore: fix spelling mistakes (#8324) 2025-05-14 06:52:16 +00:00
Syntax.lean chore: avoid runtime array bounds checks (#6134) 2024-11-21 05:04:52 +00:00
SyntheticMVars.lean feat: create private aux decls in private contexts 2025-06-03 15:53:05 +02:00
Tactic.lean chore: cleanup after renaming get_elem_tactic_trivial 2025-06-06 13:10:18 +10:00
Term.lean chore: fixes after rebootstrap 2025-06-04 18:26:05 +02:00
Time.lean chore: upstream #time command (#5044) 2024-08-15 00:17:48 +00:00
Util.lean fix: convert kernel interrupt into elab interrupt (#6988) 2025-02-07 15:55:32 +00:00