.gitignore 3.37 KB
Newer Older
Jean-Christophe Filliâtre's avatar
ignore  
Jean-Christophe Filliâtre committed
1

2
*.tmp
Claude Marche's avatar
Claude Marche committed
3
*~
MARCHE Claude's avatar
MARCHE Claude committed
4
*.bak
Francois Bobot's avatar
Francois Bobot committed
5
*.o
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
6
why3.conf
7 8 9
*.cmx
*.cmo
*.cmi
François Bobot's avatar
François Bobot committed
10
*.cmxs
11
*.annot
Andrei Paskevich's avatar
Andrei Paskevich committed
12
*.dep
13 14 15
*.vo
*.vd
*.glob
François Bobot's avatar
François Bobot committed
16
\#*\#
17

Francois Bobot's avatar
Francois Bobot committed
18 19 20 21 22 23 24 25 26 27 28
# /
/config.status
/config.log
/autom4te.cache
/Makefile
/configure
/semantic.cache
/TAGS
/output_why3
/output_coq
/dep.pdf
MARCHE Claude's avatar
MARCHE Claude committed
29
/distrib
MARCHE Claude's avatar
MARCHE Claude committed
30 31
/why3regtests.err
/why3regtests.out
MARCHE Claude's avatar
MARCHE Claude committed
32
/META
Francois Bobot's avatar
Francois Bobot committed
33

34 35 36 37 38
# /lib/why3/
/lib/why3/META
/lib/why3/why3.cm*
/lib/why3/why3.a
/lib/why3/why3.o
39

40 41 42 43 44 45 46 47
# /bench/
/bench/programs/good/booleans/
/bench/programs/good/exceptions/
/bench/programs/good/for/
/bench/programs/good/list/
/bench/programs/good/see/
/bench/programs/good/set/
/bench/programs/good/recfun/
48 49 50
/bench/programs/good/loops/
/bench/programs/good/po/
/bench/valid/list/
51

Francois Bobot's avatar
Francois Bobot committed
52
# /bin/
53 54 55 56 57 58
/bin/why3.byte
/bin/why3.opt
/bin/why3
/bin/why3ide.byte
/bin/why3ide.opt
/bin/why3ide
59
/bin/why3-cpulimit
60
/bin/why3-cpulimit.exe
61 62 63 64 65 66
/bin/why3config.byte
/bin/why3config.opt
/bin/why3config
/bin/why3bench.byte
/bin/why3bench.opt
/bin/why3bench
67 68
/bin/why3doc.byte
/bin/why3doc.opt
69
/bin/why3doc
70 71 72
/bin/why3replayer.byte
/bin/why3replayer.opt
/bin/why3replayer
73 74 75
/bin/why3html.byte
/bin/why3html.opt
/bin/why3html
76 77 78
/bin/why3stats.byte
/bin/why3stats.opt
/bin/why3stats
79
/bin/why3session.opt
80
/bin/why3session.byte
81
/bin/why3session
Francois Bobot's avatar
Francois Bobot committed
82 83 84

# /doc/
/doc/version.tex
MARCHE Claude's avatar
MARCHE Claude committed
85
/doc/ocamldoc.sty
Francois Bobot's avatar
Francois Bobot committed
86 87 88 89
/doc/*whizzy*
/doc/manual.wdvi
/doc/manual.raux
/doc/manual.log
90
/doc/manual.lof
Francois Bobot's avatar
Francois Bobot committed
91 92 93 94 95 96 97
/doc/manual.toc
/doc/manual.aux
/doc/manual.bbl
/doc/manual.blg
/doc/manual.ind
/doc/manual.ilg
/doc/manual.idx
MARCHE Claude's avatar
MARCHE Claude committed
98
/doc/manual.rel
MARCHE Claude's avatar
MARCHE Claude committed
99 100 101 102
/doc/manual.glg
/doc/manual.glo
/doc/manual.gls
/doc/manual.ist
103
/doc/manual.out
MARCHE Claude's avatar
MARCHE Claude committed
104
/doc/manual.image.out
Francois Bobot's avatar
Francois Bobot committed
105 106
/doc/*.haux
/doc/*.pdf
107
/doc/html/
Francois Bobot's avatar
Francois Bobot committed
108 109
/doc/*.hind
/doc/*.htoc
MARCHE Claude's avatar
MARCHE Claude committed
110 111 112
/doc/bnf
/doc/bnf.ml
/doc/*_bnf.tex
113
/doc/apidoc.tex
MARCHE Claude's avatar
MARCHE Claude committed
114
/doc/apidoc/
MARCHE Claude's avatar
MARCHE Claude committed
115
/doc/stdlibdoc/
Francois Bobot's avatar
Francois Bobot committed
116 117

# /share/
Jean-Christophe Filliâtre's avatar
ignore  
Jean-Christophe Filliâtre committed
118
/share/provers-detection-data.conf
Francois Bobot's avatar
Francois Bobot committed
119 120 121
/share/emacs/semantic.cache

# /src/
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
122
/src/config.sh
Francois Bobot's avatar
Francois Bobot committed
123

124
# Coq tactic
125
/src/coq-tactic/coqCompat.ml
126 127 128
/src/coq-tactic/g_why3tac.ml
/src/coq-tactic/.why3-vo-*
/lib/coq-tactic/why3tac.cma
Francois Bobot's avatar
Francois Bobot committed
129

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
130 131
# PVS
.pvscontext
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
132
orphaned-proofs.prf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
133 134 135
/lib/pvs/*/*.summary
pvsbin/

