1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
AddPath "/toto".
Anomaly: Uncaught exception Unix.Unix_error(20, "stat", "/toto").
Please report.
--> CORRIGE
Declaration de Local a l'interieur d'un but ...
Certains Clear deviennent impossible car la variable apparait dans
un lemme local, c'est plutot sain ...
La syntaxe <A>x=y est parfois refusee
Les arguments des Tactic Definition sont interpretes avant
l'application de la tactique, ils ne peuvent pas contenir des variables
qui seront introduites dans la tactique ....
MUTUAL-EXCLUSION/binary/version1/Soundness.v
--> Il y a aussi une anomalie :
fntf1 < (SolveCycleNode1 H '(not_true_is_false (hd o))).
Toplevel input, characters 0-47
> (SolveCycleNode1 H '(not_true_is_false (hd o))).
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Anomaly: Illegal application: (APP SolveCycleNode1 H
(COMMAND
(APPLIST (QUALID not_true_is_false)
(APPLIST (QUALID hd) (QUALID o))))).
l'entree numarg de g_tactic.ml4 accepte aussi des id... (pour les
binding je pense) d'ou des erreurs de syntaxe ... pure_numarg est
plus sûr
REPONSE PROVISOIRE: si c'est pour Specialize, faudrait en changer la
syntaxe, elle est incompatible avec L_tac.
CONTRIBS
---------
BellLabs/lazyPCF : OK
Bordeaux/TREES :
Bordeaux/Additions :
echecs sur Realizer
Bordeaux/GROUPS : OK
Bordeaux/EXCEPTIONS : OK
Dyade/Otway-Rees : OK
Dyade/BDD :
File "./bdd4.v", line 122, characters 10-28
Error: Tactic generated a subgoal identical to the original goal.
Lyon/AUTOMATA : OK
Lyon/CIRCUITS : OK
Lyon/COINDUCTIVES :
File "./Examples.v", line 276, characters 0-764
Error: Incorrect elimination of H in the inductive type
eq
The elimination predicate
[a1:A; _:((hd (Cons s0 H))=(hd (Cons s a0))); a2:A]
(EqSt2 A (Cons s0 H) (Cons a2 a0)) has type
A->(hd (Cons s0 H))=(hd (Cons s a0))->A->Prop
It should be one of :
(a:A)(hd (Cons a0 s0))=a->Prop, (a:A)(hd (Cons a0 s0))=a->Set,
A->Prop, A->Set
File "./Specified_Streams.v", line 11, characters 0-132
Error: Illegal application (Type Error):
The term SStream of type (A:Set)(nat->A->Prop)->Set
cannot be applied to the terms
A : Set
x : (SStream A P)
The 2nd term has type (SStream A P) which should be coercible to
nat->A->Prop
Lyon/IEEE754 : OK
Rocq/GRAPHS
/home/cpaulin/TYPES/V7/bin/coqc -q -I . lsort
Utilise NewInduction
/home/cpaulin/TYPES/V7/bin/coqc -q -I . cgraph
Warning: Found several default clauses, kept the first one
File "./cgraph.v", line 1866, characters 2-7
Error: frontier was handed back a ill-formed proof.
(Apres un EApply)
Rocq/MUTUAL-EXCLUSION/
Incompatibilite interpretation des arguments de Tactic Definition
Rocq/COC
Realizer dans Conv_Dec.v, Expr.v, Infer.v, Machine.v MyList.v Names.v
File "./Int_typ.v", line 209, characters 30-44
Error: In environment
int_typ : term->intP->(s:skel)(Can s)
T : term
ip : intP
s : skel
A : term
B : term
_ : skel
_ : skel
s1 := s : skel
The term (default_can s1) has type (Can s1)
while it is expected to have type (Can (PROD _ s1))
Rocq/ALGEBRA/RELATIONS/Relations.v
--> Un problème de Coercion au discharge
Rocq/ARITH/Chinese
File "./Zdiv.v", line 34, characters 0-944
--> Un Refine mal typé et des Realizer
Rocq/PARADOXES
File "./Reynolds1.v", line 105, characters 0-429
Error: checking of theorem per_F0 failed... aborting
Rocq/CHECKER OK
Rocq/COMPILER OK
Rocq/DEMOS OK
Rocq/HIGMAN OK
Rocq/LAMBDA OK
Rocq/SHUFFLE OK
Rocq/SCHROEDER
File "./Schroeder.v", line 351, characters 4-52
Anomaly: type_of: variable h1 unbound. Please report.
--> Pb de "Remark" local à un thm pas pris en compte dans
l'environnement de la preuve de ce théorème
Rocq/SUBST
File "./TS.v", line 69, characters 0-6
Error: Attempt to save an incomplete proof
Montevideo/CtlTctl OK
Montevideo/RailroadCrossing OK (TemporalOperators.v ne doit pas etre compile)
Nijmegen OK
Utrecht/Ramsey OK
Utrecht/ABP
coqc -q -I . abp_base
File "./abp_base.v", line 42, characters 0-154
Error: Cannot declare a variable or hypothesis over the term Y
because this term is not a type.
|
