The build breaks when I remove the option.
set_option linter.constructorNameAsVariable false
|
set_option linter.constructorNameAsVariable false |
When I remove this option, I see an error
linter Lean.Linter.constructorNameAsVariable failed: maximum recursion depth has been reached
This issue keeps track of investing the performance problem.
The first step is to upgrade the toolchain and see if it still breaks.