The Coq mailing list

[Steve Zdancewic <stevez AT cis.upenn.edu>]

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.