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, but if is fixed I can probably add it to the Coq performance tests bench or something)

Last updated: Jun 13 2024 at 03:02 UTC