Stream: Coq workshop 2020

Topic: [S6] Learning to Format Coq Code Using Language Models

Théo Zimmermann (Jun 24 2020 at 11:20):

This is the topic to ask questions on the talk "Learning to Format Coq Code Using Language Models".

Emilio Jesús Gallego Arias (Jul 05 2020 at 14:39):

Talk will start in 5 minutes

Christian Doczkal (Jul 05 2020 at 14:53):

:rolling_eyes:

Enrico Tassi (Jul 05 2020 at 14:57):

Q: you mentioned that rule-based tools don't work very well in practice. But your example about Qed not being in a new line is trivial to capture with a rule. What about mixing the two approaches?

Yves Bertot (Jul 05 2020 at 14:57):

The proof goal structure is important, we really need you to find a way to incorporate this into the treatement.

Enrico Tassi (Jul 05 2020 at 15:00):

Remark: I find it amazing that you manage to indent SSR code without running Coq (indentation is based on the number of open goals, which you are apparently predicting correctly). Wow!

Yves Bertot (Jul 05 2020 at 15:01):

The by keywords make it posible to reconstruct the number of goals, but you need lookahead.

Christian Doczkal (Jul 05 2020 at 15:02):

For the record: the reglang library is not aspiring to adhere to the mathcomp coding guidelines, in particular not as it comes to indentation and the use of bullets.

Karl Palmskog (Jul 05 2020 at 15:11):

this was not intended to disparage reglang, just to show how the tool can be applied to "new" projects (outside the training corpus). Probably, proper formatting of reglang would require additional training on reglang itself

Karl Palmskog (Jul 05 2020 at 15:13):

Yves Bertot said:

The by keywords make it posible to reconstruct the number of goals, but you need lookahead.

Right, the current model simply uses the keywords like by to infer indentation without running Coq. We have some WIP in SerAPI on accessing the proof goal structure in SerAPI, but it's not 100% clear to me how one would express a "proof goal location for a token" in a good way.

Karl Palmskog (Jul 05 2020 at 15:27):

for the record, the current main limitations:

• we don't make any special arrangements for the fact that bullets are complete sentences in themselves - this should probably be handled at the feature extraction stage
• the limited lookahead prevents handling the complex condition for line break before Qed (if X number of chars before it, then Y else Z). This should probably also be handled in feature extraction by special treatment of Qed and Defined.

Karl Palmskog (Jul 05 2020 at 15:29):

here is the complete prediction for polydiv.v which shows these issues quite clearly. However, I think it also shows that one can get quite far without much special treatment of Coq features.

Last updated: Jun 01 2023 at 12:01 UTC