Jason Gross (Jul 17 2023 at 04:36): Jason Gross (Jul 17 2023 at 04:36):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: Oct 08 2024 at 14:01 UTC