Original bug ID: 7826
Reporter: @ppedrot
Status: acknowledged (set by @xavierleroy on 2018-07-19T16:01:07Z)
Resolution: open
Priority: normal
Severity: minor
Version: 4.06.1
Category: middle end (typedtree to clambda)
Monitored by: @nojb
Bug description
The Closure.close_functions function computes the set of free variables of its arguments, which is O(n). Unluckily this function is recursive and it subcalls can do the same, which leads to a runtime quadratic in the number of nested abstraction nodes.
I doubt this is an issue in handwritten code, but the problem sure happens in generated code. I hit it in the native compilation scheme of Coq code from fiat-crypto, and the compiler takes ages for a term that is big but not crazy either (~ 500kloc of sparse code, every line being a constructor most of the time).
I do not have a small reproducible test-case at hand, this would require extracting it from the generated code and making it standalone, which is not easy.
Original bug ID: 7826
Reporter: @ppedrot
Status: acknowledged (set by @xavierleroy on 2018-07-19T16:01:07Z)
Resolution: open
Priority: normal
Severity: minor
Version: 4.06.1
Category: middle end (typedtree to clambda)
Monitored by: @nojb
Bug description
The Closure.close_functions function computes the set of free variables of its arguments, which is O(n). Unluckily this function is recursive and it subcalls can do the same, which leads to a runtime quadratic in the number of nested abstraction nodes.
I doubt this is an issue in handwritten code, but the problem sure happens in generated code. I hit it in the native compilation scheme of Coq code from fiat-crypto, and the compiler takes ages for a term that is big but not crazy either (~ 500kloc of sparse code, every line being a constructor most of the time).
I do not have a small reproducible test-case at hand, this would require extracting it from the generated code and making it standalone, which is not easy.