Stream: Coq devs & plugin devs

Topic: native_compute success story


view this post on Zulip 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: Jun 13 2024 at 03:02 UTC