Skip to content
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

feat: frontend & server support for plugins #6893

Merged
merged 1 commit into from
Feb 5, 2025
Merged

feat: frontend & server support for plugins #6893

merged 1 commit into from
Feb 5, 2025

Conversation

tydeu
Copy link
Member

@tydeu tydeu commented Feb 1, 2025 •
edited by Kha
Loading

This PR adds support for plugins to the frontend and server.

Implementation-wise, this adds a plugins argument to runFrontend, processHeader, amd importModules, a plugins field to SetupImportsResult and FileSetupResult. and a pluginsPath field to LeanPaths, and then threads the value through these.

@tydeu tydeu added the changelog-language Language features, tactics, and metaprograms label Feb 1, 2025
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 1, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6893
940963d
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6893
8d4ea1b
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Feb 1, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@tydeu tydeu marked this pull request as ready for review February 3, 2025 06:25
@tydeu tydeu requested review from mhuisi and Kha as code owners February 3, 2025 06:25
@kim-em kim-em changed the title feat: frontend & sever support for plugins feat: frontend & server support for plugins Feb 3, 2025
@Kha
Copy link
Member

Kha commented Feb 3, 2025

Shouldn't --plugin be implemented using this as well?

Do we actually need to put this in importModules? I guess there is the nit that a separate withImporting block would reset runInitializersRef. I don't feel strongly about this point.

@tydeu
Copy link
Member Author

tydeu commented Feb 4, 2025

Shouldn't --plugin be implemented using this as well?

We ended up discussing this privately. For future reference, --plugin does not use the new in-Lean approach because the server watchdog does not support it (whereas the current C approach does support extending the watchdog). This can probably be resolved in future revisions of the watchdog (or when the whole of shell.cpp is ported to Lean), but that is not in scope for this PR.

@tydeu tydeu added this pull request to the merge queue Feb 4, 2025
Merged via the queue into leanprover:master with commit ebba1e0 Feb 5, 2025
26 checks passed
@tydeu tydeu deleted the frontend-plugins branch February 8, 2025 15:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@mhuisi mhuisi Awaiting requested review from mhuisi mhuisi is a code owner

@Kha Kha Awaiting requested review from Kha Kha is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@tydeu @leanprover-community-bot @Kha