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
|
Hints Resolve fait une anomalie si la constante n'existe pas
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
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 : echec sur Realizer
Bordeaux/Additions : echec sur Realizer
Bordeaux/SearchTrees : echec sur Realizer
Bordeaux/GROUPS : OK
Bordeaux/EXCEPTIONS : OK
Dyade/Otway-Rees : OK
Dyade/BDD :
File "./bdd4.v", line 122, characters 10-28
<<<<<<< PROBLEMES
Error: Tactic generated a subgoal identical to the original goal.
Lyon/AUTOMATA : OK
Lyon/CIRCUITS : OK
Lyon/COINDUCTIVES :
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
--> Out of memory après plus de 500Mo utilisés
Lyon/IEEE754 : OK
Rocq/MUTUAL-EXCLUSION : échec sur Realizer
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
Problème d'alias dépendant dans un Cases (idem SUBST)
Rocq/ALGEBRA/SETOIDS
--> Token "=_S" non reconnus
Rocq/ARITH/Chinese
File "./Zdiv.v", line 34, characters 0-944
--> Un Refine mal typé et des Realizer
Rocq/GRAPHS
File "./cgraph.v", line 2628, characters 14-46
Anomaly: Search error. Please report.
Rocq/PARADOXES OK
Rocq/CHECKER OK
Rocq/COMPILER OK
Rocq/DEMOS OK
Rocq/HIGMAN OK
Rocq/LAMBDA OK
Rocq/SHUFFLE OK
Rocq/THREE_GAP OK
Rocq/ZF OK
Rocq/SUBST
File "./inversionSL.v", line 215, characters 38-39
Problème d'alias dépendant dans un Cases
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/TreeAutomata
File "./defs.v", line 309, characters 34-47
Error: Not a recursive eliminator: some induction hypothesis is lacking
--> Bug NewInduction...
File "./lattice_fixpoint.v", line 29, characters 44-57
--> Problème de lookup_eliminator (effet de bord sur le schéma d'élimination)
Rocq/RATIONAL
--> Des fichiers ML à porter
Lyon/AUTOMATA OK
Lyon/CIRCUITS OK
Lyon/COINDUCTIVES OK
Lyon/IEEE754 OK
Lyon/PROCESSES OK
Lyon/PROGRAMS : Nécessite Programs.v
Lyon/STREAMS OK
Lyon/FIRING-SQUAD : des identificateurs avec le symbole $ !! (plus autorisé)
Lyon/INSERTION-SORT : Nécessite Programs.v
Lyon/DISTRIBUTED_REFERENCE_COUNTING
File "./fifo.v", line 181, characters 0-6
Error: Attempt to save an incomplete proof
--> Preuve incomplète (lié à Intuition)
Rocq/MM
Marseille/CCS OK
Marseille/CIRCUITS -> Realizer
Montevideo/CtlTctl OK
Montevideo/RailroadCrossing OK (TemporalOperators.v ne doit pas etre compile)
Nancy/FOUnify OK
Nijmegen OK
Paris/ZF OK
Sophia-Antipolis/HARDWARE OK
Sophia-Antipolis/Cours-de-Coq OK
Sophia-Antipolis/MATHS/GEOMETRY
File "./part3.v", line 78, characters 0-5
Error: Attempt to save an incomplete proof
--> Changement de sémantique de Intuition
Sophia-Antipolis/condom ... vide
Sophia-Antipolis/param_pi
File "./fresh.v", line 173, characters 0-20
Error: Too few occurences
Suresnes/BDD OK
Utrecht/Ramsey OK
Utrecht/ABP OK
|
