coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
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.
> 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.
- [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Théo Zimmermann, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Beta Ziliani, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Beta Ziliani, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Théo Zimmermann, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Kenneth Roe, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
- Re: [Coq-Club] Building an ml plugin for Coq 8.5pl2, Emilio Jesús Gallego Arias, 09/11/2017
Archive powered by MHonArc 2.6.18.