The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi Everyone,

I am recently updated the OCaml compiler to 4.06.0

u5935541@newport:~/Mukesh/Code/EncryptionSchulze/code$ which ocaml
/home/users/u5935541/.opam/4.06.0/bin/ocaml

But when I am trying to install Coq using opam, I am getting this error

u5935541@newport:~/Mukesh/Code/EncryptionSchulze/code$ opam install coq
The following actions will be performed:
  ∗  install coq 8.7.2

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq] Archive in cache

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[ERROR] The compilation of coq failed at "make -j4".
Processing  1/1: [coq: rm]
#=== ERROR while installing coq.8.7.2 =========================================#
# opam-version 1.2.2
# os           linux
# command      make -j4
# path         /home/users/u5935541/.opam/4.06.0/build/coq.8.7.2
# compiler     4.06.0
# exit-code    2
# env-file     /home/users/u5935541/.opam/4.06.0/build/coq.8.7.2/coq-31520-d2c37b.env
# stdout-file  /home/users/u5935541/.opam/4.06.0/build/coq.8.7.2/coq-31520-d2c37b.out
# stderr-file  /home/users/u5935541/.opam/4.06.0/build/coq.8.7.2/coq-31520-d2c37b.err
### stdout ###
# [...]
# COQC      theories/FSets/FSetWeakList.v
# COQC      theories/FSets/FSetEqProperties.v
# COQC      theories/FSets/FSetList.v
# COQC      theories/FSets/FSetAVL.v
# COQC      theories/FSets/FSetToFiniteSet.v
# COQC      theories/Reals/Rfunctions.v
# COQC      plugins/micromega/Lra.v
# COQC      plugins/micromega/Lia.v
# COQC      plugins/micromega/Lqa.v
# make[1]: Leaving directory `/home/users/u5935541/.opam/4.06.0/build/coq.8.7.2'
### stderr ###
# [...]
# make[1]: *** Waiting for unfinished jobs....
# File "./plugins/micromega/Lia.v", line 20, characters 0-37:
# Error: System error: "/home/groups/software/bin/.: Permission denied"
#
# make[1]: *** [plugins/micromega/Lia.vo] Error 1
# File "./plugins/micromega/Lqa.v", line 20, characters 0-37:
# Error: System error: "/home/groups/software/bin/.: Permission denied"
#
# make[1]: *** [plugins/micromega/Lqa.vo] Error 1
# make: *** [submake] Error 2



=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
  ∗  install coq 8.7.2
No changes have been performed

I understand the reason of failure, because it is trying to install in directory, /home/groups/software/bin/,  which is not owned by me(u5935541) and I don't have read, write or execute permission, but  it did not happen in the past whenever I installed Coq using Opam.   Could someone please tell me how can I install Coq using Opam.

I have posted all the details in gist [1].

Best regards,
Mukesh Tiwari

[1] https://gist.github.com/mukeshtiwari/475624a99931ec3c008c6bb0fe1c6f9f