Stream: MetaCoq

Topic: How to speed up Metacoq compile time


view this post on Zulip Ember Edison (Aug 28 2021 at 07:12):

Now I'm need far more than 1.5 hours to compile Metacoq.
Why don't post the post-compilation version?

view this post on Zulip Paolo Giarrusso (Aug 28 2021 at 07:43):

Do you want the .vo files? They only work for a specific Coq version. Nix enables doing that, but (EDITING)

view this post on Zulip Paolo Giarrusso (Aug 28 2021 at 07:44):

but I would not know if Metacoq is available via Nix and Cachix.

view this post on Zulip Paolo Giarrusso (Aug 28 2021 at 07:45):

And learning to use Nix can be hard, even if rewarding. I can still use Nix only a little bit these days.

view this post on Zulip Ember Edison (Aug 28 2021 at 11:21):

Paolo Giarrusso said:

Do you want the .vo files? They only work for a specific Coq version. Nix enables doing that, but (EDITING)

not just Coq version, different OCaml version need different too
8.11~8.13 Coq just 3 .vo files, 4.06.1/4.07.1/4.10.0 OCaml need 9 .vo files lol

However, it should be take some solution. 1.5 hours can install GTA5 in SSD or WinXP in HDD...

view this post on Zulip Yannick Forster (Aug 28 2021 at 11:33):

I'm a bit surprised by the 1.5 hours. This is the time for manual compilation from code? Do you use parallel compilation via make -j 3 (or a similar number)?

view this post on Zulip Ember Edison (Aug 28 2021 at 11:47):

Yannick Forster said:

I'm a bit surprised by the 1.5 hours. This is the time for manual compilation from code? Do you use parallel compilation via make -j 3 (or a similar number)?

just manual compilation. Opam compile safechecker/pcuic need a lot of time (>45min) when opam install coq-metacoq, That's why I conducted this test.

view this post on Zulip Yannick Forster (Aug 28 2021 at 11:49):

How many physical and virtual cores do you have? Do you use -j?

view this post on Zulip Ember Edison (Aug 28 2021 at 12:26):

AMD Ryzen 5 3600 6-Core
not use any other option, just

eval $(opam env)
./configure.sh local
make
make translations
make test-suite
make install

view this post on Zulip Yannick Forster (Aug 28 2021 at 12:27):

If you use something like make -j 6 then everything should go a lot lot faster

view this post on Zulip Paolo Giarrusso (Aug 28 2021 at 13:12):

Agreed — that will use 6 parallel tasks instead of 1.
To get the same speedup on opam install ..., you can use opam install -j6 ....

view this post on Zulip Paolo Giarrusso (Aug 28 2021 at 13:13):

To tell opam to build software in parallel by default, you can append to ~/.opam/config this line:

jobs: 6

view this post on Zulip Ember Edison (Aug 28 2021 at 14:13):

Yannick Forster said:

If you use something like make -j 6 then everything should go a lot lot faster

I don't mind test again. But:
image.png

view this post on Zulip Yannick Forster (Aug 28 2021 at 14:27):

What is the OCaml version you're using?

view this post on Zulip Ember Edison (Aug 28 2021 at 15:08):

Yannick Forster said:

What is the OCaml version you're using?

4.07.1

view this post on Zulip Yannick Forster (Aug 28 2021 at 15:09):

Something is strange. This really should not take more than 30 minutes to compile, to the contrary: On a machine like yours it should be quicker than CI. Can you try less parallel tasks, something like 4-6 and report?

view this post on Zulip Ember Edison (Aug 28 2021 at 15:14):

Ember Edison [said]

I don't mind test again. But:
[image.png](/user_uploads/23559/0tUrWp4wYsFx9KofkX3r-mh9/image.png)

opam install coq-metacoq

installed coq-equations.1.2.4+8.13
installed coq-metacoq-template.1.0~beta2+8.13
installed coq-metacoq-translations.1.0~beta2+8.13

6min40s

installed coq-metacoq-pcuic.1.0~beta2+8.13

42min18s

installed coq-metacoq-safechecker.1.0~beta2+8.13

1h22min46s

installed coq-metacoq-erasure.1.0~beta2+8.13
installed coq-metacoq.1.0~beta2+8.13

1h30min43s

view this post on Zulip Ember Edison (Aug 28 2021 at 15:15):

Yannick Forster said:

Something is strange. This really should not take more than 30 minutes to compile, to the contrary: On a machine like yours it should be quicker than CI. Can you try less parallel tasks, something like 4-6 and report?

now is 6

I'm sure if this is the school's old machine, then many people will want to kill me

view this post on Zulip Paolo Giarrusso (Aug 28 2021 at 17:25):

on the system:

  1. is the system swapping? Swap would reduce performance. (The amount of RAM would give a guess)
  2. are other intensive tasks running?
    on the config

  3. does your ocaml have flambda enabled? enabling that would speed up Coq

  4. is native-compile being used? (and producing folders like .native*) — that could slow down compilation

view this post on Zulip Ember Edison (Aug 30 2021 at 03:09):

Paolo Giarrusso said:

on the system:

  1. is the system swapping? Swap would reduce performance. (The amount of RAM would give a guess)
  2. are other intensive tasks running?
    on the config

  3. does your ocaml have flambda enabled? enabling that would speed up Coq

  4. is native-compile being used? (and producing folders like .native*) — that could slow down compilation
  1. I have at least 4GB RAM can use
  2. No
    2.3.I don't understand why this affects COQC. Do I need to recompile Coq without dune?

