The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Thank you very much for your comments. I was not sure what is the proper way 
of doing things in this case. Starting from the next update I will only 
include .v files . 

Vladimir.






On May 18, 2011, at 5:43 AM, Robin Green wrote:

> 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