Coq Call 2020 07 15 - coq/coq GitHub Wiki

• July 15th 2020, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

(postponed from two weeks ago)

• 8.12 issues:

  • https://github.com/coq/coq/issues/12564
  • https://github.com/coq/coq/issues/11178
  • https://github.com/coq/coq/issues/11107#issuecomment-567040281

• Meta-topic: how to avoid last-minute cancelled Coq Calls [everybody]

• A few questions on problems with the current Hint implementation [Emilio]

• The various kinds of syntax for global references and what to call them (https://github.com/coq/coq/pull/12568#issuecomment-648298048) (Jason)

• Figure out what to do with #10652 Generate parsing statistics (Jim)

• Action on https://github.com/coq/coq/pull/11791 [Emilio]

Notes

How to avoid last minute cancellation?

Several options were discussed:

• One poll every month to get an overview of who is going to be there.
• Matthieu or his representative announces whether the Call will take place on the eve of the meeting.
• People who plan to be there register on the wiki page.
• Topics should list who needs to be there for the topic to be discussed.

For the rest of the summer, Emilio is going to prepare a poll (first option).

PR of Jim on generating statistics

People think it could be useful but it's not clear whether we want to maintain this in-tree. OTOH, Jim doesn't like the idea of maintaining a branch for this out-of-tree. Hugo is going to have a look at the code. We should also get the opinion of Pierre-Marie and users with this kind of expertise like Karl.

Most of the code is currently in doc_grammar, which Jim already maintains.

This PR also contains a general framework to accumulate statistics in CI.

jfehrle: Putting the code into a branch was very briefly mentioned but not discussed. My thoughts on that are here in #10652 comment.)

Discussing and documenting smart_global

Currently, there might be an inconsistency regarding where only true global references designated by their qualified identifiers, abbreviations, or notations denoted by strings are accepted. There is also the question of how to name them given how non-descriptive "smart_global" is.

The result of the discussion is to go for "reference" as the name to designate "smart_global", i.e. what is parsed as either a qualid or a string representing a notation and interpreted as a Gallina object (which is the head constant of the abbreviation / notation in these cases).

On the other hand, in Locate and Print which also accept the same syntax but treat the two differently, we won't use this nonterminal name anymore.

Finally, we should rename the Tactic Notation entries: reference should become qualid since it only parses qualified identifiers and reference should accept the same as today's smart_global.