Skip to content

feat: adjusted "fetch mathlib cache for ..." commands#757

Merged
mhuisi merged 1 commit intoleanprover:masterfrom
mhuisi:push-wvukqyzxyoxy
Apr 9, 2026
Merged

feat: adjusted "fetch mathlib cache for ..." commands#757
mhuisi merged 1 commit intoleanprover:masterfrom
mhuisi:push-wvukqyzxyoxy

Conversation

@mhuisi
Copy link
Copy Markdown
Collaborator

@mhuisi mhuisi commented Apr 8, 2026

This PR splits the 'Fetch Mathlib Build Cache For Current Imports' command into three:

  1. 'Fetch Mathlib Build Cache For Open Files': Displayed in the forall menu and the command prompt. Displays a quick select dialog where all open files are selected by default and allows configuring the set of files to fetch the cache for.
  2. 'Fetch Mathlib Build Cache For All Open Files': Only displayed in the command prompt (can also be bound to a keyboard shortcut). Fetches the cache for all open files without displaying a selection dialog.
  3. 'Fetch Mathlib Build Cache For Current File': Only displayed in the command prompt (can also be bound to a keyboard shortcut). Fetches the cache for the currently displayed file without displaying a selection dialog. Re-uses the command ID of the previous 'Fetch Mathlib Build Cache For Current Imports' command, which had the same functionality.

Also ensures that these commands can be used downstream of Mathlib, which was added in mathlib4#21666.

@mhuisi mhuisi force-pushed the push-wvukqyzxyoxy branch from 36c08d9 to 3fdc6c6 Compare April 8, 2026 14:16
@mhuisi mhuisi force-pushed the push-wvukqyzxyoxy branch from 3fdc6c6 to aa27aa8 Compare April 8, 2026 15:32
@mhuisi mhuisi merged commit 541cd8f into leanprover:master Apr 9, 2026
5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant