The Coq mailing list

["Robin Green" <greenrd AT greenrd.org>]

Hi Vladimir,

Just a purely technical point about your git repository, albeit an
important one. I address this email both to you and to any of your
collaborators who might be unaware of this problem. Apologies for the
length, and you can just skip to the bottom for the solution (and my offer
to do it).

It is standard practice for public repositories - I think even for
repositories of Coq files - *not* to include files generated by a
compilation process. In particular, the .vo files can become rather
enormous in comparison to the .v files. Including .vo files, as you have
done, causes the following problems in this case:

1. Because git operates by storing enough information to reconstruct
*every* revision of every file in every copy of the repository, each
repository is a complete copy (of at least the main branch, anyway). This
means each potential collaborator that checks out the repository from
github has to receive all this data, and the minimum amount of data
transfer required for a new checkout can only grow. (Provided that no
revisions are deleted, that is. It is not standard practice to delete
revisions in published git repositories because it can cause problems for
collaborators.) As more revisions containing .vo files are added, the
amount of mostly-useless data that has to be transferred upon performing
an initial checkout will only grow, so the problem gets worse over time.
Its size is proportional to the product of the number of proofs etc., the
length of the proofs, and the number of revisions. As someone who has to
pay my ISP for excess downloads (which is not at all uncommon around the
world), this slightly concerns me.

A text-only git repository would of course still grow on every commit, but
far more slowly.

2. The .vo files are binary, and are generated anew as necessary, and git
does not store multiple revisions of binary files particularly
efficiently. So not only are the .vo files going to be large, they also
will not be stored efficiently, compounding the problem.

3. Github has unpublished "soft limits" on free accounts, and may require
you and/or all github users who have forked your repository to subscribe
to a paid account if your repository/repositories become, in their view,
"huge". An avoidable annoyance, at the very least.


SOLUTION:

These problems can be addressed by scheduling the generated files for
deletion in the next commit (using the git rm command), and then creating
and committing a file named precisely .gitignore in the top-level
directory of the repository, specifying the file types to be ignored. A
suitable .gitignore file for Coq projects can be found here:

https://github.com/github/gitignore/raw/master/Coq.gitignore

and can be used without changes.

Of course one can make the .vo files and any other generated files
available in a separate downloadable archive. I just do not think it is a
good idea to include them in the repository itself, and I think many
others on this list would agree with me. I see that Dan Grayson has
already forked your repository on github and tried to remove all generated
files.

It's also standard practice to include a file to automate the compilation
(typically a Makefile), as Dan Grayson has done in his fork. That way
people can reproduce the full compilation conveniently, without having to
download all the old revisions of the compiled files.

If you want, I can take care of all of this for you - including generating
archives with generated files if you want - and you can just pull my
changes into your repository.

Regards,
Robin Green