do we have a reasonable set of micro-benchmarks for the native compiler?
I've written a patch to get rid of the naked pointer hack and would like to see how terrible it is
@Guillaume Melquiond uses native compute on real examples, I think this is better than a micro bench
but I have no easy way to bench it, haven't I?
on your machine?
@Pierre-Marie Pédrot patch for the bench should be pretty simple tho, basically add
actually I have no idea anymore what is going on the bench due to the way it was merged wihtout review
should be okish tho if it is using opam to build Coq
I will add the default support for native once we get coqnative merged
As I wrote on https://github.com/coq/coq/pull/13287 I'd really like to it unstuck and merged
@Enrico Tassi what development are you talking about precisely?
before thrashing the bench I'd like to check locally
Actually the bench will only test the performance of the ocaml compiler, not sure there are a lot of calls to native_compute there actually
I think it was the interval one, but I'm not 100 sure. anyway, grep native_compute should tell you
Yes, CoqInterval makes use of
native_compute, if asked to. So, you could
opam pin your Coq build, then build CoqInterval. Then I can give you some lengthy computations.
I pushed my PR there: https://github.com/coq/coq/pull/14048
I'll try to compile interval without having to boot up a fresh OPAM switch though
Here is an example:
From Coq Require Import Reals. From Coquelicot Require Import Coquelicot. From Interval Require Import Tactic. Goal True. (* just in case native_compute is "ondemand" *) integral_intro (RInt (fun x => sin (x + exp x)) 0 8) with (i_delay, i_native_compute) as _. (* it takes about 1 second per 1k fuel, change the fuel amount accordingly *) Time integral_intro (RInt (fun x => sin (x + exp x)) 0 8) with (i_width (-40), i_fuel 10000, i_delay, i_native_compute).
@Pierre-Marie Pédrot https://github.com/mit-plv/fiat-crypto/blob/master/src/UnsaturatedSolinasHeuristics/Tests.v is one of the few cases I've seen where
native_compute is much, much faster than
vm_compute. The current tests are supposed to take about 40s in
native_compute, though by just adjusting the filter on line 145 from
2^401 you can double the length of the test. We have tests set up all the way up to
2^521, but expect these to be very very slow.
If you want to factor this out into a standalone benchmark, I expect the fully inlined file will only be 1000--2000 loc.
Last updated: Dec 06 2023 at 13:01 UTC