Ember Edison (Aug 28 2021 at 07:12): 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?
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)
Paolo Giarrusso (Aug 28 2021 at 07:44):but I would not know if Metacoq is available via Nix and Cachix.
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.
Ember Edison (Aug 28 2021 at 11:21):Paolo Giarrusso said:
Do you want the
.vofiles? 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...
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)?
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.
Yannick Forster (Aug 28 2021 at 11:49):How many physical and virtual cores do you have? Do you use -j?
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
Yannick Forster (Aug 28 2021 at 12:27):If you use something like make -j 6 then everything should go a lot lot faster
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 ....
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
Yannick Forster said:
If you use something like
make -j 6then everything should go a lot lot faster
I don't mind test again. But:
image.png
Yannick Forster (Aug 28 2021 at 14:27):What is the OCaml version you're using?
Ember Edison (Aug 28 2021 at 15:08):Yannick Forster said:
What is the OCaml version you're using?
4.07.1
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?
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)
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
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
Paolo Giarrusso (Aug 28 2021 at 17:25):on the system:
are other intensive tasks running?
on the config
does your ocaml have flambda enabled? enabling that would speed up Coq
.native*) — that could slow down compilation Ember Edison (Aug 30 2021 at 03:09):Paolo Giarrusso said:
on the system:
- is the system swapping? Swap would reduce performance. (The amount of RAM would give a guess)
are other intensive tasks running?
on the configdoes your ocaml have flambda enabled? enabling that would speed up Coq
- is native-compile being used? (and producing folders like
.native*) — that could slow down compilation
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
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.
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.
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:
- 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?
.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. 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)
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.
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.
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
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.
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".
Ember Edison (Sep 01 2021 at 11:59):Paolo Giarrusso said:
- 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%
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.
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
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.
Ali Caglayan (Sep 02 2021 at 14:16):Someone could test this on their machine with ulimit.
Last updated: Nov 29 2023 at 18:01 UTC