Skip to content

Declaration information extraction #119

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 23 commits into
base: master
Choose a base branch
from
Open

Declaration information extraction #119

wants to merge 23 commits into from

Conversation

@augustepoiroux
Copy link
Contributor

@augustepoiroux augustepoiroux commented Jul 9, 2025 •
edited
Loading

Extract various information about declarations in commands through the "declarations": true attribute:

  • Kind: definition, theorem, inductive, ...
  • Modifiers: docstring, visibility (private, protected, ...), computeKind ("meta", "noncomputable", ...), recKind ("partial", "nonrec", ...), isUnsafe, and attributes
  • Type (= conclusion for theorems)
  • Binders (= variables/hypotheses for theorems)
  • Signature (= binder + type)
  • Value (= proof for theorems)
  • Scope information: current namespace, declared variables, ...

TODO:

  • Improving the extraction of used constants.
  • Improving the extraction of declaration full names (they should match the ones in the environment).

Contributions and feedback are welcome!

Notes:

@augustepoiroux augustepoiroux force-pushed the declaration-extraction branch from e743bce to 9734b35 Compare July 24, 2025 07:41
@augustepoiroux augustepoiroux force-pushed the declaration-extraction branch 2 times, most recently from 494cc23 to 8e5cc95 Compare August 15, 2025 11:43
@augustepoiroux augustepoiroux mentioned this pull request Sep 25, 2025
Open
@augustepoiroux augustepoiroux marked this pull request as ready for review September 25, 2025 15:57
@augustepoiroux augustepoiroux mentioned this pull request Oct 12, 2025
Merged
augustepoiroux added a commit to augustepoiroux/LeanInteract that referenced this pull request Oct 13, 2025
@augustepoiroux
v0.9.0 (#33)
6f60a30 
Add the following features:
- Fine-grained data extraction for Lean declarations leanprover-community/repl#119
- Incremental elaboration leanprover-community/repl#110
  - also fixes #6
- Parallel elaboration (through `set_option` support)
- `set_option` support leanprover-community/repl#119

A few fixes:
- leanprover-community/repl#108
- leanprover-community/repl#109

Add py.typed
- #32 

Breaking changes:
- Support for Lean v4.7.0 is dropped
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@augustepoiroux