Francois Bobot's avatar
Francois Bobot committed
136 137 138 139
# /src/driver/
/src/driver/driver_lexer.ml
/src/driver/driver_parser.ml
/src/driver/driver_parser.mli
140
/src/driver/driver_parser.output
Francois Bobot's avatar
Francois Bobot committed
141 142 143 144 145

# /src/parser/
/src/parser/lexer.ml
/src/parser/parser.ml
/src/parser/parser.mli
146
/src/parser/parser.output
Francois Bobot's avatar
Francois Bobot committed
147

148
# /src/why3doc/
149
/src/why3doc/doc_lexer.ml
150

Francois Bobot's avatar
Francois Bobot committed
151
# /src/util/
152
/src/util/config.ml
Francois Bobot's avatar
Francois Bobot committed
153 154
/src/util/rc.ml

155 156 157
# /src/session
/src/session/xml.ml

Andrei Paskevich's avatar
Andrei Paskevich committed
158 159 160 161 162 163
# /plugins/tptp/
/plugins/tptp/tptp_lexer.ml
/plugins/tptp/tptp_parser.ml
/plugins/tptp/tptp_parser.mli
/plugins/tptp/tptp_parser.output

164 165
# /drivers
/drivers/coq-realizations.aux
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
166
/drivers/pvs-realizations.aux
167

Francois Bobot's avatar
Francois Bobot committed
168
# /tests/
169
/tests/test-jcf/
170
/tests/test-pgm-jcf/
MARCHE Claude's avatar
MARCHE Claude committed
171
/tests/test-claude/
172
/tests/test-and/
MARCHE Claude's avatar
MARCHE Claude committed
173 174

# /examples/
MARCHE Claude's avatar
MARCHE Claude committed
175
/examples/programs/course/
176
/examples/programs/wcet_hull/
177
/examples/programs/binary_search2/
Jean-Christophe Filliâtre's avatar
ignore  
Jean-Christophe Filliâtre committed
178
/examples/programs/vacid_0_red_black_trees_harness/
179
/examples/programs/next_digit_sum/
180
/examples/programs/binary_search_c/
MARCHE Claude's avatar
MARCHE Claude committed
181
/examples/why3bench.html
MARCHE Claude's avatar
MARCHE Claude committed
182 183
/examples/why3regtests.err
/examples/why3regtests.out
MARCHE Claude's avatar
MARCHE Claude committed
184 185 186
/examples/*/*.html
/examples/*/*/*.html
/examples/*/*/*/*.html
187 188 189
/examples/*/*.tex
/examples/*/*/*.tex
/examples/*/*/*/*.tex
Jean-Christophe Filliâtre's avatar
ignore  
Jean-Christophe Filliâtre committed
190 191
/examples/runstrat/makejob.opt
/examples/runstrat/runstrat.opt
192

193
# modules
194
/modules/string/
195
/modules/stack/
196
/modules/queue/
197
/modules/pqueue/
198

MARCHE Claude's avatar
MARCHE Claude committed
199 200 201 202 203 204 205
# jessie3
/src/jessie/.depend
/src/jessie/Jessie3.cma
/src/jessie/Jessie3_DEP
/src/jessie/autom4te.cache/
/src/jessie/config.log
/src/jessie/config.status
MARCHE Claude's avatar
MARCHE Claude committed
206
/src/jessie/Makefile
MARCHE Claude's avatar
MARCHE Claude committed
207
/src/jessie/literals.ml
MARCHE Claude's avatar
MARCHE Claude committed
208
/src/jessie/ptests_local_config.ml
MARCHE Claude's avatar
MARCHE Claude committed
209
/src/jessie/tests/basic/result/*.log