Emilio Jesús Gallego Arias
Emilio Jesús Gallego Arias
Marking this 8.20 ; it is non-controversial IMHO, and would be a pity for UI users to have to keep patching Coq in order to get reliable interruptions.
> @coqbot bench Maybe I should rebase and re-run?
> With memprof-limits, the code to be audited for problems like this should first be strictly delineated by the memprof-limits tasks (e.g. one only need to look at the functions...
@gadmm actually could you have a look at the new function here `Util.atomify`? Is that the right way to do that? TIA!
@SkySkimmer indeed bench found some trouble, will rebase and re-run.
IMHO noise / no-effect (we should actually have a different metric that %, as for equations 11 seconds runtime, 2% is not significative) @SkySkimmer how would it best to go...
> @ejgallego you should probably rebase and undraft quickly if you want this in 8.20. Yes, when is the deadline? Running the test suite for this unfortunately not trivial.
Rebased and undrafted, need to do more testing, but code should not be too different in the final version, maybe protecting the full summaries so we guard against plugins.
@gadmm I'm not using any signals in my implementation, indeed if you send `SIGINT` to Flèche behavior is undefined.