Skip to content

Commit 9029b1b

Browse files
vladimiriasvladimirias
committed
Major Update
1 parent 2925999 commit 9029b1b

22 files changed

+7512
-2755
lines changed

‎Coq_patches/README

Lines changed: 91 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,99 @@
1-
This directory contains two patches for Coq-8.3pl2 written by Hugo Hereblin which are needed for proper compilation of the "Foundations" library. They are intended only as a temporary solution for the universe management issues in Coq which arise in connection with the univalent approach.
1+
This directory contains patches for Coq-8.3pl2 written by Hugo Hereblin and Dan Grayson which are needed for proper compilation of the "Foundations" library.
22

3-
The patches are to be applied in the home directory of Coq (before "make world") with the commands
4-
5-
patch -p1 < inductive-indice-levels-matter-8.3.patch
6-
7-
patch -p3 < patch.type-in-type
3+
Hugo's patches "inductive-indice-levels-matter-8.3.patch" and "patch.type-in-type" are intended only as a temporary solution for the universe management issues in Coq which arise in connection with the univalent approach.
84

95
The first of these patches changes the way the universe level of inductive types is computed for those definitions which do not specify [ Set ] or [ Prop ] as the target of the inductive construction explicitely. The new computation rule for the universe level takes into account not only the u-levels of the types occuring in the constructors but also the u-levels of types occuring in "pseudo-parametrs" i.e. in the [ forall ] expressions in the type of the inductive definition. For example, in the definition:
106

117
[ Inductive Ind ( a1 : A1 ) : forall a2 : A2 , Type := ... ]
128

139
The u-level of [ Ind ] will be the maximum of the u-level computed on the basis of types occuring in the constructors and the u-level of [ A2 ]. The u-level of [ A1 ] which the type of a parameter [ a1 ] ( as opposed to a pseudo-parameter [ a2 ] ) is not taken into account.
1410

15-
The second patch switches off the universe consistency checking in Coq which is a temporary measure which allows us to formalize interesting constructions such as [ ishinh ] and [ setquot ] without having the resizing rules.
11+
The second patch switches off the universe consistency checking in Coq which is a temporary measure which allows us to formalize interesting constructions such as [ ishinh ] and [ setquot ] without having the resizing rules.
12+
13+
Dan's patches have the following functions (see also comments in the individual patches):
14+
15+
1. "grayson-closedir-after-opendir.patch" imporoves the management of file openings/closing and eliminates in most cases the complaint that there arev too many open files.
16+
17+
2. "grayson-fix-infinite-loop.patch" this is a temporary fix for a bug in the current version of Coq's "call by need" normnalization algorithm. The patch uses a flag previously installed in the source code to switch off some optimization features of the algorthim. The need for this patch has arised because of several cases when Coq process would hang after "Admitted". In practice the patch prevents hangings but makes compilation of some of the code slower. In particular, with this patch installed the current standard library file Cycllic31.v does not compile in a reasonable amount of time (see the suggestion of how to compile Coq without much of the standard library below). It also affect the time of compilation for some of the "computation tests" in the Foundations library increasing the compilation time by a factor of >5. Hopefully, the actuall buf will be located and removed in the next update.
18+
19+
3. "grayson-improved-abstraction-version2-8.3pl2.patch" this patch dramatically improves the behavior of the [destruct] tactic making it applicable in many the cases when dependencies are present. It is not creating any complicated proof terms but simply uses the eliminator for inductive definitions in a more intelligent way than the standard [ destruct ] .
20+
21+
22+
4. "grayson-fix-infinite-loop.patch" fixes another hanging situation.
23+
24+
The following is a copy of the terminal session on my mac with the application of the patches which shows in particular the "-p" levels which have to be used in each case. It also shows how one can compile all of the Coq which is needed for the Foundations library without compiling most of the Standard Library (it takes about 5 min instead of 20 min on my computer to do it the way suggested here):
25+
26+
27+
fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ ./configure --prefix /opt/local
28+
You have GNU Make >= 3.81. Good!
29+
You have Objective-Caml 3.11.2. Good!
30+
LablGtk2 not found: CoqIde will not be available.
31+
pngtopnm was not found; documentation will not be available
32+
33+
Coq top directory : /Applications/coq-8.3pl2_two_patches_and_Dan_3
34+
Architecture : i386
35+
Coq VM bytecode link flags : -custom
36+
Coq tools bytecode link flags : -custom
37+
OS dependent libraries : -cclib -lunix
38+
Objective-Caml/Camlp4 version : 3.11.2
39+
Objective-Caml/Camlp4 binaries in : /opt/local/bin
40+
Objective-Caml library in : /opt/local/lib/ocaml
41+
Camlp4 library in : +camlp5
42+
Native dynamic link support : true
43+
Documentation : None
44+
CoqIde : no
45+
Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
46+
Coq web site : http://coq.inria.fr/
47+
48+
Paths for true installation:
49+
binaries will be copied in /opt/local/bin
50+
library will be copied in /opt/local/lib/coq
51+
man pages will be copied in /opt/local/man
52+
documentation will be copied in /opt/local/share/doc/coq
53+
emacs mode will be copied in /opt/local/share/emacs/site-lisp
54+
55+
If anything in the above is wrong, please restart './configure'.
56+
57+
*Warning* To compile the system for a new architecture
58+
don't forget to do a 'make archclean' before './configure'.
59+
fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ patch -p1 < inductive-indice-levels-matter-8.3.patch
60+
patching file kernel/indtypes.ml
61+
patching file kernel/inductive.ml
62+
patching file kernel/inductive.mli
63+
fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ patch -p3 < patch.type-in-type
64+
patching file kernel/reduction.ml
65+
fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ patch -p0 < fix-hanging-at-end-of-proof.patch
66+
patching file kernel/closure.ml
67+
fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ patch -p0 < grayson-fix-infinite-loop.patch
68+
patching file ./tactics/tactics.ml
69+
fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ patch -p0 < grayson-improved-abstraction-version2-8.3pl2.patch
70+
patching file ./configure
71+
patching file ./pretyping/evd.ml
72+
patching file ./pretyping/evd.mli
73+
patching file ./pretyping/pretype_errors.ml
74+
patching file ./pretyping/pretype_errors.mli
75+
patching file ./pretyping/unification.ml
76+
patching file ./pretyping/unification.mli
77+
patching file ./proofs/logic.ml
78+
patching file ./tactics/tactics.ml
79+
patching file ./test-suite/success/unification.v
80+
patching file ./test-suite/success/unification2.v
81+
patching file ./toplevel/himsg.ml
82+
fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$
83+
fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ patch -p0 < grayson-closedir-after-opendir.patch
84+
patching file ./lib/system.ml
85+
fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ sudo make GOTO_STAGE=2 coqbinaries states
86+
....
87+
fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ sudo make install .
88+
89+
90+
(Note : install may give error messages because some of the files it wants to move are not created by this version of the compilation process. Just ignore it. )
91+
92+
93+
94+
95+
96+
97+
98+
99+

