aboutsummaryrefslogtreecommitdiffhomepage
path: root/PROBLEMES
blob: a1042192835dcea2f0e6b07ac9ce325cf76b1c4c (plain)
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
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