mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 10:24:07 +00:00
9e0aa14b6f
This PR adds the `fixedToolchain` Lake package configuration option. Setting this to `true` informs Lake that the package is only expected to function on a single toolchain (like Mathlib). This causes Lake's toolchain update procedure to prioritize its toolchain and avoids the need to separate input-to-output mappings for the package by toolchain version in the Lake cache.