Lake now treats platformIndependent as trace-compatible (
fde478c)
Modules that don't depend on dynamic libraries can now toggle platformIndependent between true and unset without forcing a rebuild. The change also updates the precompile/link test coverage to verify the new behavior and related trace output.
Fast import parser fixes overlapping block-comment terminators (
ce02720)
finishCommentBlock now restores the parser position when a - doesn't actually start a terminator, so overlapping candidates like --/ are rechecked correctly. This fixes a subtle import-header parsing bug that could skip valid terminator starts.
lia stops generating instances from hypotheses (
247ad57)
Lean's @[lia] setup now disables local theorem instantiation in this path, preventing lia from creating instances from quantified hypotheses. That closes off a performance trap that could otherwise blow up when problematic hypotheses are in scope.
