The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

I got the code to compile.  And the commands that I registered with "VERNAC COMMAND EXTEND" seem to work.  However, the "arewrite" tactic that I registered with "TACTIC EXTEND" is not recognized.  I get the error:

Error: The reference arewrite was not found in the current environment.

I seem to remember having a similar issue with Coq 8.5pl2.  What do I need to change?

                 - Ken

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Maxime Dénès <mail AT maximedenes.fr>
Sent: Saturday, November 4, 2017 9:00 AM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7

 

Try adding `open Ltac_plugin` at the top of your file.

Maxime.

On 11/04/2017 04:52 PM, Kenneth Roe wrote:
> It looks like I'm getting closer.  My file compiles.  However, I get the
> following error:
>
> File "./src/Theory.v", line 74, characters 0-28:
>
> *Error:*
>
> while loading /Users/kendroe/FDS/engine/plugin/src/thepack.cmxs:
>
> error loading shared library:
> dlopen(/Users/kendroe/FDS/engine/plugin/src/thepack.cmxs, 138): Symbol
> not found: _camlTacenv
>
>   Referenced from: /Users/kendroe/FDS/engine/plugin/src/thepack.cmxs
>
>   Expected in: flat namespace
>
>  in /Users/kendroe/FDS/engine/plugin/src/thepack.cmxs
>
>
>
> I discovered the cause of this undefined symbol is this macro:
>
> TACTIC EXTEND AR2
>
> | ["arewrite"] -> [Stuff.arewrite]
>
> END
>
>
> When I comment it out, the resulting module loads.  What do I need to
> include or change?
>
>                  - Ken
>
> ------------------------------------------------------------------------
> *From:* Matej Košík <mail AT matej-kosik.net>
> *Sent:* Saturday, November 4, 2017 6:30 AM
> *To:* coq-club AT inria.fr; kendroe AT hotmail.com
> *Subject:* Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7
>  
> Hi,
>
> On 11/04/17 14:10, Kenneth Roe wrote:
>> Didn't work.
>>
>> Does someone have a sample project that uses "VERNAC COMMAND EXTEND" (and also "TACTIC EXTEND" or what ever it became) for Coq 8.7?
>
> The attached demo exercises some of those mechanisms.
> (Compiles with the "v8.7" branch of Coq).
>
> Let me know what you think.
>
> ---
>
> Matej