Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Makefile targets

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Makefile targets


Chronological Thread 
  • From: "N. Raghavendra" <nyraghu27132 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Makefile targets
  • Date: Sat, 16 Dec 2017 00:07:51 +0530
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=nyraghu27132 AT gmail.com; spf=Pass smtp.mailfrom=nyraghu27132 AT gmail.com; spf=None smtp.helo=postmaster AT mail-pg0-f48.google.com
  • Ironport-phdr: 9a23:V5nw6xeF+YGHE2eBS32LWq6+lGMj4u6mDksu8pMizoh2WeGdxcS8Yx7h7PlgxGXEQZ/co6odzbaO6ua4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahfL9+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38H/ZhNFyg6JVrh2hvRJxzY3bb46JO/RzZb/dfcoASGZdQspcTS5MD4WhZIUPFeoBOuNYopHzq1UWtxe1GBWiC/ngyj9InHD2w7M10+I8HgHcxgMsEc8FvXPSrNT1LqcdS++1zKnVzTndbf5axDnw5JbTfxAupPGDR7Nwcc7LxUYzEAPFi0ydpIr4ND2b0eQNtnKU7+tmVe+3i24nsQBxriK1xsgykYnFnIMVylbc+SVj3ok1Oce4SElnYdG6H5pQqzqaO5FwQsw8X2FlvjsxxL4euZOjfiUHx44rywPBZ/GHaYSF4RzuWPyeLDp7nH5pZqyziwqo/US+1OHxVNO43EtWoidLiNXAq34A2h7V58OaUPVy5F2h1iyK1w3L6uFLP0Q0la3DJp4k2LEwl54TvV3bHi/5hEn6laGWe0on9+Sy5OTnZbLmppCYN4BqkA3xLqMumsmnDeQ5NAgBQXSb9Py+2bDs50H1XatGg/0snqTavp3WP8sWq62hDw9QyIkj6hK/Dzm80NQfmHkKNFRFeRKdj4fzNFHOIO34Aem9jlixnjpn2evLPrLkAprXL3jDlK3tcqp6605Z0AYz18xQ54pICrEdJ/L+QlP+tNvBDhMgLwO0x/vnB85m24MFWWOPB7eZP7nIvV+J4OIvOeiMa5UPtDbzMfh2r8Lp2HQ+gBoWebSj9ZoRcnGxWPp8cH+UeX79vtBUW0FM9jA3Q+zjllCEXSRaLT7mWbMm7z47Fdj5VNyZbo+oib2Fmiy8G8sFSHpBDwXGNzGgTYyLW/4SZSSeOMYr2mgCRKKoRI88j07371XSxL9uL+6S8Sod48GwnONp7vHewElhvQd/CN6QhjmA
At 2017-12-15T16:58:27+01:00, Gaëtan Gilbert wrote:

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

Thanks, and I am sorry, I wrote that with "make coqbinaries ltac tools"
my files don't compile, but I saw just now that they do. I last tried
it a few days ago, and must have messed up something, which led to an
error that I can't recall. When I tried compiling my files just now,
after "make coqbinaries ltac tools", they did compile. However, I see
that this make command also installs Prelude.vo.

I guess there is no point in trying to install only the components that
I need. The command "make coqbinaries states tools" is quick enough.

Best regards,
Raghu.

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

Archive powered by MHonArc 2.6.18.

Top of Page