Stream: Coq devs & plugin devs

Topic: stressing the native compiler on the bench


view this post on Zulip Jason Gross (Sep 09 2023 at 00:28):

I've prepared a PR for a development that stresses the native-compiler

view this post on Zulip Jason Gross (Sep 09 2023 at 00:32):

Is there a way to run the bench on that PR with native on vs native off, for the package coq-neural-net-interp-computed only?

view this post on Zulip Gaëtan Gilbert (Sep 09 2023 at 10:58):

you put depends: coq-native in the opam package (why?) so no

view this post on Zulip Gaëtan Gilbert (Sep 09 2023 at 12:36):

done

view this post on Zulip Jason Gross (Sep 09 2023 at 14:00):

Thank you! It looks like native gives an impressive 2x speedup over the vm

view this post on Zulip Gaëtan Gilbert (Sep 09 2023 at 16:23):

https://coq.gitlabpages.inria.fr/-/coq/-/jobs/3409666/artifacts/_bench/html/coq-neural-net-interp-computed/theories/MaxOfTwoNumbers/Computed/AllLogits.v.html

expected: about 45 minutes in vm, about 19 minutes in native

but the bench got 457s (~7.5min) on VM and 164s (~2.7min) on native


Last updated: Jul 24 2024 at 13:02 UTC