The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

I do not know how to answer your question but just one comment on the whole 
situation. The reason patched coq does not build with the usual make is that 
the compilation of some of the standard library files hangs. This is in turn 
caused by the patch which switches off sharing in the computation algorithm 
which makes some of the computations/normalizations used in the standard 
library very very slow.

This patch was and is intended as a temporary measure until someone fixes a 
bug in the sharing algorithm which leads to the hanging of the system in some 
other situations which occur in the Univalent library. I know that both Hugo 
and George and probably many others are aware of this bug. May be it's time 
to have it fixed?

Vladimir.

  



On Mar 26, 2012, at 10:24 AM, Jelle Herold wrote:

> Hello,
> 
> To work with Vladimir Voevodsky's code you need a patched Coq. Once
> patched, it is suggested[1] Coq is build using:
> 
> make GOTO_STAGE=2 coqbinaries states
> make install
> 
> (building without GOTO_... fails)
> 
> While this works there are two problems:
> 
> 1) coqdep is not build, coqdep_boot is there, but that seems not to be
> the same thing...?
> 2) coqc.opt is build, but not the coqc binary/symlink
> 
> The 2nd is not such a big deal, but can I somehow build coqdep?
> 
> [1]
> https://github.com/vladimirias/Foundations/blob/master/Coq_patches/README
> 
> Any thoughts?
> 
> Thanks a lot,
> 
> Jelle.
> 
> PS. Here is a script that builds coq as described.
> 
> ----
> 
> #! /bin/sh
> # shell script to compile and patch coq for HoTT work
> set +x
> git clone https://github.com/vladimirias/Foundations.git
> curl -L http://coq.inria.fr/distrib/8.3pl2/files/coq-8.3pl2.tar.gz ;| tar
> xzvf -
> #tar xjvf coq-8.3pl2.tbz
> cd coq-8.3pl2
> ./configure -with-doc no -local #-coqide no
> ln -s ../Foundations/Coq_patches patches
> patch -p1 < patches/inductive-indice-levels-matter-8.3.patch
> patch -p3 < patches/patch.type-in-type
> patch -p0 < patches/fix-hanging-at-end-of-proof.patch
> patch -p0 < patches/grayson-fix-infinite-loop.patch
> patch -p0 < patches/grayson-improved-abstraction-version2-8.3pl2.patch
> patch -p0 < patches/grayson-closedir-after-opendir.patch
> time make GOTO_STAGE=2 coqbinaries states
> time make install