Discussion:
[Coq-Club] Problems installing coq-flocq via opam
Steve Zdancewic
2018-11-06 16:58:18 UTC
Permalink
I am having difficulties installing coq-flocq via opam.  I'm using opam
2.0.0 with ocaml 4.06.0 and coq 8.8.2 on OSX 10.14 (Mojave). The issue
seems to be a permissions problem in the opam sandboxing script, which
gives the error "# Failed to create server: Operation not permitted".  
The compilation of 'remake' generates a warning, but seems to succeed. 
(See detailed output below.)

I've tried disabling opam sandboxing (via 'opam init
--disable-sandboxing'), but so far have had no luck.  opam seems to work
fine for other packages I've installed recently.

Any suggestions about where the problem might be?

Thanks!
--Steve


====================
~ opam install -v coq-flocq
The following actions will be performed:
  ∗ install coq-flocq 3.0.0

<><> Gathering sources
<><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
[coq-flocq.3.0.0] found in cache

<><> Processing actions
<><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
+ /Users/stevez/.opam/opam-init/hooks/sandbox.sh "build" "./configure"
"--libdir" "/Users/stevez/.opam/4.06.0/lib/coq/user-contrib/Flocq"
(CWD=/Users/stevez/.opam/4.06.0/.opam-switch/build/coq-flocq.3.0.0)
- checking for g++... g++
- checking whether the C++ compiler works... yes
- checking for C++ compiler default output file name... a.out
- checking for suffix of executables...
- checking whether we are cross compiling... no
- checking for suffix of object files... o
- checking whether we are using the GNU C++ compiler... yes
- checking whether g++ accepts -g... yes
- checking for coqc... /Users/stevez/.opam/4.06.0/bin/coqc
- checking for coqdep... /Users/stevez/.opam/4.06.0/bin/coqdep
- checking for coqdoc... /Users/stevez/.opam/4.06.0/bin/coqdoc
- configure: building remake...
- remake.cpp:2593:16: warning: 'tempnam' is deprecated: This function is
provided for compatibility reasons only.  Due to security concerns
inherent in the design of tempnam(3), it is highly recommended that you
use mkstemp(3) instead. [-Wdeprecated-declarations]
-         socket_name = tempnam(NULL, "rmk-");
-                       ^
-
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.14.sdk/usr/include/stdio.h:306:1:
note: 'tempnam' has been explicitly marked deprecated here
- __deprecated_msg("This function is provided for compatibility reasons
only.  Due to security concerns inherent in the design of tempnam(3), it
is highly recommended that you use mkstemp(3) instead.")
- ^
-
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.14.sdk/usr/include/sys/cdefs.h:180:48:
note: expanded from macro '__deprecated_msg'
-         #define __deprecated_msg(_msg) __attribute__((deprecated(_msg)))
-                                                       ^
- 1 warning generated.
- configure: creating ./config.status
- config.status: creating Remakefile
- config.status: creating src/Version.v
+ /Users/stevez/.opam/opam-init/hooks/sandbox.sh "build" "./remake"
"-j7" (CWD=/Users/stevez/.opam/4.06.0/.opam-switch/build/coq-flocq.3.0.0)
- Failed to create server: Operation not permitted
[ERROR] The compilation of coq-flocq failed at
"/Users/stevez/.opam/opam-init/hooks/sandbox.sh build ./remake -j7".

#=== ERROR while compiling coq-flocq.3.0.0
====================================#
# context     2.0.0 | macos/x86_64 | base-bigarray.base
base-threads.base base-unix.base ocaml-base-compiler.4.06.0 |
https://coq.inria.fr/opam/released
# path        ~/.opam/4.06.0/.opam-switch/build/coq-flocq.3.0.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build ./remake -j7
# exit-code   1
# env-file    ~/.opam/log/coq-flocq-1700-05296d.env
# output-file ~/.opam/log/coq-flocq-1700-05296d.out
### output ###
# Failed to create server: Operation not permitted



<><> Error report
<><><><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
┌─ The following actions failed
│ λ build coq-flocq 3.0.0
└─
╶─ No changes have been performed
'opam install -v coq-flocq' failed.
Guillaume Melquiond
2018-11-06 17:28:07 UTC
Permalink
Post by Steve Zdancewic
I am having difficulties installing coq-flocq via opam.  I'm using opam
2.0.0 with ocaml 4.06.0 and coq 8.8.2 on OSX 10.14 (Mojave). The issue
seems to be a permissions problem in the opam sandboxing script, which
gives the error "# Failed to create server: Operation not permitted".
The compilation of 'remake' generates a warning, but seems to succeed.
(See detailed output below.)
I've tried disabling opam sandboxing (via 'opam init
--disable-sandboxing'), but so far have had no luck.  opam seems to work
fine for other packages I've installed recently.
Any suggestions about where the problem might be?
My suggestion would also be to disable sandboxing. Note that "opam init"
does nothing if opam is already initialized. So, typing "opam init
--disable-sandboxing" does not disable sandboxing, unfortunately. You
need to manually edit the "config" file to remove the "wrap-*-commands"
lines.

Best regards,

Guillaume
Steve Zdancewic
2018-11-06 17:52:09 UTC
Permalink
Thanks!  Manually removing ~/.opam/config to remove the wrap-*-command
lines did the trick.

Interestingly, I had previously tried to disable the sandbox by doing: 
opam init --reinit --disable-sandboxing.  This caused all of my opam
switch to be re-built, but had no effect (as far as I could tell) on the
sandboxing scripts.

--Steve
Post by Guillaume Melquiond
Post by Steve Zdancewic
I am having difficulties installing coq-flocq via opam.  I'm using
opam 2.0.0 with ocaml 4.06.0 and coq 8.8.2 on OSX 10.14 (Mojave). The
issue seems to be a permissions problem in the opam sandboxing
script, which gives the error "# Failed to create server: Operation
not permitted". The compilation of 'remake' generates a warning, but
seems to succeed. (See detailed output below.)
I've tried disabling opam sandboxing (via 'opam init
--disable-sandboxing'), but so far have had no luck.  opam seems to
work fine for other packages I've installed recently.
Any suggestions about where the problem might be?
My suggestion would also be to disable sandboxing. Note that "opam
init" does nothing if opam is already initialized. So, typing "opam
init --disable-sandboxing" does not disable sandboxing, unfortunately.
You need to manually edit the "config" file to remove the
"wrap-*-commands" lines.
Best regards,
Guillaume
Guillaume Melquiond
2018-11-06 18:09:39 UTC
Permalink
Post by Steve Zdancewic
Thanks!  Manually removing ~/.opam/config to remove the wrap-*-command
lines did the trick.
That is fortunate. Nonetheless, I will investigate what might cause
remake to fail starting under the opam's sandbox on OSX.
Post by Steve Zdancewic
opam init --reinit --disable-sandboxing.  This caused all of my opam
switch to be re-built, but had no effect (as far as I could tell) on the
sandboxing scripts.
Right, this is a known feature of opam:

https://github.com/ocaml/opam/issues/3634

Best regards,

Guillaume
Frédéric Blanqui
2018-11-07 07:18:20 UTC
Permalink
Hello. I got the same problem with CoLoR but not with coq-bignums. See
https://github.com/fblanqui/color/issues/12. Why do we have to disable
sandboxing? Is it a bug in opam?
Post by Guillaume Melquiond
Post by Steve Zdancewic
Thanks!  Manually removing ~/.opam/config to remove the
wrap-*-command lines did the trick.
That is fortunate. Nonetheless, I will investigate what might cause
remake to fail starting under the opam's sandbox on OSX.
Post by Steve Zdancewic
Interestingly, I had previously tried to disable the sandbox by
doing: opam init --reinit --disable-sandboxing.  This caused all of
my opam switch to be re-built, but had no effect (as far as I could
tell) on the sandboxing scripts.
https://github.com/ocaml/opam/issues/3634
Best regards,
Guillaume
Guillaume Melquiond
2018-11-07 08:15:56 UTC
Permalink
Post by Frédéric Blanqui
Hello. I got the same problem with CoLoR but not with coq-bignums. See
https://github.com/fblanqui/color/issues/12. Why do we have to disable
sandboxing? Is it a bug in opam?
For Flocq, the opam issue is https://github.com/ocaml/opam/issues/3659

I don't think Color suffers from the same issue, but the fix might
actually turn out to be the same.

Best regards,

Guillaume
Guillaume Melquiond
2018-11-07 08:31:34 UTC
Permalink
Post by Guillaume Melquiond
Post by Frédéric Blanqui
Hello. I got the same problem with CoLoR but not with coq-bignums. See
https://github.com/fblanqui/color/issues/12. Why do we have to disable
sandboxing? Is it a bug in opam?
For Flocq, the opam issue is https://github.com/ocaml/opam/issues/3659
I don't think Color suffers from the same issue, but the fix might
actually turn out to be the same.
Scrap that. The issue is much simpler and it is actually a bug in the
opam package for Color. Indeed, it installs the library using the
"build" rule. The "build" rule should only be used to build the library.
The library should be installed by the "install" rule.

Best regards,

Guillaume
Frédéric Blanqui
2018-11-07 09:25:21 UTC
Permalink
Oh, right. I updated the git repo but not the opam package!
Post by Guillaume Melquiond
Post by Guillaume Melquiond
Post by Frédéric Blanqui
Hello. I got the same problem with CoLoR but not with coq-bignums.
See https://github.com/fblanqui/color/issues/12. Why do we have to
disable sandboxing? Is it a bug in opam?
For Flocq, the opam issue is https://github.com/ocaml/opam/issues/3659
I don't think Color suffers from the same issue, but the fix might
actually turn out to be the same.
Scrap that. The issue is much simpler and it is actually a bug in the
opam package for Color. Indeed, it installs the library using the
"build" rule. The "build" rule should only be used to build the
library. The library should be installed by the "install" rule.
Best regards,
Guillaume
Loading...