Rival no profiling

[obround]

This PR:

• Removes all Rival profiling data from the Herbie nightly and timeline
• Extends --enable dump:rival dumps:
  • Format now has an (answer <valid/invalid> <answer>) instruction, and a top-level (precision <binary32/binary64>) instruction
  • Below is an example Rival dump
  • Fixes a dumping race condition when running on multiple threads that would overwrite other threads' .rival files
• Modifies the --num-points syntax to take #train/#test instead of just #train like before (this is
• Introduces make points.tar.xz to dump Rival points for the Rival 3 nightly: samples 256 training points and 1000 test points (--num-points 256/1000)
• Rival 3 mirrors these changes to use the new points (24 MB at the current configuration)

New Rival dump format example:

(precision binary64)
(define (f g h)
  (assert (TRUE))
  (* 2 (cos (+ (/ (* 2 (PI)) 3) (/ (acos (/ (neg g) h)) 3)))))
(eval f #i4.620547116939733e+155 #i6.246387790113829e+187)
(answer valid -1.7320508075688772)
(eval f #i-7.075089557411109e-272 #i-1.623615482099185e+147)
(answer valid -1.7320508075688772)
(eval f #i-2.94884489652898e-244 #i2.274622184692958e-118)
(answer valid -1.7320508075688772)
(eval f #i4.3646937051460406e-241 #i7.879187542989997e-246)
(answer invalid)
...

[pavpanchekha]

So this is interesting. Precision is presumably per-function/per-output? A bit ugly to set this globally, then.

[obround]

Hmm if I understand what you're saying correctly, would a syntax like this be better as opposed to (precision binary64 binary64) at the top:

(define (f v_0 v_1) (assert (TRUE)) (! :precision binary64 v_0) (! :precision binary64 v_1))

There's only one Rival file that compiles more than one output (and hence has more than one precision specified).

[pavpanchekha]

Yeah, uhh, I don't know if I have a preferred syntax here but we're trying to make the benchmarks use rival's normal input language. Which presumably an actual user somewhere might use. So we should try to make it usable!

[pavpanchekha]

Ok, I don't have a real solution here, and I'm not sure how important it is. Better to merge this and fix issues later. In terms of actual usability as a stand-alone programming language, (precision X Y Z) is weird because it introduces lots of state & possibility for error. Like what if you write that and then define a function with 2, or 4, return values? BTW (answer valid) and (answer invalid) is also a bit weird, right, since again what if you list the wrong number of answers or something? But there at least I see the point, the syntax allows us to write out the query before we launch it. Some other alternatives, if any appeal to you: 1) we could only dump cases where all the types match, and keep (precision X); 2) we could do the (! :precision X foo) syntax, though it's kinda ugly; 3) you could do (define (...) X Y Z :precisions foo bar baz). We can always merge this now and now worry about it, but again, you're not going to have this stuff more paged in in the future. You might know more, it can be legitimate to say "let's decide this when we know more. It's a judgement call.