coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Makefile targets

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Makefile targets
Date: Fri, 15 Dec 2017 16:58:27 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay5-d.mail.gandi.net
Ironport-phdr: 9a23:MSXBFRUObjQVCHQ43ubOGvj434LV8LGtZVwlr6E/grcLSJyIuqrYbBGHt8tkgFKBZ4jH8fUM07OQ7/i5HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9vIBmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/KlMJwgqJVrhGvqRNxzIHbYp2aOvVlc6PBft4XX3ZNUtpfWiFDBI63cosBD/AGPeZdt4TzpkEBqgeiBQa2AuPg0j5Ghn7y3aIhzeshCx3G1xEnEtIBqnvbssn1O70UUeyvw6nIzDHDYOhI1jfn9IjFaQshofKMXLJrcsrRyEwvFwbbgVWKs4DlOS2a1vgUvmWd8uFuW+Wvi2s9pAFwpDii3scsipPIho4P0FDL6z55zJw0Jd2+UEJ7e8CrEIdKtyGdK4t5XMwjQ31zuCogzL0Jp4K7cS4Xw5ok3x7Sc+KLf5WK7x75VuudPS10iG9mdb+xnRq+7Eytx+/kWsS1zlpGtDdJnsXSunwXyhDe5cuKRuFg8kqh2DuC0R3Y5PteLkAuj6XbLoYswr4umZoXtkTOBjX2l1vyjKCMdkQp+vGk5Pn9brXjvJCcNot0hhvxMqs0nMywHOU4PhIIX2eF5eSwzLzj/UvnT7VWlvA6jLTVvZLAKckZuqK1GRJZ34Ut5hqlEjur1NYVkWECLF1feRKHi4bpO0vJIPD9Ffq/jE6jnyl3x//cOL3tGJrNLnnHkLj6Y7l98VJcxREozdBc55NUEbIBIPP2Wk/0qtPYFAU1MwqqzOb7ENl9zJ8RWXqTAq+FN6PfqUOH5uU2I+WVeIAVvCv9JOM+6v71jX45nEcdcrOz0ZsWbnC4BPVmLF+DbXrimNdSWVsN6wE5VanhjECIeT9VfXe7GawmtR8hD4fzIo5AWomrt5OA2C22BIEeMm9PB0yFFzHndoGOVu0QQDmRM9RikzkBWKLnTYI9g0L9/DTmwqZqe7KHshYTsojugYB4

coqbinaries tools pluginsopt?

Hard to say without knowing what kind of error you get.

Gaëtan Gilbert

On 15/12/2017 16:52, N. Raghavendra wrote:

I have a Coq development, for which I am using coqtop / coqc with
the -noinit option, and the commands

Declare ML Module "ltac_plugin".
Global Set Default Proof Mode "Classic".

in the source files. Right now, I am building Coq for this project
using "make coqbinaries states tools". This still builds Prelude.vo,
which I don't need because I use the "-noinit" option. So, is there a
set of Makefile targets for building Coq, which gives me just
coqbinaries, tools, and the ltac plugin? (I have tried "make
coqbinaries ltac tools", but my files don't compile with the resulting
build.)

Thanks and best regards,
Raghu.

--
N. Raghavendra
<raghu AT hri.res.in>,
http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

[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