Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari
Last active April 17, 2018 07:14
Show Gist options
  • Save mukeshtiwari/f9c33e1f564f6c04022abec0ffc594c3 to your computer and use it in GitHub Desktop.
Save mukeshtiwari/f9c33e1f564f6c04022abec0ffc594c3 to your computer and use it in GitHub Desktop.
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