coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: e AT x80.org (Emilio Jesús Gallego Arias)
- To: Théo Zimmermann <theo.zimmi AT gmail.com>
- Cc: coq-club AT inria.fr, Kenneth Roe <kendroe AT hotmail.com>
- Subject: Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2
- Date: Mon, 11 Sep 2017 16:16:40 +0200
- 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:3TY58R+7Pe0Cbf9uRHKM819IXTAuvvDOBiVQ1KB90+gcTK2v8tzYMVDF4r011RmSAtWdtqoMotGVmp6jcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47WLmffqXyq7DMUBg63dU8sfry0ScbuiJGL12G1s6/SZgBFnj+0Z7U6eAm2oAKXpMgThIpKJaM4yx+PqXxNLbd432RtcF+7j0akoMCq89Yj3iFRv/Mmv+xNSjfhN4sxSbhVAzNuGno07daq5kqLdheG+nZJCjZeqRFPGQWQqUiiBpo=
- Organization: X80 Heavy Industries
Hi Théo,
Théo Zimmermann
<theo.zimmi AT gmail.com>
writes:
> When building a plugin, don't target an old, unsupported version of
> Coq.
Indeed, this is a good point; I assumed that Kenneth had written his
plugin some time ago when Coq 8.5pl2 was the current version.
In this case, it does make sense to make it work first with 8.5, then to
move to 8.6, then finally to 8.7.
Even if not an official policy, in practice the recommended upgrade path
for old Coq developments/plugins is the linear one.
However, if you are starting afresh, you'd absolutely rather target 8.7.
E.
- [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Théo Zimmermann, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Beta Ziliani, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Beta Ziliani, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Théo Zimmermann, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
Archive powered by MHonArc 2.6.18.