Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Trouble building 8.8.0

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Trouble building 8.8.0


Chronological Thread 
  • 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

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



Archive powered by MHonArc 2.6.18.

Top of Page