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: David Naumann <dnaumann AT stevens.edu>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] problem installing flocq using opam
Date: Sat, 8 Aug 2020 11:06:11 +0200
Authentication-results: mail2-smtp-roc.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 sonic317-34.consmr.mail.ne1.yahoo.com
Ironport-phdr: 9a23:NOi1tx8VD2N1Xv9uRHKM819IXTAuvvDOBiVQ1KB21eIcTK2v8tzYMVDF4r011RmVBNudu6kP0rGG+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhJiTanYr5/Ihq6oRjfu8QVnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRQT2gykbKTE27GDXitRxjK1FphKhuwd/yJPQbI2MKfZyYr/RcdYcSGFcXMheSjZBD5uhYYUPEeQBM+VWoYfzqFQBrxSxGQaiCuT0xz9UhHL7x7E23v4vHAzE2gErAtIAsG7TrNXwLKocVuG1w7XIzTrZcfxW3Sr25pXPch8/rvGMQahwcc3JyUIyEA7LiUieqYv7MDOayuQNqW+b7/J7WOOvkWEnqwZxoj+1ysgxlIbEn4QYwU3L+itl2og6P8G4SFJlbt6+Fptdrz+XO5V1T848TW9kpDo2x6EatJO1fyUG1pQqyhreZvGHfYWE/w/vWeifLDplhn9rd6yzihWy/0W81+HxVci53EpMoyFYnNfMsXUN2AbS6siBUvZ98Uah2SqP1wDO8e5IO1w7la3eK5Mn37U+lYITvFzCEyL3gkn6ka6be0s+9uS16Onqba/qq5CcOoJylwrwKL4hmtalDuQ9KgUOX3aU+eC71LD75k35R7NKjvwqnaTXrZzXJ90Xq6C2DgNPzokj7BC/Dyyj0NQCh3UHKUhKeBODj4TzPVHBPu30Ae2/glu2kDdrwPfGMqf9DZXKK3jPiLbhfbBj5E5A0Ac+zNFS64hJBrwALv//QFL9ud/XAxMjPAG5w/7rCNBn2YMfXWKPDLWZMKTXsVKQ4+IvOO6Ma5EauDbhMfgl4ObugGQ5mFAHfamp2pwXZGqlEft4O0mZe2bjgs8dEWcWuQozVPDliFqbUTJKe3myW7886SogBYK9DYbDQ5itj6ab0Ce6GJ1WfGFGBUqWHXfmbYXXE8sLPQ6bPM5t2hoNSL2oTYlpgR2ovRL/wrxhBvHI9zMVs4ml2dRosamb3xo17Hl/C9mX+2CLVWB92G0SDXdi16dm5Ed5112r0K5igvUeG8YFtN1TVQJvEJ/Xz+V3D5jJXQ/OYs2OUB7yZ+6hDD4tVNUp684HY0F6Xdmv2EOQlxG2CqMYwuTYTKc/9bjRij2of54kmiT2kZI5hlxjefNhcGivh6px7Q/WXtabgkyZkKHsealOhXeQplfG9nKHuQRjaCA1UajBWitONFDRq9XyvRqdCuTyT78gNBBE04iHI6pOLNvk1BNXTffkP5LVZGfjwz7sVybN/auFac/RQ0tYxD/UURBWggkT+nHAOQVsXio=

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://github.com/ocaml/opam/pull/3663
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