search

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
158 stars 48 forks source link

feat: fetch mathlib build cache for focused file command #509

Closed mhuisi closed 2 months ago

mhuisi commented 2 months ago

This PR adds a new 'Project: Fetch Mathlib Build Cache For Focused File' command for use in Mathlib itself.

Closes #416.