spacepaste

Paste details

reply | raw

  1.  
  2. The following actions will be performed:
  3. - install coq 8.7.1+1 [required by coq-bignums]
  4. - install coq-bignums 8.7.0
  5. ===== 2 to install =====
  6. Do you want to continue ? [Y/n]
  7. =-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
  8. [coq] Archive in cache
  9. [coq-bignums] Archive in cache
  11. =-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
  12. [coq: ./configure no] Command started
  13. [coq: make] Command started
  14. [ERROR] The compilation of coq failed at "make -j4".
  15. [coq: rm] Command started
  16. [coq: rm] Command started
  18. #=== ERROR while installing coq.8.7.1+1 =======================================#
  19. # opam-version 1.2.2
  20. # os linux
  21. # command make -j4
  22. # path /home/auke/.opam/system/build/coq.8.7.1+1
  23. # compiler system (4.06.0)
  24. # exit-code 2
  25. # env-file /home/auke/.opam/system/build/coq.8.7.1+1/coq-30635-6cc03f.env
  26. # stdout-file /home/auke/.opam/system/build/coq.8.7.1+1/coq-30635-6cc03f.out
  27. # stderr-file /home/auke/.opam/system/build/coq.8.7.1+1/coq-30635-6cc03f.err
  28. ### stdout ###
  29. # [...]
  30. # OCAMLC toplevel/coqtop.mli
  31. # OCAMLC kernel/byterun/coq_fix_code.c
  32. # OCAMLC kernel/byterun/coq_memory.c
  33. # OCAMLC kernel/byterun/coq_values.c
  34. # OCAMLC kernel/byterun/coq_interp.c
  35. # OCAMLC plugins/ltac/tauto.mli
  36. # OCAMLC plugins/fourier/fourier.ml
  37. # OCAMLC plugins/micromega/sos_types.mli
  38. # OCAMLC plugins/micromega/micromega.mli
  39. # make[1]: Leaving directory '/home/auke/.opam/system/build/coq.8.7.1+1'
  40. ### stderr ###
  41. # Redundant [TYPED AS] clause in [ARGUMENT EXTEND ssrindex].
  42. # File "plugins/micromega/sos_types.mli", line 15, characters 11-18:
  43. # Error: Unbound module Num
  44. # make[1]: *** [Makefile.build:605: plugins/micromega/sos_types.cmi] Error 2
  45. # make[1]: *** Waiting for unfinished jobs....
  46. # make: *** [Makefile:159: submake] Error 2
  50. =-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
  51. The following actions were aborted
  52. - install coq-bignums 8.7.0
  53. The following actions failed
  54. - install coq 8.7.1+1
  55. No changes have been performed
  56.  
Powered by spacepaste. Paste removal.