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

https://github.com/coq/coq/pull/12974

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^350`

to `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: Oct 13 2024 at 01:02 UTC