‎Coq_patches/fix-hanging-at-end-of-proof.patch

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
diff -ub coq-8.3pl2-clean/kernel/closure.ml coq-8.3pl2-no-universe-constraints--index-levels-matter/kernel/closure.ml
2+
--- kernel/closure.ml 2010-07-28 07:22:04.000000000 -0500
3+
+++ kernel/closure.ml 2011-10-03 14:48:17.000000000 -0500
4+
@@ -17,7 +17,7 @@
5+
open Esubst
6+
7+
let stats = ref false
8+
-let share = ref true
9+
+let share = ref false
10+
11+
(* Profiling *)
12+
let beta = ref 0

‎Coq_patches/grayson-closedir-after-opendir.patch

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
This patch will leave many few file descriptors unclosed.
2+
3+
Dan Grayson
4+
5+
diff -ur ../coq-8.3pl2-clean/lib/system.ml ./lib/system.ml
6+
--- ../coq-8.3pl2-clean/lib/system.ml 2010-12-24 03:55:54.000000000 -0600
7+
+++ ./lib/system.ml 2011-10-14 12:49:30.000000000 -0500
8+
@@ -103,7 +103,7 @@
9+
(* All subdirectories, recursively *)
10+
11+
let exists_dir dir =
12+
- try let _ = opendir dir in true with Unix_error _ -> false
13+
+ try let _ = closedir (opendir dir) in true with Unix_error _ -> false
14+
15+
let skipped_dirnames = ref ["CVS"; "_darcs"]
16+

‎Coq_patches/grayson-fix-infinite-loop.patch

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
This "fixes" a seemingly infinite loop by abandoning the routine after ten repetitions.
2+
A better fix would involve understanding what the code was supposed to do.
3+
4+
Dan Grayson
5+
6+
diff -ubr ../coq-8.3pl2-clean/tactics/tactics.ml ./tactics/tactics.ml
7+
--- ../coq-8.3pl2-clean/tactics/tactics.ml 2011-04-08 11:59:26.000000000 -0500
8+
+++ ./tactics/tactics.ml 2011-10-07 09:55:24.000000000 -0500
9+
@@ -522,7 +522,10 @@
10+
11+
let pf_lookup_hypothesis_as_renamed_gen red h gl =
12+
let env = pf_env gl in
13+
+ let infinite_loop_detector = ref 0 in
14+
let rec aux ccl =
15+
+ incr infinite_loop_detector;
16+
+ if !infinite_loop_detector > 10 then raise Redelimination;
17+
match pf_lookup_hypothesis_as_renamed env ccl h with
18+
| None when red ->
19+
aux

0 commit comments

Comments
 (0)