The Coq mailing list

[Jelle Herold <jelle AT defekt.nl>]

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