Catalin Hritcu

The `PROFILING` file in the top folder contains the commands I was using for profiling in the past: https://github.com/QuickChick/QuickChick/blob/master/PROFILING (the `QuickChick8baf2f` part would need to be generalized, if you wanted...

We could also try to use the newly released "OCaml Memory Profiler": http://memprof.typerex.org/ On Thu, Feb 12, 2015 at 9:39 AM, Çagdas Bozman [email protected] wrote: > Hi, > > On...

Here are the remaining admits in the code, all related to termination: - [FIXED] In `Arbitrary.v` (we don't prove `shrinkZ` terminating, although it seems easy, the measure is already there):...

The `shrinkZ` function is non-terminating in Coq, where `Z.div (-1) 2 = -1` But terminating in OCaml where for ints ``` # (-1)/2;; - : int = 0 ``` I'm...

Ah, it's not so bad actually, it seems that `Z.div` is extracted as is, instead of mapped to OCaml's (/). So `shrinkZ` should be non-terminating in OCaml too. There is...

Here are some new ones I've added to `Tests.v`: - [FIXED] ``` (* TODO: CH: The final theorem I was expecting about removeP is this. CH: Does it follow from...

This is commented out code ``` [hritcu@detained src]$ grep unsafeRandomSeed *.v Extraction.v:(*Extract Constant Test.unsafeRandomSeed => "(unsafePerformIO (SR.randomIO :: GHC.Base.IO GHC.Base.Int))". *) Test.v:(* Axiom unsafeRandomSeed : Z. * ``` Can I...

[DONE (removed)] What's up with this Axiom in `SemChecker.v`? ``` Axiom semSizeCorrect : forall A (g : G A) (x : A) size, semSize g size x exists seed, run...

We could easily get rid of the `show_` and `def` axioms by giving them trivial definitions that are then ignored by extraction. The only reason the `def`s are axioms is...

Not really an axiom, but an extraction trick: ``` Definition trace (A : Type) (s : string) (a : A) : A := a. Extract Constant trace => "(fun x...