I finally have a proof where native_compute outperforms vm_compute, by (estimated) 4x. It takes almost 10 minutes in the native compiler execution. (Can't really be added to Coq's CI due to https://github.com/coq/coq/issues/17833, but if https://github.com/coq/coq/issues/17833 is fixed I can probably add it to the Coq performance tests bench or something)

Last updated: Jun 13 2024 at 03:02 UTC