coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: David Naumann <dnaumann AT stevens.edu>
To: Michael Soegtrop <MSoegtrop AT yahoo.de>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] problem installing flocq using opam
Date: Sat, 8 Aug 2020 19:34:04 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=stevens.edu; dmarc=pass action=none header.from=stevens.edu; dkim=pass header.d=stevens.edu; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=klUbQZb/qA3Y9/qK76+KXJ1NZI0zEaGGRfMeXBoBgBo=; b=RxoVFcmLZN8xc3sQ09gPv0nSFf5qT0fTW8hrQ8UezUTfFeciCOnLCaynOGXN60yglFk6cESd/xU1sSCpKRCMftDOVGARYxDlRkvkxFmEa/xejl8OXEXbsEjiVzEm+6ypgXU4dxZt7i/Vf882YbghrN/ZktH0QRUH8aUa9yCdHoKT7OHVThB+19V69mb89IgLd6BmUI+IlG6mbwu/GWSE4WBZ6bmq3MAi+NQ9gdH63iONr5f8FfbwnxcAnDBxZZ2i2mZ3RY8tUmtNQ0PO5TKC7SlLhA+YaWNo16Hpsj9m0BuK+ZYjqj2pRhl7IwUrctPum0GaUi7mvGIa3zMmDctKSA==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=LG3WX3NCwwe9MX2JkGks956+HAIiRjye/vsjNtSS4eB5ho4EyAaEP4AWLHXsIo0cONeVv39oJg0QSV3r+Wp+TeZ7dZAjzwIunQ1qXDRh/vIWiZ/vfDE1pNx+egz96a5zL2yRd/ey2cpCC7p6+E5x7Z7BemolZJLHPzB5eO84CUMgKacAgwXqVDYjdUCanv1zTlZqVrAfwM9n2n3ASVk0j1dVnra2jxLnPscNF5RpIXpLHna83qGG7MtbVxmmzYfnhLAVSb8nl+nUFG6HmLqV6810hWUN+RV8umykOW1pSAdLivX0CbuzrtAmHjPhxO7+0GWdfcnkPHt0F4sy+IAapA==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dnaumann AT stevens.edu; spf=Pass smtp.mailfrom=dnaumann AT stevens.edu; spf=Pass smtp.helo=postmaster AT NAM11-DM6-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:bus86xBexO6KNmchoAYzUyQJP3N1i/DPJgcQr6AfoPdwSP37r8iwAkXT6L1XgUPTWs2DsrQY0rSQ4/yrADVcqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5zIRmsrgjcucYajZZ/Jqs+1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOiUn+2/LlMN/kKNboAqgpxNhxY7UfJqVP+d6cq/EYN8WWXZNUsNXWidcAI2zcpEPAvIBM+hGsof9u1UAoxiwBQauCuzvyyNHiHD50qAhz+QuCgTG0BA8E98UsnnZqsj+OqcIUeCyyanF1TvNYOlI2Tf89YfDbwgvruuRXbJ1a8XRz08vHB7Cg1qNr4zqJS6V1uEXvGid6eptTvmvi3I5pAFvvDevwNwshpPXiY0I11DJ7CN0y5s6KtOkUkB0e8KkEIdOuCGAMYt7Wt8uTmNntSs6xLMLpZC1cDYExZk6yBDRZOCKfoiG7B/jSeqfITl1iXBqdb6jmxu/70atxOP9W8e6zltHsiVLn93Ku3sQ2RLT7c2HReF8/kenwTuP0B3T6v1AIUAzkqrbKIQtzaI3lpoWqUjDES72mFn2jK+LbUoo4PSn6+PiYrjgu5SSNJd0hxnxP6gygMCzHPg0PwoUU2SF5+ix2qfv8E76TblSk/E6jrXVvIrZKMgBuKK1HhFZ3pw95xqhETuqyMoUkHgbIF9LfR+LkpTlNErPLf39E/uzn1ehnTJ2y/zYILHsB5DAI3bfnLrnYL1z8VRTyBApwtBa/59UCq8OIPb0WkLprNLVEhg3PxGpz+r+Bttz0YITVXuIAqCCLqzeq1iI5v8zI+aXY48VpTD9JOU/6/72l385nkMdcre10psLaXC4GfJmL1+eYXrxntcBFWAKvg09TODwlFKCVjtTa26zX6I6+D47FJqrAIjfSoy3nbCNwCW2EodIamxYBF2AC3TleoacV/cJci2SI8thkjIeVbimTo8szQyhtAngxLp6K+rb4CsYtZT42dhu++3ciw8y+iJyD8SGyW2CUXx7nn4QSz8swK9/uVB9ykuE0aVgn/NYEsVT6+pVXQc+KJ7T1Pd3C8vyWwLEZteGUkyqQtSgATErT9I+2cUCY0hnG4bqsheW+iuhA7YYk/SwA5E77rjbxzClAv16xnnazq45p0gvQsxIc2Gr0Oo3vQPUHsvCl1iTv6esb6UVmiDXvi/Xxm2X+UpcTQRYUKPfXHlZaFGA/vrj4UaXY7awCLhvFAJczMeELOMeZtvgkFBPQvHLI8jTfW+3gCG9CQveleDEV5bjZ2hIhHaVM0MDiQ1GuC/ebVFjVBfkmHrXCXlVLXyqY07o9rUh+lWSaxZtii2vMQhm3bfz/QMJj/uBTf9VxqgDpCoqtzRzGhC6ws7SDN2D4QFmefcFOI9v0BJ8zWvc8jdFENm4Nak73QwFbwlpskX1kRh7F9cYyJl4nDYR1AN3bJmg/hZEfjKc04r3P+SMeHLu8Q6ibbWQ113Dgo+b

Thanks for the info. But I'm using opam 2.0.7. I get opam updates via
macports.

On 8/8/20, 5:06 AM, "Michael Soegtrop" <MSoegtrop AT yahoo.de> wrote:

Hello David,

I discussed this with Guillaume. He said that remake (which is used by
Flocq) has indeed some kind of job server (but more fancy) and that opam
sandboxing was to restrictive for this. This has been fixed in opam
2.0.2 by:

https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Focaml%2Fopam%2Fpull%2F3663&data=02%7C01%7Cdnaumann%40stevens.edu%7C415a783b6c6049a2849908d83b7a4e00%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C637324743774843050&sdata=iF3zCqYqUGglk1OEYIU4AQEzK8QKYqB7yic9CQj6iS0%3D&reserved=0
Can you please check your opam version if you are indeed using 2.0.1
(which is not that unlikely - 2.0.2 was released December 2018 and opam
has afaik no self update mechanism)?

I will add an opam version check to the coq-platform script to avoid
such issues.

Best regards,

Michael

[Coq-Club] problem installing flocq using opam, David Naumann, 08/07/2020
- Re: [Coq-Club] problem installing flocq using opam, Laurent Thery, 08/07/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