[Install Coq] Error during Coq installation through OPAM

[DE-Kim]

Hello,

I use the VM with ubuntu 16.04 64 bit. I just followed the instruction on the course page (the section OPAM, Coq), but I failed the installation with the error below (with opam install coqide.8.5.2 command);

### stderr ###
# [...]
# File "toplevel/coqloop.ml", line 67, characters 4-28:
# Warning 3: deprecated: Util.String.set
# Use Bytes.set instead.
# File "toplevel/coqloop.ml", line 119, characters 26-41:
# Warning 3: deprecated: Util.String.set
# Use Bytes.set instead.
# Error: Could not compile the library to native code.
# make[1]: *** [theories/Logic/Hurkens.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make: *** [submake] Error 2

That error message was from OPAM, but I think that if you have an error during make coq, it can be also the case in point. (It is because I had the same problem when I tried to install Coq through a binary file.)

Now, I know why. It was the problem of the limitation of the memory. If there is someone who has the same error with me, increase the amount of the memory more than 4GB.

Do not suffer from this problem... Thank you.

[jeehoonkang]

I.. think it is one of the most strange behaviors of a compiler. Lack of memory space should not emit vastly irrelevant error messages without saying "out of memory"... Thank you for finding and sharing this!

• How did you figure it out?
• I think I want to bug-report this behavior to OCaml development team, if you didn't. May I ask if you could give me a detailed log (command input, output ~20 lines, ...)?

[DE-Kim]

One of my senior members adviced me. The change between was only the size of memory. About the details for bug-report, yes I will give you them, but please wait for a couple of days.