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
149
150
151
152
153
154
155
156
157
158
159
|
- Problème affichage de Cases (alpha-conversion dans les patterns)
======================================================================
Inductive t : Set := c : nat->nat->t.
Definition foo' := [x:t]Cases x of (c y z) => (plus y z) end.
Print foo'.
======================================================================
Des CASTEDCOMMAND s'affiche dans les scripts de preuves.
Probleme d'affichage des scripts de preuve (disparition des THEN)
Compute affiche Cbv Beta Iota
Variable + Record => clash. Exemple:
======================================================================
Section S.
Variable F:Set.
Record R [ F:Set; x:F ] : Set := { c : x=x }.
=> Error: new_isevar_sign: two vars have the same name
======================================================================
Hints Resolve fait une anomalie si la constante n'existe pas
--> CORRIGÉ
(* Probleme de lancement de coqtop lorsque le fichier n'est pas sauve
sous emacs et qu'un lien (lock ?) .#fichier a ete cree *)
/home/cpaulin/coq/V7/bin/coqc -q -I . Axioms
Anomaly: Uncaught exception Unix.Unix_error(20, "stat", "/home/cpaulin/coq/V7/theories/Num/.#Axioms.v").
Please report.
make: *** [Axioms.vo] Error 1
--> CORRIGÉ (message explicatif et n'échoue plus)
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
---> N'était-ce pas quand elle était précédée d'un symbole, style ~<A>x=y ??
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/Additions : échec sur Realizer
Bordeaux/SearchTrees : échec sur Realizer
Bordeaux/TREES : échec 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.
Lannion : échec sur Realizer
Lyon/AUTOMATA : OK
Lyon/CIRCUITS : OK
Lyon/COINDUCTIVES : OK
Lyon/IEEE754 : OK
Rocq/MUTUAL-EXCLUSION : échec sur Realizer
Rocq/ALGEBRA/SETOIDS
File "CATEGORY_THEORY/CATEGORY/ONE.v", line 83, characters 0-61
Error: There is an unknown subterm I cannot solve
Rocq/ARITH/Chinese
File "./Zdiv.v", line 34, characters 0-944
--> Un Refine mal typé et des 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/DEMOS OK
Rocq/GRAPHS OK
Rocq/LAMBDA OK
Rocq/SHUFFLE OK
Rocq/THREE_GAP OK
Rocq/ZF OK
Rocq/PARADOXES OK
Rocq/CHECKER OK
Rocq/COMPILER OK
Rocq/HIGMAN 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: Un Rewrite ou Unfold en a trop ou pas assez fait (union.v)
Rocq/RATIONAL
--> Des fichiers ML à porter
Lyon/AUTOMATA OK
Lyon/CIRCUITS OK
Lyon/COINDUCTIVES OK
Lyon/IEEE754 (passait dans la V7.0beta !!)
File "./IEEE754_def.v", line 427, characters 0-1194
Error: Some clauses are redondant
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)
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
|
