coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Théo Zimmermann <theo.zimmi AT gmail.com>
- To: "Perry E. Metzger" <perry AT piermont.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Trouble building 8.8.0
- Date: Tue, 17 Apr 2018 17:41:57 +0000
- Authentication-results: mail3-smtp-sop.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-vk0-f52.google.com
- Ironport-phdr: 9a23:nZ2gtRB6Sc5raSBjn/2JUyQJP3N1i/DPJgcQr6AfoPdwSPT4pMbcNUDSrc9gkEXOFd2Cra4c0KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUijexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Qiqp4bt1RxD0iScHLz85/3/Risxsl6JQvRatqwViz4LIfI2ZMfxzdb7fc9wHX2pMRsleVyJDDY28YYUBDPcPM/hEoITmvVQCsQGzCBOwCO/zyDJFgGL9060g0+QmFAHLxBIuH9IUt3TTtNr6N6YSUeWwzKbW1zXDaulZ2TH76IPVdR0hvfGMUqx3ccbLyEgvFgbFjlCRqYH+MDOV0/4Cs2mf7+Z6Se2vjGsnphh3rzOyyMksjYzJiZgUylDC7Sh5z4c1JcG4SE5metGoCodftyafN4duXswiRHtotzgmyrIcpZG7YCkKx4g8xxLFbvyHd46F6Q/gWuaJOTp0mm5pdbalixux8UWs0PPwWtS63VpQridJjN/BvW0X2RPJ8MiIUP5981+h2TmR0wDT7flJIUUumqraL54t26AwlpkPvUjaEC/7mFv6gLWZdkUj/eio5ODnbav8qpCAMI90jxnyMqUomsOhHeQ1KhYCU3Sf9Oim17Du/Vf1TKtXgvA4iKXUsI7WKdwepqGjAg9V1ogj6wy4DzejyNkYgXkHI0xCeB6djonpOlTOIPX5DfqkjFSslS1kx/HCPrH7HprNKX3DnK/7fblh805c1BYzzddH6p1IDbEBOev/VVP1tNzFFRA0KBe0wubiCNVlzIwSQ2OPAqmDMKPTq1CE/OwvI/PfLLMS7XzFJuI/9rbDyzcclEMPcqSzl9NDcH2iBOVOO0SUe3/rhMtHGmAP6FkQVuvv3WGC0DlkVXe3Wq8m4zg9DsryEYfOQca/gbmE3Q+0G5RXYiZNDVXaQiSgTJmNR/pZMHHaGcRmiDFREOH5E9ZwhyHrjxfzzv9cFsSR/yQZsZz5090svr/ckBgz8Xp/CMHPijjRHVExpXsBQnoN5I46uVZ0kw7R3q1xgvgeHttWtasQD1UKcKXExuk/MOjcHwLMetDTFQSjS9SiRC8yFpc/noVIbEF6FNGvyBvE2njyDg==
My understanding of ocamlfind doesn't go very far but I would say that the META file only serves to register the package (there is no ocamlfind command to execute) but ocamlfind must be able to find this file (for instance in a sub-directory of the directories listed in $OCAMLPATH). You can check the installation is correct by running:
$ ocamlfind query camlp5.gramlib
Théo$ ocamlfind query camlp5.gramlib
Le mar. 17 avr. 2018 à 18:42, Perry E. Metzger <perry AT piermont.com> a écrit :
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
- 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
Archive powered by MHonArc 2.6.18.