The Coq mailing list

[Zoe Paraskevopoulou <zoe.paraskevopoulou AT gmail.com>]

Hi Talia, Gaëtan, 

Thank you both for your answers. 

> On Jan 31, 2020, at 5:22 AM, Gaëtan Gilbert 
> <gaetan.gilbert AT skyskimmer.net>
>  wrote:
> 
> Did you open Stdarg?

Yes. My (relevant) imports right now are:

open Stdarg
open Pp
open Ltac_plugin

> On Jan 31, 2020, at 2:53 AM, Talia Ringer 
> <tringer AT cs.washington.edu>
>  wrote:
> 
> Maybe a silly question, but does it work if you use { } instead of [ ]? I 
> don't know if you just copied over the code incorrectly. The error messages 
> for .mlg files are always bewildering. Apologies if it's not that. I 
> haven't used VERNAC ARGUMENT EXTEND before.


Ah, that’s an interesting observation. My file is an .ml4 file (which seems 
deprecated for this purpose, but I never knew until now) and the syntax is 
exactly the syntax that I use in the file (in fact the {} syntax gives me a 
syntax error in .ml4). But I’ll try to change it to .mlg and see if that 
works. 

> Whenever you do figure this out, I'd like to add an example to one of the 
> plugin tutorials in the Coq repo. Please let me know if you are willing to 
> share a minimal example for that.

Sure thing! I can submit something to the Coq plugin tutorial, once I get 
something working.

Cheers, 
Zoe



> On Jan 31, 2020, at 5:22 AM, Gaëtan Gilbert 
> <gaetan.gilbert AT skyskimmer.net>
>  wrote:
> 
> Did you open Stdarg?
> 
> Gaëtan Gilbert
> 
> On 30/01/2020 21:18, Zoe Paraskevopoulou wrote:
>> Hi Coq Club,
>> I’ve been trying to write a vernacular command that parses some optional 
>> arguments, but I’m facing some issue and I’d appreciate some help.
>> The result I’m trying to achieve is:
>> CertiCoq Compile [options] <global_identifier>
>> where [options] is zero or more compilation flags like -debug.
>> For this I wrote the following code:
>> type command_args =
>>  | ANF
>>  | TIME
>>  | OPT of int
>>  | DEBUG
>>  | ARGS of int
>> VERNAC ARGUMENT EXTEND cargs
>> | [ "-anf" ] -> [ ANF ]
>> | [ "-time" ] -> [ TIME ]
>> | [ "-o1" ] -> [ OPT(1) ]
>> | [ "-debug" ] -> [ DEBUG ]
>> | [ "-args" int(n) ] -> [ ARGS(n) ]
>> END.
>> However, when I compile I get the following error:
>> File "g_certicoq.ml4", line 1, characters 0-0:
>> Error: This expression has type int -> Pp.t
>>        but an expression was expected of type
>>          'a Extend.entry = 'a Grammar.GMake(CLexer).Entry.e
>> This happens whenever I try to parse a non-terminal symbols (e.g. 
>> string()) in VERNAC ARGUMENT EXTEND, not just with int().
>> If I drop the last case of cargs and parse this option at the VERNAC 
>> COMMAND instead, everything works:
>> VERNAC COMMAND EXTEND CertiCoq_Compile CLASSIFIED AS QUERY
>> | [ "CertiCoq" "Compile" cargs_list(l) “-args” int(x) global(gr) ] -> [ 
>> ... do stuff ...  ]
>> END
>> Any idea about what is going on? I’m suspecting that I’m missing an import 
>> because I’ve seen this type of parsing in VERNAC ARGUMENT EXTEND before. 
>> For example here: 
>> https://github.com/coq/coq/blob/master/plugins/ltac/g_ltac.mlg. I tried to 
>> use the same imports but that didn’t help.
>> I am using Coq 8.9.1 and OCaml 4.07.0.
>> Cheers,
>> Zoe