The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

On Thu, Mar 10, 2011 at 3:45 AM, AUGER Cedric <Cedric.Auger AT lri.fr> wrote:

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

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).

Linear would be good but I'm also a little worried about the constant. It isn't uncommon for some of my vo files to be >1M so paying a small constant can mean a non-trivial amount of space (not that bits cost much these days). It seems like what we really want is a stable binary format (not dependent on the ocaml version and not changing much between at minor versions at least). Has there been any work on something like this?

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

-- 
gregory malecha