131b35a...
by
=?utf-8?q?Ga=C3=ABtan_Gilbert?= <email address hidden>
Revert "Mark arrays, products, and plain constants, as potentially needing a delayed evaluation during native_compute (fix #18703)."
This reverts commit b13eb1e93016bf605f2783ac32074faa3ec609ac.
ca44371...
by
=?utf-8?q?Ga=C3=ABtan_Gilbert?= <email address hidden>
Backport PR #18469: Delay the lookup of csdp until the tool is actually needed.
0da7e0b...
by
Guillaume Melquiond <email address hidden>
Delay the lookup of csdp until the tool is actually needed.
(cherry picked from commit 8eb6ef7b9eafbf60a21c6ae80c81f2ac459ad692)
8cf7d4e...
by
=?utf-8?q?Ga=C3=ABtan_Gilbert?= <email address hidden>
Backport PR #18883: Mark arrays, products, and plain constants, as potentially needing a delayed evaluation during native_compute (fix #18703).
b13eb1e...
by
Guillaume Melquiond <email address hidden>
Mark arrays, products, and plain constants, as potentially needing a delayed evaluation during native_compute (fix #18703).
The following statements would otherwise cause a stack overflow if the
module were to be compiled and then loaded, even if the constant was
completely unrelated to the term being normalized.
Definition large := [|fact 100|0|].
Definition large := (0 <= fact 100) -> Prop.
Definition large := large'.
Note that the following statements are still eagerly evaluated, on purpose.
Definition small := [|0|0|].
Definition small := Prop -> Prop.
Note also that the translation of the following code is a bit suboptimal:
Definition large := large'.
(* let large = lazy (Lazy.force large') *)
(cherry picked from commit 6fe5e52896a10d3cfe2214c39ba40168f4810428)
d6577af...
by
=?utf-8?q?Ga=C3=ABtan_Gilbert?= <email address hidden>
Backport PR #18924: Make some VM allocations more robust
355f34d...
by
Guillaume Melquiond <email address hidden>
Make MAKESWITCHBLOCK more robust against large stack frames.
When it encounters an accumulator, MAKESWITCHBLOCK copies the whole stack
frame of the current function, so that the code of the pattern-matching
branches can be replayed later, during strong normalization. There is no
reason why the stack frame could not exceed 256 words, even in a
non-malicious function, so it needs to be taken into account.
(cherry picked from commit 8e43e6fc6207ad60a6056c688bc071c4a35587df)
d7a3dab...
by
Guillaume Melquiond <email address hidden>
Allow large allocations with MAKEBLOCK.
Now that MAKEBLOCK is also used for allocating universe blocks, and since
those can grow larger than 256 words (one known instance of size 888 in
non-malicious user code), it needs to be made more robust.
(cherry picked from commit f8df1f995c9d240a87525b0ab3071679e9bee05a)
d65add6...
by
Guillaume Melquiond <email address hidden>
Factor out comments about Alloc_small, as more instances are about to be added.
(cherry picked from commit 3d454dc9dd3309297695f8e205658070121f8a11)
dc2e6d6...
by
=?utf-8?q?Ga=C3=ABtan_Gilbert?= <email address hidden>
Backport PR #18991: Fix dependent evars line with defined evars
