[sertop] Add sername program for serialization of terms #207

palmskog · 2020-05-28T20:00:55Z

This targets the v8.10 branch and is intended for inclusion in the 0.7.1 release of SerAPI for Coq 8.10. The sername program is used by our Roosterize toolchain for suggesting Coq lemma names. The sername program will be forward-ported to the v8.11 branch after the Roosterize toolchain is released.

cc: @pengyunie

…module on initialization

… de Bruijn indexed constrs

…ized terms

…ot just constant types)

palmskog · 2020-05-28T20:04:38Z

Note that compilation of the v8.10 branch with sexplib 0.13.0 and dune 2.5.1 currently gives errors like the following:

File "serapi/serapi_protocol.mli", line 293, characters 23-32:
Error (warning 3): deprecated: Sexplib.Conv.sexp_list
[since 2019-03] use [@sexp.list] instead

... unless one compiles with dune build --profile=release. @ejgallego is this something you want to address before the 0.7.1 release or can we just go ahead and release after merging this PR?

ejgallego · 2020-05-28T20:13:38Z

@ejgallego is this something you want to address before the 0.7.1 release or can we just go ahead and release after merging this PR?

I'm aware of this problem, and some other problems that newer toolchains do introduce. Not sure what we should do here. I'd like to avoid an upper constraint if necessary.

ejgallego · 2020-05-28T20:14:28Z

@palmskog , how does this relate to #174

palmskog · 2020-05-28T20:22:06Z

@palmskog , how does this relate to #174

It's not directly related, but both fit into an overall plan on learning and suggesting code conventions for Coq. The work on lemma name suggestions (primary use of sername) doesn't use tactic or proof state serialization at all.

However, the extended abstract recently accepted at the Coq workshop looks at suggesting spacing, which does use tactic/proof data for learning, but does not use sername at all.

ejgallego · 2020-05-28T20:29:44Z

I see, thanks for the explanation, adjust #174 plans as you think then; I will prepare a release shortly [actually for both v8.11 and v8.10]

palmskog · 2020-05-28T20:32:53Z

I see, thanks for the explanation, adjust #174 plans as you think then; I will prepare a release shortly [actually for both v8.11 and v8.10]

Ah, so you think you can forward port to v8.11 easily? That would be great. Let me know if I can help in some way, e.g., writing release notes.

ejgallego · 2020-05-28T21:00:24Z

Ah, so you think you can forward port to v8.11 easily? That would be great. Let me know if I can help in some way, e.g., writing release notes.

I can give the forward porting a go myself; I don't expect any particular trouble. I will do 8.10 first, then 8.11

ejgallego · 2020-05-29T12:23:38Z

sertop/sername.ml

+     sdoc
+     *)
+     let doc,sid = Stm.new_doc ndoc in
+     let sent = Printf.sprintf "Require %s." l in


Why are you not adding this to require_libs above?

You mention a problem in the commit, but with no further details given it is hard to say more.

ejgallego

I'm not sure I like the way this PR is going; the batch tools are meant to process files, we cannot affort to add a binary for every possible query system.

For this use case, there is little improvement of this solution vs using the standard query protocol from sertop.

I understand the current query system is not featureful enough as to support this use case, see #155 and #196 for example, but I'm working on fixing those right now.

This is thus a tool that in principle, I'm not willing to support in future releases [I'm very open to be convinced to do so tho] .

Instead, improved printing options will be added so sertop can do what sername does using the query language.

For the 0.7 branch; I'm OK merging this PR, as long as the tool documentation states that this tool won't be available in future releases and sertop must be used.

What do you think @palmskog ? Am I off in my point of view?

1.4 is required for fmt 1.0

ejgallego · 2020-05-29T12:59:28Z

Pushed a fix for Travis and warning on newer sexplib, let's see how it goes.

This should fix Travis on newer sexplib, and still keep compat with 0.12. We also fix Coq's Travis install [wrong version picked for this branch]

palmskog · 2020-05-29T15:12:56Z

For the 0.7 branch; I'm OK merging this PR, as long as the tool documentation states that this tool won't be available in future releases and sertop must be used.

This is fine by me. Do you want the statement about future releases in sername --help or in the release notes? You can let me know or just add it for yourself.

As for the require_libs code comment, if we don't keep sername in future versions, maybe we can just leave that code as is? There was a very specific use case that motivated that change which I may have to dig quite a lot to find.

ejgallego · 2020-05-29T15:36:21Z

This is fine by me. Do you want the statement about future releases in sername --help or in the release notes? You can let me know or just add it for yourself.

Thanks @palmskog , I can add a small note myself.

As for the require_libs code comment, if we don't keep sername in future versions, maybe we can just leave that code as is? There was a very specific use case that motivated that change which I may have to dig quite a lot to find.

That's fine then.

Something it would be very useful to have tho is a small test case that covers all the things this tool does; this way we can be sure Query name does support the required functionality if we deprecated sername

ejgallego · 2020-05-30T12:59:43Z

Thinking a bit about it, I propose we mark sername deprecated in 8.11/8.12 once can be done with Query, but don't remove it, at least until it becomes a problem for maintenance.

sertop/sername.ml

ejgallego · 2020-05-30T13:32:12Z

This is also perfectly fine with me. However, unless I'm missing something, I think the main obstacle to turning sername into a simple query separate from Coq's API is the use of detyping here. Would this best be solved by adding another query function?

See ejgallego/coq-lsp#331 and #196 , they request precisely that.

ejgallego · 2020-06-02T12:28:20Z

@palmskog this is ready IMO, can you have a look to the two latest commits?

Maybe I do push a few tweaks to ease forward-porting, but no code changes themselves.

palmskog · 2020-06-02T12:53:49Z

@ejgallego the last two commits look good to me.

