The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

On Mon, Sep 11, 2017 at 12:25 PM, Kenneth Roe <kendroe AT hotmail.com> wrote:

I'll rename the "env" module.  Any other modules that I should rename?

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

By the way, I saw a POPL talk on MetaCoq.  However, I cannot find any tutorials.  Is there something I can read that gives a brief overview of MetaCoq?

 

We're currently under heavy development of MetaCoq. It might even be renamed... It currently builds with 8.6, and it depends on Unicoq which is already ported to 8.6. Let's continue talking in a private channel so I can give you more precise pointers according to your needs.

Best,

Beta

 

            - Ken

---

From: Emilio Jesús Gallego Arias <e AT x80.org>
Sent: Monday, September 11, 2017 7:16 AM
To: Théo Zimmermann
Cc: coq-club AT inria.fr; Kenneth Roe
Subject: Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2

 

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.