Adding a mode to sercomp to get rid of all notations

[vsiles]

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]

Hi @vsiles ,

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

• you could consider this a duplicate of Print a sentence with the notation interpretation, scope resolution, and explicit arguments rocq-community/rocq-lsp#331 , 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 [CEP 012] Roadmap for Public OCaml Interfaces. rocq-prover/rfcs#19 , this would be very helpful as to run separate phases and still keep location info, etc...

[vsiles]

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 rocq-community/rocq-lsp#331 . 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]

By the way, it really looks like rocq-community/rocq-lsp#331, so feel free to close and move the discussion there

[vsiles]

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]

The main blocker for rocq-community/rocq-lsp#331 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]

Does that ring any bell ?

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

[ejgallego]

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

[vsiles]

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]

You need to run sercomp with the proper ocaml env, dune provides dune exec -- for that purpose, see SerAPIs FAQ: https://github.com/ejgallego/coq-serapi/blob/v8.11/FAQ.md#i-get-an-error-cannot-link-ml-object- and https://github.com/ejgallego/coq-serapi/blob/v8.11/notes/build.md#executing-built-binaries

[ejgallego]

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]

got it running fine with dune, thanks !

[vsiles]

@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]

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