fix: run `Lean.enableInitializersExecution`

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover

Apache License 2.0

253 stars 105 forks source link

Closed eric-wieser closed 1 week ago

eric-wieser commented 1 week ago

Without this command, parsers exposed through

suddenly stop existing when the linters run, and so a crash happens when processing the syntax.

It's likely that this has other unintended consequences...

leanprover-community-bot commented 1 week ago

Mathlib CI status (docs):

✅ Mathlib branch batteries-pr-testing-1047 has successfully built against this PR. (2024-11-15 01:00:36) View Log