Stream: Coq devs & plugin devs

Topic: stressing the native compiler on the bench

Jason Gross (Sep 09 2023 at 00:28):

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

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?

Gaëtan Gilbert (Sep 09 2023 at 10:58):

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

Gaëtan Gilbert (Sep 09 2023 at 12:36):

done

Jason Gross (Sep 09 2023 at 14:00):

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

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: Dec 05 2023 at 12:01 UTC