The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

Actually, I figured out this error.  It turns out the files in the .mllib file need to be ordered by dependencies.

         - Ken

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Kenneth Roe <kendroe AT hotmail.com>
Sent: Sunday, September 10, 2017 7:34 PM
To: Emilio Jesús Gallego Arias
Cc: Coq-Club
Subject: Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2

 

Thanks.  I'm getting a bit further.  I created an AdvancedRewritePlugin.mllib with the following contents:

Builtin

Cache

Rcontext

Crewrite

Derive

Disc

Env

Exp

ExpIntern

Getfile

Inner

Intern

Kbrewrite

Lex

Match

Mylist

Parser

PrettyPrint

Rule_app

Rsubst

Rtrace

Rtype

Rtrie

Advanced_rewrite

I added it to my _CoqProject.  I still get the following error:

"coqc"  -q  -R "theories" AdvancedRewrite -I "src"   theories/advancedRewrite.v

File "./theories/advancedRewrite.v", line 1, characters 0-42:

Error: while loading src/AdvancedRewritePlugin.cmxs:

no implementation available for Rtype

make[1]: *** [theories/advancedRewrite.vo] Error 1

make: *** [plugin] Error 2

This error appears when I compile the file "theories/AdvancedRewrite.v" which contains one file:

Declare ML Module "AdvancedRewritePlugin".

How do I fix this error?

               - Ken

---

From: Emilio Jesús Gallego Arias <e AT x80.org>
Sent: Sunday, September 10, 2017 4:50 PM
To: Kenneth Roe
Cc: Coq-Club
Subject: Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2

 

e AT x80.org (Emilio Jesús Gallego Arias) writes:

> Assuming you are using Coq 8.7 [which you should be], I suggest you add
> a file to _CoqProject:
>
> src/advanced_rewrite_plugin.mlpack

Oh, I missed the Coq version in the Subject. Then, you may want to use a
mllib file:

> src/advanced_rewrite_plugin.mllib

and list the modules your plugin will need.

E.