CRGTCoq20100920

Date Mon, 20 Sep 2010

Time 10:00–12:45

Location INRIA Place d'Italie, salle verte 2

People

• Arnaud Spiwack
• Assia Mahboubi
• Bruno Barras
• Cyril Cohen
• Élie Soubiran
• Enrico Tassi
• Guillaume Melquiond
• Hugo Herbelin
• Jean-Marc Notin
• Julien Forest
• Matthias Puech
• Pierre Boutillier
• Pierre Courtieu
• Pierre Letouzey
• Ronan Saillard
• Stéphane Glondu
• Tom Hutchinson
• Vincent Siles
• Yann Régis-Gianas

Optimizations

Yann presented some experiments he did to improve performances.

Hash-consing

General presentation about hash-consing. The focus of the talk is on "constr" (i.e. Coq terms in the OCaml world).

Coq's implementation is based on OCaml's generic hash function, which generates a lot of collisions for deep terms. The compilation of a simple file:

Definition N := $1.

doesn't scale for big values of $1.

Yann modified hashing so that it is performed on the whole term, with a "local cache" on each node (this changes the constr type). This causes ~10 % loss of efficiency, but the simple test above does scale. By interleaving the computation of the hash value and the hash consing, and also by optimizing the hash table representation, he manages to get the original performances.

.vo marshalling

Yann optimized the -dont-load-proof option. Instead of unmarshalling a whole file and removing opaque constants, the opaque bodies are put in a separate table that is unmarshalled only when needed. Gain: ~10 %, "Require" more reactive. It is committed in trunk.

We might want to remove -dont-load-proof altogether, and lazily load opaque bodies on demand... later.

Representation of identifiers

With a perfect hash function (collecting all identifiers occuring in the standard library, and replacing them with an int), Yann got a 10 % gain: this is the maximum that can be expected. He tried many things, but nothing stands out.

General remarks

• Pervasives.compare is used too much in Coq and prevents more aggressive optimizations.
• Implementing our own marshalling function would provide great flexibility (but achieving OCaml's performances might be tricky).
• Hash-consing could be used more often.

ADT "interfaces"

In October, not during TYPES 2010.

Possible talks:

• Tom
• Enrico Tassi (Matita)
• Makarius (Isabelle/Scala)

Adding Eta

Hugo presented his changes to include eta (for lambda) in conversion. Rationale: it is no worse than the current situation w.r.t. the set model. Patching the kernel and type inference poses no problem. Patching unification in tactics poses some compatibility issues. Bruno points out that comparing two terms with different types might be problematic. Arnaud wonders why we would add eta for lambda, but not for other constructions of the language. Hugo answers that it is very easy for lambda, but not so much for others.

No changes were done in pattern unification... eta should be taken care of there.

The changes will be committed soon.

General discussion

• HH: the bug-tracker is too complex, in particular:
  • the UNCO/NEW states
  • priorities
  • the different kinds of resolutions
• HH: asks for a volunteer to triage new bugs
• PB: younger people might not have enough experience to assess whether a certain behaviour is expected or not
• JMN: it should be done collectively
• PL: basic search settings exclude UNCO bugs
• AS: there is too much bureaucracy for such a small organization
• JMN: categories are hard-coded in the (MySQL) database and cannot be changed (easily), but putting new bugs directly in NEW (instead of UNCO) should be possible... and will be done
• What about simplifying the web interface?
• HH: PB triages bugs, and asks PL for difficult stuff
• HH: the trunk should be stabilized
• HH: wonders if he can assign bugs more aggressively, everyone agrees
• JF: the bench should give the last working revision, in addition to the date
• JMN: http://coq.inria.fr/newbench, will be announced on coqdev soon
• Bug 2222: HH asks which of typeclass resolution or goal-directed unification should be prioritized... most of people agree typeclass resolution should be done last
• Focus on bug 2212
• HH: unification is more powerful in 8.3, and generates more uninstantiated evars... he proposes a heuristic to automatically instantiate them at Qed time (e.g. with eauto)
• Complaint: side-effects on global definitions should not be done in unrelated libraries, or more generally, "Require"-ing a library should not change behaviours of existing stuff, such as implicit arguments. Program is blamed. If implicit-related stuff needs changing, this must be done next to the definition.
• AS: explains the new semantics of {Global,Local,} {Set,Unset}. There is a known incompatibility, what used to be "Set" should be "Local Set" now.
• Release management: there were too many changes (in particular, new features) between 8.3 beta and rc. There should be more discipline in release branches...
• 8.3: we freeze changes in two days, and release by the end of the week.