coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Trouble building 8.8.0

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Trouble building 8.8.0
Date: Tue, 17 Apr 2018 16:06:19 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f174.google.com
Ironport-phdr: 9a23:ZF3WGx2RyE+TlZ3XsmDT+DRfVm0co7zxezQtwd8Zse0RLPad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLnhykHODw5/m/ZicJ+kbxVrw66qhNl34LZepuYOOZicq7fe94RWGpPXtxWVyxEGo6ycYsPCPAGPelArIb9pl4OrR6gCgm2AePg0DlIhnnr1qA9z+QhER/J3As6E9MPsXTUqdD1NKYJXOC6yanH1zTDb/dM1Tjh74jIdwksrPeRVrx+dsrRzFMgFwLDjliIpozlPi+V1uQQs2eA9eZvSeWvi2s/pw5tpTiv3NkjipXTiY0J1lDE9Dl2wJ0vKd29TE52Z8OvHphItyyCKYd6XscvT3trtSs60LEKp4O3cSoQxJg6xRPSZPqKeJWS7B35TuaeOzJ4iWpleL2hgxay9lCtyujmWcm11FZGtzdFncPQunwU2Rzf98qKR/Rn8keu3jaP0A/T6uVaLkwuiaXbLJshzqYxlpoVr0vDAjf7lFvqgKKSbEkp+eil5/75brn7pJKQLZJ4hwPxP6g2n8ywG+U4MgwAX2iB/uS80aXu/VH5QLpUif06iKjYsJHfJcQep660GABV0oM55Ba+CzeqysgXnX4CLF5dYhKIk5DpO03SIPD/Ffqwn1OskC5yy//aOr3hH47CI2PYkLbheLZ981RTxBAyzdBZ/ZJUC6sOLOj9Wk/r55TkCUoyNBXxyOL6Av180JkfUCSBGPy3KqTX5GOIZ+UYEeiJYYIPvT/7LbBx+/7jijkrmFoYfIGm2JIWbDazGfEwcBbRWmblntpUSTRChQE5VuG/0ATTAw4WXG67WucH3h9+DYunCYnZQYX02e6O2S66GttdYWUUUwnQQ0etTJ2NXrI3UAzXOtVoy2VWWr2oSotn3har5lejluhXa9HM8yhdjqrNkdh44+qJy0M3/D1wStmUiySDFj4o2GwPQDAy0eZ0pkkvklo=

You need camlp5 to be properly registered with ocamlfind, cf.
https://github.com/coq/coq/issues/6782

That the error doesn't come earlier (at configure time) should probably be considered as a bug though.

Le mar. 17 avr. 2018 à 16:42, Perry E. Metzger <perry AT piermont.com> a écrit :

Howdy! I'm updating the MacPorts Coq port to 8.8.0, but I got the
following odd error message during the build...

...
OCAMLOPT plugins/ltac/coretactics.ml
ocamlfind: Package `camlp5.gramlib' not found
....

after which the build dies. If someone could tell me what's likely to
be wrong, it would be appreciated, then I can update the
MacPorts package.

Perry
--
Perry E. Metzger perry AT piermont.com

[Coq-Club] Trouble building 8.8.0, Perry E. Metzger, 04/17/2018
- Re: [Coq-Club] Trouble building 8.8.0, Théo Zimmermann, 04/17/2018
  - Re: [Coq-Club] Trouble building 8.8.0, Perry E. Metzger, 04/17/2018
    - Re: [Coq-Club] Trouble building 8.8.0, Théo Zimmermann, 04/17/2018