Guillaume Melquiond

@coqbot merge now

> I understand that the {native,vm}_compute machineries have been pessimized a bit in OCaml 5 What makes you say that? Anyway, FourColor is mostly VM, and its running time is...

To be clear, the VM in FourColor allocates like crazy, especially since the executed bytecode does not rely on native integers. After all, the VM does not do anything except...

> It might be possible to annotate VM closures with the relevance of their arguments but IDK how to do it and doing it for native seems even less likely....

The main (and huge) issue is that there is a wide variety of implementation of `fma`. Some of them are blatantly wrong (newlib and uclibc). Some of them seem correct...

While the pull request has been accepted, it seems `opam update` does not yet know about `malfunction >= 0.6` (double-checked locally). I guess we need to wait a whole day...

No, using `rewrite -[Rmult]/scal` (as well as `@scal` variants) does not work any better than `change Rmult with (@scal _ R)`, since the "fold pattern scal does not match redex...

Indeed, this is the likely culprit. ```coq Print Grammar constr. (* | "0" LEFTA [ "[find"; "v1,"; "..,"; term LEVEL "200"; "|"; term LEVEL "200"; "∼"; term LEVEL "200"; "]";...

Note that this is not the same behavior as with `-native-compiler`. If one does ``` ./configure -native-compiler no ... coqc -native-compiler yes ``` then native compilation is still disabled (and...

Do we need yet another option? Would not it be sufficient to teach `coq_makefile` that, if it finds a `_CoqProject` file at the target directory of a `-R` or `-Q`...