Skip to content

Instantly share code, notes, and snippets.

@llelf

llelf/coq+flambda.org Secret

Last active October 25, 2019 21:41
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save llelf/bbd589aff60f7fdf2a597acc209f170b to your computer and use it in GitHub Desktop.
Save llelf/bbd589aff60f7fdf2a597acc209f170b to your computer and use it in GitHub Desktop.
Download ZIP
Raw
coq+flambda.org

Coq vs flambda

stdpp

stdpp: master, e35c9837

coq:

The Coq Proof Assistant, version 8.11+alpha (October 2019)
compiled on Oct 25 2019 23:29:42 with OCaml 4.09.0

stdpp compile time (make), best-of-𝑛:

4.09

Ocaml: ocaml-base-compiler.4.09.0

Coq: ./configure -prefix /usr/local/packages/coq.409

real	1m48,929s
user	1m37,802s
sys	0m10,614s

4.09 +flambda

Ocaml: ocaml-variants.4.09.0+flambda

Coq: ./configure -flambda-opts "-O3 -unbox-closures" -prefix /usr/local/packages/coq.409+FL

real	2m21,702s
user	2m9,269s
sys	0m11,360s

4.09 +flambda −native-compiler

Ocaml: ocaml-variants.4.09.0+flambda

Coq: ./configure -native-compiler no -flambda-opts "-O3 -unbox-closures" -prefix /usr/local/packages/coq.409+FL+NN

real	1m23,248s
user	1m13,071s
sys	0m9,785s
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment