Last active
April 17, 2018 07:14
-
-
Save mukeshtiwari/f9c33e1f564f6c04022abec0ffc594c3 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
u5935541@newport:~$ which ocaml | |
/home/users/u5935541/.opam/4.06.0/bin/ocaml | |
u5935541@newport:~$ opam install coq | |
The following actions will be performed: | |
∗ install coq 8.7.1+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.1+2 =======================================# | |
# opam-version 1.2.2 | |
# os linux | |
# command make -j4 | |
# path /home/users/u5935541/.opam/4.06.0/build/coq.8.7.1+2 | |
# compiler 4.06.0 | |
# exit-code 2 | |
# env-file /home/users/u5935541/.opam/4.06.0/build/coq.8.7.1+2/coq-15384-0a5907.env | |
# stdout-file /home/users/u5935541/.opam/4.06.0/build/coq.8.7.1+2/coq-15384-0a5907.out | |
# stderr-file /home/users/u5935541/.opam/4.06.0/build/coq.8.7.1+2/coq-15384-0a5907.err | |
### stdout ### | |
# [...] | |
# COQC theories/FSets/FSetList.v | |
# COQC theories/FSets/FSetAVL.v | |
# COQC theories/FSets/FMaps.v | |
# COQC theories/Reals/R_sqr.v | |
# COQC theories/Reals/SplitAbsolu.v | |
# COQC theories/Reals/ArithProp.v | |
# COQC plugins/micromega/Lra.v | |
# COQC theories/Reals/Rminmax.v | |
# COQC plugins/micromega/Lia.v | |
# make[1]: Leaving directory `/home/users/u5935541/.opam/4.06.0/build/coq.8.7.1+2' | |
### stderr ### | |
# [...] | |
# File "./plugins/micromega/Lra.v", line 21, characters 0-37: | |
# Error: System error: "/home/groups/software/bin/.: Permission denied" | |
# | |
# make[1]: *** [plugins/micromega/Lra.vo] Error 1 | |
# 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 | |
# make: *** [submake] Error 2 | |
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= | |
The following actions failed | |
∗ install coq 8.7.1+2 | |
No changes have been performed | |
I have no permission to install anything outside of my home directorr (/home/users/u5935541), so why Coq is trying to install | |
itself in /home/groups/software/bin/ ? | |
Error: System error: "/home/groups/software/bin/.: Permission denied" | |
u5935541@newport:~$ cat /home/users/u5935541/.opam/4.06.0/build/coq.8.7.1+2/coq-15384-0a5907.err | |
Redundant [TYPED AS] clause in [ARGUMENT EXTEND ssrindex]. | |
File "plugins/ltac/tacentries.ml", line 219, characters 8-9: | |
Warning 56: this match case is unreachable. | |
Consider replacing it with a refutation case '<pat> -> .' | |
File "plugins/ltac/tacentries.ml", line 219, characters 8-9: | |
Warning 56: this match case is unreachable. | |
Consider replacing it with a refutation case '<pat> -> .' | |
findlib: [WARNING] Interface profile.cmi occurs in several directories: /home/users/u5935541/.opam/4.06.0/lib/ocaml/compiler-libs, lib | |
findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /home/users/u5935541/.opam/4.06.0/lib/ocaml/compiler-libs, /home/users/u5935541/.opam/4.06.0/lib/ocaml | |
File "./plugins/micromega/Lra.v", line 21, characters 0-37: | |
Error: System error: "/home/groups/software/bin/.: Permission denied" | |
make[1]: *** [plugins/micromega/Lra.vo] Error 1 | |
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 | |
make: *** [submake] Error 2 | |
u5935541@newport:~$ cat /home/users/u5935541/.opam/4.06.0/build/coq.8.7.1+2/coq-15384-0a5907.env | |
PATH=/home/users/u5935541/.opam/4.06.0/bin:/home/users/u5935541/Mukesh/racket/bin:/home/users/u5935541/bin:/home/users/u5935541/Mukesh/Excercism/bin:/home/users/u5935541/Mukesh/satsolvers/cvc4:/home/users/u5935541/Mukesh/clojure:/home/users/u5935541/Mukesh/satsolvers/yices-2.5.2/bin:/home/users/u5935541/Mukesh/satsolvers/mathsat-5.4.1-linux-x86_64/bin:/home/users/u5935541/Mukesh/satsolvers/boolector-2.4.1-with-lingeling-bbc/boolector/bin:/home/users/u5935541/Mukesh/HOL/bin:/home/users/u5935541/Mukesh/polyml/bin:/home/groups/software/bin:/home/users/u5935541/.local/bin:/home/users/u5935541/Mukesh/satsolvers/z3satsolver/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games | |
OCAML_TOPLEVEL_PATH=/home/users/u5935541/.opam/4.06.0/lib/toplevel | |
PERL5LIB=/home/users/u5935541/.opam/4.06.0/lib/perl5 | |
MANPATH=:/home/users/u5935541/.opam/4.06.0/man | |
OPAMSWITCH=4.06.0 | |
CAML_LD_LIBRARY_PATH=/home/users/u5935541/.opam/4.06.0/lib/stublibs | |
XDG_VTNR=11 | |
XDG_SESSION_ID=c24 | |
CLUTTER_IM_MODULE=xim | |
SELINUX_INIT=YES | |
XDG_GREETER_DATA_DIR=/var/lib/lightdm-data/u5935541 | |
SESSION=gnome-fallback | |
GPG_AGENT_INFO=/run/user/593554/keyring-e36oTu/gpg:0:1 | |
TERM=xterm | |
SHELL=/bin/bash | |
XDG_MENU_PREFIX=gnome-flashback- | |
VTE_VERSION=3409 | |
WINDOWID=69206026 | |
OLDPWD=/home/users/u5935541/.opam | |
UPSTART_SESSION=unix:abstract=/com/ubuntu/upstart-session/593554/10481 | |
GNOME_KEYRING_CONTROL=/run/user/593554/keyring-e36oTu | |
GTK_MODULES=overlay-scrollbar:unity-gtk-module | |
USER=u5935541 | |
LS_COLORS=rs=0:di=01;34:ln=01;36:mh=00:pi=40;33:so=01;35:do=01;35:bd=40;33;01:cd=40;33;01:or=40;31;01:su=37;41:sg=30;43:ca=30;41:tw=30;42:ow=34;42:st=37;44:ex=01;32:*.tar=01;31:*.tgz=01;31:*.arj=01;31:*.taz=01;31:*.lzh=01;31:*.lzma=01;31:*.tlz=01;31:*.txz=01;31:*.zip=01;31:*.z=01;31:*.Z=01;31:*.dz=01;31:*.gz=01;31:*.lz=01;31:*.xz=01;31:*.bz2=01;31:*.bz=01;31:*.tbz=01;31:*.tbz2=01;31:*.tz=01;31:*.deb=01;31:*.rpm=01;31:*.jar=01;31:*.war=01;31:*.ear=01;31:*.sar=01;31:*.rar=01;31:*.ace=01;31:*.zoo=01;31:*.cpio=01;31:*.7z=01;31:*.rz=01;31:*.jpg=01;35:*.jpeg=01;35:*.gif=01;35:*.bmp=01;35:*.pbm=01;35:*.pgm=01;35:*.ppm=01;35:*.tga=01;35:*.xbm=01;35:*.xpm=01;35:*.tif=01;35:*.tiff=01;35:*.png=01;35:*.svg=01;35:*.svgz=01;35:*.mng=01;35:*.pcx=01;35:*.mov=01;35:*.mpg=01;35:*.mpeg=01;35:*.m2v=01;35:*.mkv=01;35:*.webm=01;35:*.ogm=01;35:*.mp4=01;35:*.m4v=01;35:*.mp4v=01;35:*.vob=01;35:*.qt=01;35:*.nuv=01;35:*.wmv=01;35:*.asf=01;35:*.rm=01;35:*.rmvb=01;35:*.flc=01;35:*.avi=01;35:*.fli=01;35:*.flv=01;35:*.gl=01;35:*.dl=01;35:*.xcf=01;35:*.xwd=01;35:*.yuv=01;35:*.cgm=01;35:*.emf=01;35:*.axv=01;35:*.anx=01;35:*.ogv=01;35:*.ogx=01;35:*.aac=00;36:*.au=00;36:*.flac=00;36:*.mid=00;36:*.midi=00;36:*.mka=00;36:*.mp3=00;36:*.mpc=00;36:*.ogg=00;36:*.ra=00;36:*.wav=00;36:*.axa=00;36:*.oga=00;36:*.spx=00;36:*.xspf=00;36: | |
XDG_SESSION_PATH=/org/freedesktop/DisplayManager/Session11 | |
XDG_SEAT_PATH=/org/freedesktop/DisplayManager/Seat0 | |
SSH_AUTH_SOCK=/run/user/593554/keyring-e36oTu/ssh | |
DEFAULTS_PATH=/usr/share/gconf/gnome-fallback.default.path | |
SESSION_MANAGER=local/newport:@/tmp/.ICE-unix/10674,unix/newport:/tmp/.ICE-unix/10674 | |
XDG_CONFIG_DIRS=/etc/xdg/xdg-gnome-fallback:/usr/share/upstart/xdg:/etc/xdg | |
DESKTOP_SESSION=gnome-fallback | |
QT_IM_MODULE=ibus | |
QT_QPA_PLATFORMTHEME=appmenu-qt5 | |
JOB=dbus | |
PWD=/home/users/u5935541 | |
XMODIFIERS=@im=ibus | |
GNOME_KEYRING_PID=10477 | |
LANG=en_AU.UTF-8 | |
GDM_LANG=en_AU | |
MANDATORY_PATH=/usr/share/gconf/gnome-fallback.mandatory.path | |
UBUNTU_MENUPROXY=0 | |
IM_CONFIG_PHASE=1 | |
GDMSESSION=gnome-fallback | |
SESSIONTYPE=gnome-session | |
XDG_SEAT=seat0 | |
HOME=/home/users/u5935541 | |
SHLVL=1 | |
LANGUAGE=en_AU: | |
GNOME_DESKTOP_SESSION_ID=this-is-deprecated | |
LOGNAME=u5935541 | |
XDG_DATA_DIRS=/usr/share/gnome-fallback:/usr/share/gnome:/usr/local/share/:/usr/share/ | |
QT4_IM_MODULE=ibus | |
DBUS_SESSION_BUS_ADDRESS=unix:abstract=/tmp/dbus-GeF6tf7wco | |
INSTANCE= | |
TEXTDOMAIN=im-config | |
XDG_RUNTIME_DIR=/run/user/593554 | |
DISPLAY=:4.0 | |
XDG_CURRENT_DESKTOP=Unity | |
GTK_IM_MODULE=ibus | |
TEXTDOMAINDIR=/usr/share/locale/ | |
COLORTERM=gnome-terminal | |
XAUTHORITY=/home/users/u5935541/.Xauthority | |
_=/usr/bin/opam | |
OPAM_PACKAGE_VERSION=8.7.1+2 | |
OPAM_PACKAGE_NAME=coq | |
MAKELEVEL= | |
MAKEFLAGS= | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment