coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Trouble building 8.8.0

From: "Perry E. Metzger" <perry AT piermont.com>
To: Théo Zimmermann <theo.zimmi AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Trouble building 8.8.0
Date: Tue, 17 Apr 2018 12:42:15 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=perry AT piermont.com; spf=Pass smtp.mailfrom=perry AT piermont.com; spf=None smtp.helo=postmaster AT hacklheber.piermont.com
Ironport-phdr: 9a23:8iTjxxJKdT/BzNqKHdmcpTZWNBhigK39O0sv0rFitYgRL/jxwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhikHOTAn7W/Zic5/jKxUrx29qBJy2JLUYJiPOfZiYq/RYdEXSGxcVchRTSxBBYa8YpMBA+QbI+lYtZP9plsTphWxHwWnGeThxSFUhn730q01zf4hHQ/b1wEnB9IBrm7UrM/1NaoJSeC1zbfHzS/Gb/NR3zf99JLEfQwmofGJRL99d9fax0coFwPAlFqQqIrlMiua1uQMr2ib7/dgWvm1h2E7rAFxpz6izdovhInRno8Z11HJ+CRjzIs2KtC0Ukx2bcS5HJZfsSyRKpF4Tdk4Q25yvSY30r0GtoC/fCgN0JknxwTQZOCEc4iM4hLsSv2eLilihH5/YLK/hgi98VKlyu37UMm0zExGoTZCktnJrnwN1hrT5dabSvZl40us2DeC2xrQ5+xLO0w5l7DXJ4Muz7Iok5ocq0XDHiv4mEXsi6+Wc10p+vC25OT9eLXnpoSRN5d1ig7gKKQun8u/AeIkMgQUQ2eb/uG82KX5/ULlWLVKkuE2kq7BvZ/GIsQbv7e1DBNR0oY+8BmyFCym0dQdnXkfNl1JYhOHj47zO1HPOv/0F/m/g07/2AtskszGv7qpMJTIK3XZlb7ne/4p905Rz0whzNVa5rpbD7gAJLT4XUqn5/LCCRpseTS52fz2QPg7nqYTRXCAD7XTePfKvEWS98o3IuSWYYgTpHD2LP1ztK2mtmMwhVJIJfrh5pAQcn3tRq03cXXcWmLlh5I6KUlPuwM/SOLwj1jbDWxLZnuoWqU6+ncwD4f0VN6fFLDou6SI2WKAJrMTfnpPUwzeCXblbYCDXetKYyWXcJc4z240EIO5Qopk7imA8Q/3z709c7jU8yYbsZLu3tVvofXSmAs38jpoSc+a1jPVQg==

On Tue, 17 Apr 2018 16:06:19 +0000 Théo Zimmermann
<theo.zimmi AT gmail.com>
wrote:
> You need camlp5 to be properly registered with ocamlfind, cf.
> https://github.com/coq/coq/issues/6782

My understanding of ocamlfind is a bit weak. What ocamlfind command
exactly needs to be executed in order to register the META file
correctly? (Assume I know the path to the META file.)

Perry

> 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 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