1. Jelle Herold
  2. htt

Commits

Jelle Herold  committed ad725b5

initial import

  • Participants
  • Branches master

Comments (0)

Files changed (1)

File BUILDSCRIPT

View file
+#! /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 .