diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-23 20:55:21 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-23 21:02:18 +0200 |
commit | 1e3d73abd90af8646222bc4d6ea42f7d7ed3ddd1 (patch) | |
tree | 380eec492ad25568d8d3ef7661378253d13fd3da /lib | |
parent | a321074cdd2f9375662c7c9f17be5c045328bd82 (diff) |
Fix bug #5096: [vm_compute] is exponentially slower than [native_compute].
The fix is essentially a revert of f22ad60 that introduced the use of the
pretyper version of whd_all instead of the one from the kernel. The exact
cause of slowness of the pretyper version is still to be investigated, but
it is believed that it is due to a call-by-name strategy, to compare with
call-by-need in the kernel.
Note that there is still something fishy in presence of evars. Technically
vm_compute does not handle them, but if this comes to be the case, it might
be worthwile to use an evar-aware variant of whd_all.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions