Emilio Jesús Gallego Arias

icon indicating a website link https://www.irif.fr/~gallego/ icon indicating an email [email protected]

icon company Inria icon location Paris icon location “La perfection est atteinte, non pas lorsqu'il n'y a plus rien à ajouter, mais lorsqu'il n'y a plus rien à retirer.”

Results 1525 comments of Emilio Jesús Gallego Arias

[ci] Resurrect CI job for OCaml trunk.

@coqbot bench now

[ci] Resurrect CI job for OCaml trunk.

Now bench 4.14-nnp vs 5.0

[ci] Resurrect CI job for OCaml trunk.

Next bench will be once https://github.com/ocaml/ocaml/pull/11827 lands into OCaml master, I wish there was an easier way to try OCaml PRs from opam. Note also the problems with incorrect `Gc`...

[ci] Resurrect CI job for OCaml trunk.

@coqbot bench now

[ci] Resurrect CI job for OCaml trunk.

@coqbot bench now

[ci] Resurrect CI job for OCaml trunk.

@coqbot bench now

[ci] Resurrect CI job for OCaml trunk.

@coqbot bench now

[ci] Resurrect CI job for OCaml trunk.

@coqbot bench now

[ci] Resurrect CI job for OCaml trunk.

Gonna test with 4.09 to see how much of the speedup is due to 4.x GC features from 4.10 onwards @coqbot bench now

Adding "Body", synonymous of "Proof", for interactively-defined definitions

IMHO I'd instead remove the `VernacExactProof` construction at all.