ejgallego/coq-serapi

Adding a mode to sercomp to get rid of all notations

vsiles opened this issue · 14 comments

vsiles commented

Hi !
Do you know how complex it would be to extend sercomp with a mode that strips a vernacular expression of all notations ? The end goal here is to train an algorithm without having to deal/depend on user notations, feeding it only notation free expressions.

To my knowledge there is currently no option to do that (and coqc -beautify is quite broken). I'm not familiar with Coq plugin development, but if you think that's not a huge task, I might be able to help implementing it.

Just asking :)

Best,
V.

ejgallego commented

Hi @vsiles ,

that's a tricky question; indeed it may be doable but there are several approaches:

  • you could consider this a duplicate of #155 , so we could just have a mode where terms are internalized; this will also resolve implicits, tweaks matches, and performs a form of name resolution; main downside is that you change the base type from constr_expr to glob_expr; this requires special handling and is in a sense a bit redundant
  • you could write you own function to desugar the notations, not sure how easy this would be, but doable
  • there were some discussions in particular with @herbelin about unifying glob_constr and constr_expr into a single parametric type; see CEP coq/ceps#19 , this would be very helpful as to run separate phases and still keep location info, etc...
vsiles commented

It looks like the discussion hit a dead end last year. Do you think with some external use cases we could get new traction on that direction ? It looks like a promising step towards #155 . In the meantime, I'll get a bit more familiar with 2020's Coq internals, see if I can provide more than just a use case :)

vsiles commented

By the way, it really looks like #155, so feel free to close and move the discussion there

vsiles commented

Since it's still open, I'm taking the opportunity to ask an implementation question: in vsiles@e456953 I quickly hacked what I think could be the "notation erasure" function.

As you can see there's a message when I run the new binary:

[sertop] Critical Dynlink error implementation mismatch on
Serlib__Ser_names

Does that ring any bell ?

Also, do you think that's the way to go ?

ejgallego commented

The main blocker for #155 was actually designing a flexible protocol so "internalization" [the part of the elaboration that deals with notations] would be available in some contexts.

A really big problem with exposing internalization for vernaculars is that they don't really have an internalized form in the syntax, as of today internalization of commands happens internally so we don't have a VernacDefinition ready in Coq that would allow us to modify the output format as a parameter. We can try some things in this regard, but maybe the solution in the CEP is the right one [but quite costly to implement].

ejgallego commented

Does that ring any bell ?

Umm, it seems you are using an incomplete build? Does it work if you do dune build before?

ejgallego commented

Also, I recommend you place the functions in a separate module from the beginning.

  • 👍1
vsiles commented

Does that ring any bell ?

Umm, it seems you are using an incomplete build? Does it work if you do dune build before?
So I move the code into its own module and tried again, still got this dll message:

$ eval $(opam env)
$ dune build
$ ./_build/default/sertop/sercomp.exe -Q ..,Temp --input=vernac --mode=print --omit_loc ../toto.v
[sertop] Critical Dynlink error error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "(Failure\n   \"dlopen(/Users/vsiles/.opam/coq/lib/coq-serapi/serlib/ground_plugin/serlib_firstorder.cmxs, 10): Symbol not found: _camlSerlib__Ser_loc__fun_1223\\\n  \\n  Referenced from: /Users/vsiles/.opam/coq/lib/coq-serapi/serlib/ground_plugin/serlib_firstorder.cmxs\\\n  \\n  Expected in: flat namespace\\\n  \\n in /Users/vsiles/.opam/coq/lib/coq-serapi/serlib/ground_plugin/serlib_firstorder.cmxs\")")
Inductive foo :=
  | X : _
  | Y : _.
Notation "'A'" := X.
Definition X0 := X.
Definition X1 := X.
$ coqc --version
The Coq Proof Assistant, version 8.11.0 (March 2020)
compiled on Mar 5 2020 8:39:08 with OCaml 4.08.1
$ dune --version
2.3.1
$ ocamlc --version
4.08.1

It seems to run ok... I was usually building using make. I have the same results with make and dune build directly.

EDIT: I have serapi installed in my opam switch too. Maybe it's getting confused between the local version I'm building and the one in opam ? I'll try to remove it

EDIT2: I removed serapi from my opam switch, now it doesn't run at all:

$ make clean
$ make
$ ./_build/default/sertop/sercomp.exe -Q ..,Temp --input=vernac --mode=print --omit_loc ../toto.v
Error:
       Cannot link ml-object ground_plugin.cmxs to Coq code (Fl_package_base.No_such_package("coq-serapi.serlib.ground_plugin", "")).
ejgallego commented

Installing into the opam switch will make the default paths work, however plugins will become out of date the moment you rebuild and the interface changes [so you need to reinstall again]

vsiles commented

got it running fine with dune, thanks !

  • 👍1
vsiles commented

@ejgallego Ok, my attempt seems to work "kind of"... but there's some cases where it doesn't work at all (involving inductive types e.g., not sure what's wrong).

What would be the best way to contact Coq devs and see what they think of it ? Coq-club, an issue on github ?

ejgallego commented

For these kind of questions Gitter may be the perfect spot.