Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2


Chronological Thread 
  • From: Kenneth Roe <kendroe AT hotmail.com>
  • To: Emilio Jesús Gallego Arias <e AT x80.org>
  • Cc: Coq-Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2
  • Date: Mon, 11 Sep 2017 02:34:32 +0000
  • Accept-language: en-US
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=Pass smtp.mailfrom=kendroe AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM02-CY1-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:2zzoPRfVlcxHBISMK+zpKWJIlGMj4u6mDksu8pMizoh2WeGdxc29YR7h7PlgxGXEQZ/co6odzbGJ4+a9ASQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpW1aJhKqGA90IuXyLazflFas4M+7/5nebAJ/rSC8aKg6eBievVWJ8M4Mjt0xBLw2z07qr31OdvhWjVlvKBrHnBv66t238bZj9DhVsvMlscVHVPOpLOwDUbVEAWF+YCgO78rxuEybQA==
  • Spamdiagnosticmetadata: NSPM
  • Spamdiagnosticoutput: 1:99

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.



Archive powered by MHonArc 2.6.18.

Top of Page