Now I'm need far more than 1.5 hours to compile Metacoq.
Why don't post the post-compilation version?
Do you want the .vo
files? They only work for a specific Coq version. Nix enables doing that, but (EDITING)
but I would not know if Metacoq is available via Nix and Cachix.
And learning to use Nix can be hard, even if rewarding. I can still use Nix only a little bit these days.
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...
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)?
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.
How many physical and virtual cores do you have? Do you use -j
?
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
If you use something like make -j 6
then everything should go a lot lot faster
Agreed — that will use 6 parallel tasks instead of 1.
To get the same speedup on opam install ...
, you can use opam install -j6 ...
.
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 6
then everything should go a lot lot faster
I don't mind test again. But:
image.png
What is the OCaml version you're using?
Yannick Forster said:
What is the OCaml version you're using?
4.07.1
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 [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
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
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 compilationPaolo 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
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
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.
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.
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.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)
I don't know either way and I'm not among the MetaCoq authors, but "you don't want to admit" seems unnecessarily aggressive.
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.
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
@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.
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".
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%
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.
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
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.
Someone could test this on their machine with ulimit
.
Last updated: Nov 29 2023 at 18:01 UTC