Emilio Jesús Gallego Arias

Test-suite is passing again :) Only a very small bit remaining for 5.0 support then.

@coqbot run full ci

> @coqbot run full ci Of course this does nothing, we need to update the docker file.

First CI for edge=5.0.0 is almost done, it doesn't look too bad: - one true incompatibility with QC (due to mutable strings) - compcert's version check strikes back - memory...

Thanks for the hints @ppedrot , would be nice to streamline this a bit more. @coqbot bench now

Huhu this looks like it is going to be interesting; first suspect is current GC settings I guess.

@coqbot bench now

No GC tweaking closes the gap a bit, but things are notably slower w.r.t. Coq's defaults. Next, I will bench 4.14-nnp vs 5.0

Some feedback from MC team: - best-fit is not available in 5.0 - 4.14 may set best-fit by default, thus we need to tweak the testing to be sure both...

Next bench is 4.14 with regular GC vs 5.0 with regular GC, which needs to be set explicitly.