view this post on Zulip Matthieu Sozeau (Aug 30 2021 at 09:04):

I don't think we ever tried compiling with native enabled, but that could slow down compilation tremendously.
You could try:

# make COQFLAGS="-native-compiler no"

and see if that improves the compilation time

view this post on Zulip Janno (Aug 30 2021 at 09:16):

I've had issues like that on network file systems before. Whatever OCaml and Coq do seems to be the absolute worst case; at least for the configuration I had to work with. You could easily spend hours compiling Coq itself.

view this post on Zulip Janno (Aug 30 2021 at 09:18):

I have also experienced similarly extreme slowdowns in linux containers (lxc or lxd or whatever they changed it to now). That wasn't with OCaml though but with gcc. Developments that would compile in seconds outside of the container would take half an hour inside.

view this post on Zulip Paolo Giarrusso (Aug 30 2021 at 13:36):

I have at least 4GB RAM can use

With so little, I'd check out memory consumption. IME a Coq process takes anywhere from 500MB to few GBs, so -j6 can easily hit limits.

Ember Edison said:

Paolo Giarrusso said:

on the system:

  1. does your ocaml have flambda enabled? enabling that would speed up Coq

2.3.I don't understand why this affects COQC. Do I need to recompile Coq without dune?

  1. I was unclear; building Coqc with the ocaml optimizer active would likely produce a faster Coqc; a bit OT but a good tip.
  2. Coq can compile .v files to native code, but that can be very slow. (The point is that this native code can be run by the native_compute tactic). Hence, Matthieu's advice.

view this post on Zulip Ember Edison (Aug 31 2021 at 15:50):

I have completed all your requirements. There is almost no difference in time. (gap < 5min)
Since you don't want to admit that MetaCoq compile just slow, I propose to add MetaCoq to the OCaml Performance Numbers benchmarks. (https://github.com/coq/coq/wiki/OCaml-Performance-Numbers)

view this post on Zulip Paolo Giarrusso (Aug 31 2021 at 17:01):

I don't know either way and I'm not among the MetaCoq authors, but "you don't want to admit" seems unnecessarily aggressive.

view this post on Zulip Théo Zimmermann (Aug 31 2021 at 17:16):

Hey @Ember Edison, I am a moderator here and I agree with Paolo. Please be kind to the people who are giving away their time to try to help you.

view this post on Zulip Ember Edison (Aug 31 2021 at 18:23):

I may be extreme, I just want to remind you that the "flaws" on the opam file/make file will take >1.5 hours for the user to test once
The responsibility for the problem should be clear

view this post on Zulip Théo Zimmermann (Aug 31 2021 at 18:34):

@Ember Edison Do I need to remind you that free software comes without any warranty? Your wording "the responsibility for the problem" may give the impression that you feel entitled. If you are just giving feedback, that's welcome but again, please try to use language that is considerate and respectful. Note that discussions on this chat are bound by our Code of Conduct.

view this post on Zulip Ember Edison (Sep 01 2021 at 11:57):

Théo Zimmermann said:

Ember Edison Do I need to remind you that free software comes without any warranty? Your wording "the responsibility for the problem" may give the impression that you feel entitled. If you are just giving feedback, that's welcome but again, please try to use language that is considerate and respectful. Note that discussions on this chat are bound by our Code of Conduct.

I am not an English native language user, I can apologize again. Our university in this poor area just this English level.

This is NOT a warranty claim.
If I get a proof of False in MetaCoq, I will “apply for warranty”.

Just talk about this topic, You can announce that like "takes 1.5 hours to compile" or "OCaml 4.10 can't install" is a "feature".

view this post on Zulip Ember Edison (Sep 01 2021 at 11:59):

Paolo Giarrusso said:

  1. I was unclear; building Coqc with the ocaml optimizer active would likely produce a faster Coqc; a bit OT but a good tip.

With current data (OCaml Performance Numbers), COQC very stable, replace compiler performance improvements will not bring more than 15%

view this post on Zulip Théo Zimmermann (Sep 01 2021 at 12:13):

I am not an English native language user, I can apologize again. Our university in this poor area just this English level.

That's fine. I kind of guessed that this was mostly a language barrier issue.

view this post on Zulip Yannick Forster (Sep 01 2021 at 15:03):

Sadly, the problem seems to be specific to your machine, Ember. Many people contributed ideas what the culprit is, but I'm now clueless. On my machine, on the machines of many students I've worked with on MetaCoq and on both the MetaCoq and the Coq CI the installation time is around 30 minutes. That doesn't mean we won't fix the problem, I really would like to understand what's going on. We'll definitely keep an eye out whether the problem occurs also on other machines, but until then my personal suggestion would be that you endure the 1.5 hours once and then use MetaCoq, which hopefully works without huge slowdowns. But, if you're willing to debug more, we can also collectively generate new ideas how you might be able to speed up compilation

view this post on Zulip Michael Soegtrop (Sep 01 2021 at 15:42):

At one point it was mentioned that the machine in question has just 4 GB of RAM. You might want to clarify what Coq Platform recommends in this case - see (https://github.com/coq/platform/blob/2021.02/shell_scripts/ask_parallel_build.sh). I would recommend "-j 2" and it definitely will be much slower than with more memory - both cause of reduced parallelization and cause of reduced file cache size or even swapping. With a factor of 3 slower than a machine with larger RAM you are quite lucky IMHO.

view this post on Zulip Ali Caglayan (Sep 02 2021 at 14:16):

Someone could test this on their machine with ulimit.


Last updated: Aug 11 2022 at 02:03 UTC