coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Adding ML tactic plugins

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Kenneth Roe <kendroe AT hotmail.com>
Cc: Coq-Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Adding ML tactic plugins
Date: Mon, 02 Oct 2017 09:58:07 +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:I+LqzhSNdlnXUMd/e7zMOxu9/tpsv+yvbD5Q0YIujvd0So/mwa67bRON2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnY6Uy/yPgttJ+nzBpWaz4Huj7jzqNXvZFBriTy7bK9yZC+xoE2FtcQQjZFlJ44xzQfMq3pMPe9RwDU7C0iUmkPxztfgpNhk6SsY+98k9spBVu3Ycr+qVvR3BTAiPm8yrOTxtBDYDFjcrkAAW3kbx0IbSzPO6wv3C9Ko6nP3
Organization: X80 Heavy Industries

Dear Ken,

Kenneth Roe
<kendroe AT hotmail.com>
writes:

> I've done a bit of further investigation on the issue. I now have two
> source trees. There is one in which the tactics seem to be registering
> and one in which they are not. I am unable to figure out what is
> different between the source trees. Is there someone I can send the
> two source trees to for further investigation?

It seems to me that creating a reproducible bug report in bugzilla is be
the proper next step. Howewer,

> By the way, I am using Coq 8.5pl2.

the first obvious step is to update your plugin to use 8.7 beta, just to
be sure you are not suffering from some already-fixed bug.

Also, you may find that coqdev[1] may be a better place for questions
about plugin development.

E.

Re: [Coq-Club] Adding ML tactic plugins, Kenneth Roe, 10/02/2017
- Re: [Coq-Club] Adding ML tactic plugins, Emilio Jesús Gallego Arias, 10/02/2017