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 17:27:42 +0100
Authentication-results: mail3-smtp-sop.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:X6MuMh/VXYY6w/9uRHKM819IXTAuvvDOBiVQ1KB52+gcTK2v8tzYMVDF4r011RmVBdyds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+54Dfbx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaMD45/m/Zhc5zgq1Vrx2uuwdyw5LIbIyPKPZyYrnQcNEcSGFcXshRTStBAoakYoQRFOcAMuVVo5Xnq1sJtxu+ChSnCOfgxD9Nh3/22aw60+M8Gg/CwgMgBMgWsG/Jp9v0LqgSVeS1w7fHzTXEcvhbxS396InSfRA6pP2BW697f8nJyUQ3Cg/IjVadpZb7Mz+L1+kBqXWX4uh9We61lmIqpR99riCsy8otkIXEh4AYxkrA+Clj3Yo4K9u1Q1Nhb9G+CptfrSSaOpN2Qsw8R2Fovz43y7IFtJKnZiQKz44nxxHHZ/yGdYiH/A7jWf6MLTp7h39pYqyziwiz/ES61+HxVNS43ExXoidLjNXArnUN2AbS6siDRPt95ECh2TOX2g/N8exFLkM5mbbBJ54m2L4wmYIfsV7fES/uhEX2kKiWe1049eiv8uTre6npppuBN4BvkQz+KaQvmsmnAesiKAQOXm6b+f691LL550H5Tq9K3bUKlfzSt4mfLsAGrIa4BRVU28At8UWRFTCjhdkwjSlfalVfd1rHoo3oP1DJaNL1FmWky3ullDNmyPeOF6fgC46MfSuLq6voYbsosx0U8wE0190Kv58=
Organization: X80 Heavy Industries

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

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

> So, is there a set of Makefile targets for building Coq, which gives
> me just coqbinaries, tools, and the ltac plugin?

Well, if you wanna be so fine grained I think you may want to use directly:

$ make plugins/ltac/ltac_plugin.cmxs

etc...

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