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
|
coqtop -byte
Anomaly: Uncaught exception Unix.Unix_error(20, "execv", "./coqtop.byte").
Please report.
portable-demons ~/coq/V7 > which \coqtop
/home/cpaulin/coq/V7/bin//coqtop
portable-demons ~/coq/V7 > \coqtop -byte
Anomaly: Uncaught exception Unix.Unix_error(20, "execv", "./coqtop.byte").
Please report.
portable-demons ~/coq/V7 > which coqtop.byte
/home/cpaulin/coq/V7/bin//coqtop.byte
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
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
Associativite Repeat Orelse changee
Repeat A Orelse B se lit (Repeat A) Orelse B
ce n'est pas malin car Repeat A n'echoue jamais
Probleme de Reset Initial.
Load Field.
Reset Initial.
Coq < Load Field.
Error while reading ./Field.v :
File "./Field.v", line 6, characters 0-83
Error: list already exists
(* l'erreur ne se produit pas sur un fichier plus court ..)
voir dans library states.ml
la fonction freeze=set_state qui modifie l'etat initial ....
les parentheses ne sont pas autorises autour de
motifs constants :
> Check [n:nat]Cases n of (O) => true | _ => false end.
Syntax error: 'as' or ',' or [ne_pattern_list] expected after [Constr.pattern] (in [compound_pattern])
CONTRIBS
---------
BellLabs/lazyPCF : OK
Bordeaux/TREES :
File "./ABR.v", line 131, characters 0-88
Anomaly: Unrecognizable ast node of vernac arg:
(COMMAND (PROP {Null})). Please report.
Derive Inversion_clear HAS_INV with
(n,p:nat)(t1,t2:bintree)(has (bin n t1 t2) p).
Bordeaux/Additions :
echecs sur Realizer
Bordeaux/GROUPS : OK
Dyade/Otway-Rees : OK
Dyade/BDD : Require Rocq/GRAPHS
Lyon/AUTOMATA : OK
Lyon/IEEE754 : OK
Lyon/COINDUCTIVES : OK
Rocq/GRAPHS
/home/cpaulin/TYPES/V7/bin/coqc -q -I . lsort
Warning: compute_metamap: MV(1506) sans type !
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
File "./Conv_Dec.v", line 68, characters 2-459
Error: Inference of annotation not yet implemented in this case
Rocq/ARITH/Chinese
File "./Zdiv.v", line 34, characters 0-944
Anomaly: Search error. Please report.
Refine
Rocq/PARADOXES
File "./BuraliForti.v", line 176, characters 0-26
Anomaly: Uncaught exception Univ.UniverseInconsistency. Please report.
A la fermeture de section, est-ce normal ? pourquoi une anomalie ?
Rocq/CHECKER OK
Rocq/COMPILER OK
Rocq/DEMOS OK
Rocq/HIGMAN OK
Rocq/LAMBDA OK
Rocq/SHUFFLE OK
Rocq/SCHROEDER
File "./Functions.v", line 95, characters 0-15
Error: Bad inductive definition.
A la fermeture de section
Rocq/SUBST
File "./TS.v", line 69, characters 0-6
Error: Attempt to save an incomplete proof
Rocq/DEMOS/Demo_AutoRewrite
Anomaly: Invalid argument "output_value: functional value".
Montevideo/CtlTctl OK
Montevideo/RailroadCrossing
File "./railroad_crossing.v", line 613, characters 2-20
Anomaly: useInversionLemma. Please report.
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.
|
