coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Makefile targets

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Makefile targets
Date: Fri, 15 Dec 2017 19:57:08 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:/emaJByMFMPyaEbXCy+O+j09IxM/srCxBDY+r6Qd1eIUIJqq85mqBkHD//Il1AaPAd2Craocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HObwlSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKjk58G/ZhMNyj6xUrh2uqABkzo7IfI2YLuZycr/HcN4YQ2dKQ8ZfVzZGAoO5d4YAEfEMPOlbooXhvVcOqgG+BQaxD+/rxTFIg3723ak70+QmDArI2BIvH8kUqHTPsd77Nb0dUeSxzKbWwjXDaO5d1Cvn6IjJaB8huvSAULRtesTS0UkiDx7Jg1aTpID/IT+ZyOUAv3KG4+diSO6jkXMrpg9vrjS3xcohi5PFi4MXx1ze8Sh12pg5KNy+RUVme9CrCoFQuDufN4ZuQsMtXWVouCEix7wJupO3YDIGyJM9xx7Qc/CHco6I7Qz/VOuJPDt1h3FodKihixqs8EWs0PDwW8up3FpQsyZInMfAumgI1xPJ68iHTvV9/l2m2TaKzw3c9PpJIE83mKbHMZIhxaQwlpULvUTZAiD2gFn2jLORdkg85ueo7P3nbqz6qZ+YKo97kRrzMr8um8y6GeQ3KBICX2md+eSm1b3s51f1QLtQjq5+rq6Mu5fDYM8fu6SRAglP049l5QzsIS2h1YEVtWlXdBRCYh3Pz6XsOlXPJ7jaAOwtmByDmTNvyv/BdpT7A5zWbyuQ2Iz9dKpwvhYPgDE4yspSsspZ
Organization: X80 Heavy Industries

"N. Raghavendra"
<nyraghu27132 AT gmail.com>
writes:

> I did "make coqbinaries plugins/ltac/ltac_plugin.cmxs tools", but when
> I tried to compile my files after that, I got an error "cannot guess a
> path for Coq libraries; please use -coqlib option". I think I will
> stick with "make coqbinaries states tools".

Yup, if you go so low-level you need to tell Coq where to look for
things I'm afraid.

E.

[Coq-Club] Makefile targets, N. Raghavendra, 12/15/2017
- Re: [Coq-Club] Makefile targets, Gaëtan Gilbert, 12/15/2017
  - Re: [Coq-Club] Makefile targets, N. Raghavendra, 12/15/2017
- Re: [Coq-Club] Makefile targets, Emilio Jesús Gallego Arias, 12/15/2017
  - Re: [Coq-Club] Makefile targets, N. Raghavendra, 12/15/2017
    - Re: [Coq-Club] Makefile targets, Gaëtan Gilbert, 12/15/2017
      - Re: [Coq-Club] Makefile targets, N. Raghavendra, 12/15/2017
    - Re: [Coq-Club] Makefile targets, Emilio Jesús Gallego Arias, 12/15/2017