coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: e AT x80.org (Emilio Jesús Gallego Arias)
- To: Kenneth Roe <kendroe AT hotmail.com>
- Cc: Théo Zimmermann <theo.zimmi AT gmail.com>, "coq-club\@inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2
- Date: Mon, 11 Sep 2017 17:35:47 +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:Ayfo5RQxD9ui/vZ7HmjXeshgwtpsv+yvbD5Q0YIujvd0So/mwa67bRON2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnY6Uy/yPgttJ+nzBpWaz4Huj7jzqNXvZFBriTy7bK9yZC+xoE2FtcQQjZFlJ44xzQfMq3pMPe9RwDU7C0iUmkPxztfgpNhk6SsY+98k9spBVu3Ycr+qVvR3BTAiPm8yrOTxtBDYDFjcrkAAW3kbx0IbSzPO6wv3C9Ko6nP3
- Organization: X80 Heavy Industries
Kenneth Roe
<kendroe AT hotmail.com>
writes:
> I'll rename the "env" module. Any other modules that I should rename?
I am afraid you will have to manually check that there are no conflicts
[or else move to mlpack in 8.6]
> I'll eventually move over to 8.7. The reason I used 8.5pl2 is 1) it
> is available through OPAM and 2) many of the plugins I've been
> studying to build my interface are still on 8.5pl2 (MetaCoq, PrintAST,
> coq-tutorial-ml-tactics, mirror-shard).
This is unfortunate; I feel however that differences should be
manageable would you like to move to 8.7.
In practice, using anything older than 8.7 implies that your plugin will
receive less support from the Coq side: hundredths of bugs have been
fixed since 8.5, and with developer time being quite limited these days,
bugs that cannot be tested against current version tend to slide to
bottom of TODO lists.
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.