coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] problem installing flocq using opam

From: Michael Soegtrop <MSoegtrop AT yahoo.de>
To: coq-club AT inria.fr, mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
Subject: Re: [Coq-Club] problem installing flocq using opam
Date: Sun, 9 Aug 2020 14:03:00 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=MSoegtrop AT yahoo.de; spf=Pass smtp.mailfrom=msoegtrop AT yahoo.de; spf=None smtp.helo=postmaster AT sonic307-56.consmr.mail.ne1.yahoo.com
Ironport-phdr: 9a23:s6k0EB8lUrECaP9uRHKM819IXTAuvvDOBiVQ1KB31OgcTK2v8tzYMVDF4r011RmVBNudu6wP0LSempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgRFiCC+bL5zIxm7owTcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhzodNzMh7W/ZitJ+jKxYrhyvqRNwzIzbb52aOvR5Za7dYdEXSHBdUstLWSFMAIWxZJYPAeobOuZYqpHwqVwPrRSiBQmjHv3gyjtVjXHr2q01zeshER3c3AwnB9IFrXPZotLoOqcVT++1w7XIzS/Eb/NOwjr86JLHchAmofGLR75/bNTexFApGgjYgVqetZbrMCmJ1uQRrWeb9exgWPqthmMlpA98pjmiy9ojhITXho8byl/J+yp3zYs6OdG1SkB2b9CkHZZQqyyUOYt7TM08TmxmpSs0yr8Lt56/cSQXzpks2h3Ra+SffoWJ4x/vTvudLDZ2iX5/Zb6ygwq+/VKux+HhUMS/zUxEoTBfktbWs3AAzxzT5daDSvt65kqhwjGP1wbS6u5YL004iajWJ4chz7MxjJYcrUPDHintmEXzlq+abEAk9fKp6+TjeLnmoIGTO5JuhgD+KKsumsu/AeMiPgcSWGib/Pyw1Lzl/ULnXLVHlvw7n6jDvJzHJMkWqLS1DxJR34o/8RqyASqq3MwdnXYdLVJFfByHj5LuO1HLOP34COy/g1Oynzdk2/DGJLrhAo3WI3nDirjhfbF960lGxAUu099T/4hUBa0ZIPLvRk/xs8TVAQM+Mwyt2uroFNF91p4FVm+UGa+YMKbSsUeS6e41IumMYpUVuDfnJPQ/6f7ulyxxpVhIdq6wmJATdXqQH/J8Ikzfb2CoytIcEmoRvkIiTfPjklzKBTtOZHupX749+TghCcSnDIbfQ6iihbWA2GGwGZgANU5cDVXZNHbjd4yJX783by+dPtVminRQcIOmRoA9zxa2nB7zy71gaObZrH5L/an/3cR4srWA3So58iZ5WpzEgjO9Clpsl2ZNfAcYmaV2oEhz0FCGiPAqkvVYEtsV6/4bC15nZ66Z9PRzDpXJYiyEftqNTw33EM6hBzA6FYpuhoJQJU16Hc6nlFbG1iuuRbkYzvqaDZwz9eTX2H2jf58hmUaD77EoihwdeuUKLXev3/Yt5gHTAImPn0jLz6s=

Hello Murkesh,

indeed interesting - I start to wonder if David is missing some
per-requisite I have installed and he hasn't. On the other hand I tried
my coq-platform script with an empty MacPorts (just opam) as well. As
far as I can tell I have pretty much the same setup as David has (opam
2.0.7 installed via MacPorts).

Afaik homebrew tends to be more relaxed in terms of access rights - as
far as I remember the first thing it does is make the /usr/local folder
writable to the current user - IMHO a bad idea in terms of security.

But I would think that the opam sandbox is much more restricted, so the
access right differences between MacPorts and homebrew shouldn't matter.
Anyway I can't imagine remake is creating files in a folder like
/usr/local, homebrew makes writable.

Best regards,

Michael

Re: [Coq-Club] problem installing flocq using opam, (continued)
- Re: [Coq-Club] problem installing flocq using opam, Laurent Thery, 08/07/2020
  - Re: [Coq-Club] problem installing flocq using opam, David Naumann, 08/11/2020
- Message not available
  - Re: [Coq-Club] problem installing flocq using opam, Michael Soegtrop, 08/07/2020
    - Re: [Coq-Club] problem installing flocq using opam, David Naumann, 08/07/2020
      - Re: [Coq-Club] problem installing flocq using opam, Michael Soegtrop, 08/07/2020
        
        Re: [Coq-Club] problem installing flocq using opam, Michael Soegtrop, 08/07/2020
        
        Re: [Coq-Club] problem installing flocq using opam, Michael Soegtrop, 08/08/2020
        
        Re: [Coq-Club] problem installing flocq using opam, David Naumann, 08/08/2020
        Re: [Coq-Club] problem installing flocq using opam, mukesh tiwari, 08/09/2020
        Re: [Coq-Club] problem installing flocq using opam, Michael Soegtrop, 08/09/2020
        Re: [Coq-Club] problem installing flocq using opam, Michael Soegtrop, 08/09/2020
        Re: [Coq-Club] problem installing flocq using opam, Guillaume Melquiond, 08/09/2020
        Re: [Coq-Club] problem installing flocq using opam, Michael Soegtrop, 08/09/2020