The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Thu, 10 Mar 2011 00:39:09 -0500,
Tom Prince 
<tom.prince AT ualberta.net>
 a écrit :

> On 2011-03-09, Aaron Bohannon wrote:
> > I would love to see improvements/extensions to Coq's standard
> > library. As a whole, it seems to be in rough shape.
> > 
> > As a prerequisite for such improvement, it seems critical to develop
> > an official, written, agreed-upon style guide that is as thorough
> > and detailed as possible. 
> > <...>
> 
> I certainly think that this is a laudable goal. I worry however, that
> this sets that bar too high. Certainly, there should be style
> guidelines, and the should be ahered to. I think that requiring that
> the library be a oerfect model would discourage many potential
> contributors. And I think that any definition of perfect is going to
> vary, over time, as the features provide by Coq change and improve.
> 
> I can't write perfect code, and I don't think I would be qualified to
> judge code perfect. I think that a better criterion would be, at least
> as good as the standard library, perferably better.

I agree with you, but I think that it shouldn't be required to write
"perfect code", but rather "perfect types" (and in particular perfect
names), because code is often not that important in Coq.
Then the way you write your proofs has an impact on speed and memory,
but that is not really important, as later someone can modify the
proof, to make it better without breaking your proofs (as they are
opaque).

> On a differnt tack, I wonder how much potentially generally useful
> code is written for one off task or projects, and then is forgotten
> about. I think there is value in collecting these snippets, and
> improving upon them. The coq-contribs repository does the first part
> of this, collecting the code. But to my knowledge, aside from the few
> contributions that are still being actively developed by outside
> groups, the code is static (barring compatibility updates).
> 
> Also, there is the issue of compatibility. There needs to be a balance
> between improving the library, and supporting code that worked against
> older versions. It wouldn't surprise me if a number of the perceived
> deficiencies of the standard library are due to the requirement to be
> backwards compatible. I think to a certain extent, both the goals
> that I outlined above run counter to maintaining backward
> compatibility. I don't think this is an insurmountable challenge, but
> certainly, at points it will lead to non-perfect code.

In fact, I am often wondering if libraries shouldn't be distributed in
2 forms: the actual form of coq libraries and some kind of
"pre-compiled" version, that is a version with only raw terms in
gallina, instead of proofs using tactics, the second version should be
automatically "generatable" (I don't know the word), that is it should
mainly consist in a script doing
"Deactivate Notation Display. Print [term1]. … Print [termn]." >
[precompiled.v].
(or "Eval simpl in [term1]. … Eval simpl in [termn]." to get some minor
optimizations)

The good points in that are that if you want to update coq from sources,
using precompiled theories should be faster than the actual theories to
build, and that most coq upgrades won't break the code in theories
that often (as code-breaks are often due to changement in behaviour
of tactics).
The bad points are that if the source library doesn't compile anymore,
then the precompiled is likely to be frozen, as its code is often not
maintainable and that the size of files may tend to explode (but
anyway should be kept almost linear in size of the "vo" compiled files).

>   Tom Prince
> 
> P.S. In case it wasn't clear from my rambling, I am in support of some
> sort of ExtLib.