coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Installation failed for coq-flocq package

From: Guillaume Claret <guillaume AT claret.me>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Installation failed for coq-flocq package
Date: Sun, 19 May 2019 14:52:45 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=guillaume AT claret.me; spf=Neutral smtp.mailfrom=guillaume AT claret.me; spf=None smtp.helo=postmaster AT relay11.mail.gandi.net
Ironport-phdr: 9a23:0q6vFRVtTlZWzYvew7czf8oqIufV8LGtZVwlr6E/grcLSJyIuqrYYxyPt8tkgFKBZ4jH8fUM07OQ7/m5HzVYv93c7jgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrsAndrNQajZdjJ6o+yhbEo2ZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhJi3YDUboGbOvlwcKzTctwVR3ZOUMlKWixdAY6xdZcDA/YPMOtaqYT2ulsArQG5BQmpHO7hyyJIhn7y3a0+yeshDATG0xI9FN8QtHTbts/1O7kOUeuoy6TIwijDb/JS2Tf58ofIbxUhru+XUL1sdcre01MvGB3ZjlmKrIzqISqY2+IQuGaV6OpgUPigi28hqwxprTivx9ssionUho0O0FzL6SJ5wIMzKNalS0B7ecapHIVNuyyYLYd7QN8uT3t1tCs4ybAKo4C3cSYXxJg/2hLSb/KKf5KW7h/jSuqdOyl0iGx7dL6lmhq+7VWsx+vhXceuyllKtDBKktzUu3ANyRPT7s+HR+Nn/ki/3TaAzQDS5vxZLUwukKrUMZ8hwroqmpocq0vDGDL5mETsgK+QaEok5vCk6+XhYrr4up+RL5F4hhz8P6g0mMGzHf40PhUMUmWY4+iwyrPu8VDhTLVPlPI2k63ZsJ7AJcQco660GwBV0psi6xa7CzepyskYnXwZI19eZB2Hi5LmO0vQL/DkF/u/hkqjnC9xx//aJr3hHonNLn/bnbj9erZ98ldQxxY3zdBC/J1ZEaoBIfL2Wk/prtPUFB45Mwquw+bmEtpxzI0eWXjcSpOeZajVqBqD4v8lC+iKfo4c/jjneNY/4Pu7omI4nVsUYKyklbATYWq1ArwyLFiYZX7ln9IMOWwOtxAzUKrvhQvRAnZoe3+uUvdktXkAA4W8ANKbH9z/sPm6xC6+W6ZuSCVeEFnVSCXjc4yeVutKbS/AepY8wAxBbqCoTsoa7T/rtAL+zOA7fPDZ/iQJ7Mul0dF046vcnBc+9HpyAtjPizjcHVExpXsBQnoN5I46pEV8zlmZ1q0h2q5TEdVJ6u8PVwpob5M=

Hi,

There is this issue related to Flocq on macOS: https://github.com/ocaml/opam-repository/issues/12973
It points to the the notes https://github.com/vellvm/vellvm#notes to disable opam sandboxing and prevent your error `Failed to create server: Operation not permitted`. Hope it helps.

Guillaume

Le 19/05/2019 à 10:27, mukesh tiwari a écrit :

Hi everyone,
I am trying to install coq-flocq package, but getting error operation
not permitted. I tried sudo opam install coq-flocq, but it did not
work [1].

keep-learnings-MacBook-Pro:Floatval keep_learning$ coqtop
Welcome to Coq 8.9.0 (March 2019)

keep-learnings-MacBook-Pro:Floatval keep_learning$ ocaml
OCaml version 4.07.0

keep-learnings-MacBook-Pro:Floatval keep_learning$ opam --version
2.0.3

Best,
Mukesh

[1]https://gist.github.com/mukeshtiwari/305836a97118df55f44f0b7bc17c612c

[Coq-Club] Installation failed for coq-flocq package, mukesh tiwari, 05/19/2019
- Re: [Coq-Club] Installation failed for coq-flocq package, Guillaume Claret, 05/19/2019
  - Re: [Coq-Club] Installation failed for coq-flocq package, mukesh tiwari, 05/19/2019
- [Coq-Club] First Call for Student Volunteers at ICFP'19 in Berlin, Germany, Sandra Dylus, 05/19/2019