Stream: Coq devs & plugin devs

Topic: Benching v8.13

view this post on Zulip Enrico Tassi (Nov 27 2020 at 13:18):

I tried to look at the bench script, but I could not figure out how to start a pipeline to compare tag V8.13+alpha and branch v8.13.
How can I do this?

view this post on Zulip Gaëtan Gilbert (Nov 27 2020 at 13:20):

in the script replace 

new_coq_commit=$(git rev-parse HEAD^2)
old_coq_commit=$(git merge-base HEAD^1 $new_coq_commit)

by

new_coq_commit=$(git rev-parse v8.13)
old_coq_commit=$(git rev-parse V8.13+alpha)

view this post on Zulip Enrico Tassi (Nov 27 2020 at 13:26):

thanks

view this post on Zulip Enrico Tassi (Nov 27 2020 at 13:32):

unfortunately I get

fatal: ambiguous argument 'v8.13': unknown revision or path not in the working tree.
Use '--' to separate paths from revisions, like this:
'git <command> [<revision>...] -- [<file>...]'
Uploading artifacts for failed job

view this post on Zulip Enrico Tassi (Nov 27 2020 at 13:32):

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

view this post on Zulip Enrico Tassi (Nov 27 2020 at 13:33):

is it cloning my personal repo?

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 13:38):

you can give it the full commit hash instead

view this post on Zulip Enrico Tassi (Nov 27 2020 at 13:48):

eureka https://gitlab.com/coq/coq/-/jobs/877154092

view this post on Zulip Enrico Tassi (Nov 27 2020 at 14:02):

FTR, the bench script installs a version of ocaml, but dune needs another, so we waste time compiling ocaml twice:

install ocaml-secondary-compiler 4.08.1-1 [required by ocamlfind-secondary]

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 14:54):

yeah, it does the same on my machine

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 14:54):

dune is not very friendly for people not willing to live on a bleeding edge

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 14:55):

note that there are quite a few differences about perf between OCaml versions, so even if dune reinstalls its own variant of the compiler it's the regular one that is used for the bench

view this post on Zulip Emilio Jesús Gallego Arias (Nov 27 2020 at 16:03):

Yes, the regular one is used, the reinstall is a more a limitation of opam. Dune lives a bit on the bleeding edge as it aims to profit from new OCaml features, so for example when multicore lands in OCaml's trunk, Dune will be able to use after 3 OCaml versions.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 27 2020 at 16:04):

Real problem is lack of build caching, which is not easy, tho I heard OPAM may get something

Last updated: Dec 07 2023 at 14:02 UTC