coq-community / coq-plugin-template Goto Github PK

Say, QuickChick tests its plugin with a bunch of examples: https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/Makefile#L66-L78 , which includes building entire directories like https://github.com/QuickChick/QuickChick/tree/master/tutorials .

How should we write the Dune rules?

I tried the template and noticed that the integer returned by the C function get_n is 1092 but the integer that is getting printed by the CallC Vernacular command is 546.
For me it seams that at some point there happens a bitshift to the right because for the following other integers I get the following other prints:
return 1093 prints 546
return 1094 prints 547
return 0 prints 0
return -1 prints 2147483647
return -2 prints 2147483647
return -3 prints 2147483646
because I can't find any reason for this in the code I thought I write an Issue for this.

How would a _CoqProject file using this plugin look like?

I couldn't make it work.

Is there a specific reason this is not in coq plugin tutorials? It would have saved me hours, probably will to others.