@palmskog

CHANGES: * [sertop ] Add `sername` program for batch serialization elaborated terms Note that this utility will be deprecated in future versions, to be subsumed by `Query`. (rocq-archive/coq-serapi#207, @palmskog, with help from @ejgallego) * [serlib ] Expose `QueryUtil.info_of_id` and `gen_pp_obj` in `serapi_protocol.mli` to enable using them in `sername` to retrieve serialized body-type pairs (@palmskog) * [general] Improved compat with Jane Street v0.13 toolchain * [serlib ] Only use `ssreflect` from Coq in tests (@ejgallego)

@palmskog

CHANGES: * [sertop ] Add `sername` program for batch serialization elaborated terms Note that this utility will be deprecated in future versions, to be subsumed by `Query`. (rocq-archive/coq-serapi#207, @palmskog, with help from @ejgallego) * [serlib ] Expose `QueryUtil.info_of_id` and `gen_pp_obj` in `serapi_protocol.mli` to enable using them in `sername` to retrieve serialized body-type pairs (@palmskog) * [general] Improved compat with Jane Street v0.13 toolchain * [serlib ] Only use `ssreflect` from Coq in tests (@ejgallego)

palmskog added 10 commits May 28, 2020 14:44

[sertop] Add sername program

98e98c2

[sername] Add basic printing of terms

fa70044

[sername] Use detyping to get term without de Bruijn indices

db82bdc

[sername] Add option --require-lib to sername for loading a custom …

1873f9a

…module on initialization

[sername] Add option for disabling printing of prettified constrs and…

282fd3f

… de Bruijn indexed constrs

[sername] Workaround for issue with error on load for some files

95c10e5

[doc] Improve sername documentation

8546a0a

[serlib] Expose some key functions needed by sername to obtain serial…

e86b502

…ized terms

[sername] Add --body option to allow serializing constant bodies (n…

f266c4c

…ot just constant types)

[doc] Add changes for 0.7.1

441f5cd

palmskog requested a review from ejgallego May 28, 2020 20:01

palmskog added kind: enhancement kind: serialization labels May 28, 2020

ejgallego self-assigned this May 28, 2020

ejgallego reviewed May 29, 2020

View reviewed changes

ejgallego added this to the 0.7.2 milestone May 29, 2020

[build] Correct dune version.

40760cd

1.4 is required for fmt 1.0

[travis] [build] Disable warnings for sexplib >= 0.13, fix Coq version

000dac6

This should fix Travis on newer sexplib, and still keep compat with 0.12. We also fix Coq's Travis install [wrong version picked for this branch]

ejgallego force-pushed the v8.10+sername branch from 8a79ef2 to 000dac6 Compare May 29, 2020 13:11

palmskog commented May 30, 2020

View reviewed changes

sertop/sername.ml Show resolved Hide resolved

ejgallego modified the milestones: 0.7.2, 0.7.1 Jun 2, 2020

ejgallego added 2 commits June 2, 2020 14:06

[changes] Note about sername future.

f3323d5

[sername] Add small test.

13064aa

ejgallego merged commit d424aef into v8.10 Jun 2, 2020

ejgallego deleted the v8.10+sername branch June 2, 2020 14:04

ejgallego mentioned this pull request Jun 2, 2020

[new release] coq-serapi (8.10.0+0.7.1) ocaml/opam-repository#16564

Merged

ejgallego mentioned this pull request Jun 2, 2020

[sercomp] Forward port of sername #209

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[sertop] Add sername program for serialization of terms #207

[sertop] Add sername program for serialization of terms #207

palmskog commented May 28, 2020 •

edited

Loading

palmskog commented May 28, 2020 •

edited

Loading

ejgallego commented May 28, 2020 •

edited

Loading

ejgallego commented May 28, 2020

palmskog commented May 28, 2020 •

edited

Loading

ejgallego commented May 28, 2020

palmskog commented May 28, 2020

ejgallego commented May 28, 2020 •

edited

Loading

ejgallego May 29, 2020

ejgallego May 29, 2020

ejgallego left a comment

ejgallego commented May 29, 2020

palmskog commented May 29, 2020

ejgallego commented May 29, 2020 •

edited

Loading

ejgallego commented May 30, 2020

ejgallego commented May 30, 2020

ejgallego commented Jun 2, 2020 •

edited

Loading

palmskog commented Jun 2, 2020

[sertop] Add sername program for serialization of terms #207

[sertop] Add sername program for serialization of terms #207

Conversation

palmskog commented May 28, 2020 • edited Loading

palmskog commented May 28, 2020 • edited Loading

ejgallego commented May 28, 2020 • edited Loading

ejgallego commented May 28, 2020

palmskog commented May 28, 2020 • edited Loading

ejgallego commented May 28, 2020

palmskog commented May 28, 2020

ejgallego commented May 28, 2020 • edited Loading

ejgallego May 29, 2020

Choose a reason for hiding this comment

ejgallego May 29, 2020

Choose a reason for hiding this comment

ejgallego left a comment

Choose a reason for hiding this comment

ejgallego commented May 29, 2020

palmskog commented May 29, 2020

ejgallego commented May 29, 2020 • edited Loading

ejgallego commented May 30, 2020

ejgallego commented May 30, 2020

ejgallego commented Jun 2, 2020 • edited Loading

palmskog commented Jun 2, 2020

palmskog commented May 28, 2020 •

edited

Loading

palmskog commented May 28, 2020 •

edited

Loading

ejgallego commented May 28, 2020 •

edited

Loading

palmskog commented May 28, 2020 •

edited

Loading

ejgallego commented May 28, 2020 •

edited

Loading

ejgallego commented May 29, 2020 •

edited

Loading

ejgallego commented Jun 2, 2020 •

edited

Loading