.gitignore 4.52 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
6
*.a
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
7
why3.conf
8 9 10
*.cmx
*.cmo
*.cmi
François Bobot's avatar
François Bobot committed
11
*.cmxs
12 13
*.cma
*.cmxa
14
*.annot
Andrei Paskevich's avatar
Andrei Paskevich committed
15
*.dep
16 17 18
*.vo
*.vd
*.glob
19
*.elc
François Bobot's avatar
François Bobot committed
20
\#*\#
21

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

38 39 40 41 42 43 44 45
# /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/
46 47 48
/bench/programs/good/loops/
/bench/programs/good/po/
/bench/valid/list/
49

Francois Bobot's avatar
Francois Bobot committed
50
# /bin/
51 52 53
/bin/why3.byte
/bin/why3.opt
/bin/why3
54 55 56
/bin/why3contraption.byte
/bin/why3contraption.opt
/bin/why3contraption
57 58 59 60 61 62 63 64 65
/bin/why3ide.byte
/bin/why3ide.opt
/bin/why3ide
/bin/why3config.byte
/bin/why3config.opt
/bin/why3config
/bin/why3bench.byte
/bin/why3bench.opt
/bin/why3bench
66 67
/bin/why3doc.byte
/bin/why3doc.opt
68
/bin/why3doc
69 70 71
/bin/why3extract.byte
/bin/why3extract.opt
/bin/why3extract
72 73 74
/bin/why3execute.byte
/bin/why3execute.opt
/bin/why3execute
75 76 77
/bin/why3prove.byte
/bin/why3prove.opt
/bin/why3prove
78 79 80
/bin/why3realize.byte
/bin/why3realize.opt
/bin/why3realize
81 82 83
/bin/why3replayer.byte
/bin/why3replayer.opt
/bin/why3replayer
84
/bin/why3session.opt
85
/bin/why3session.byte
86
/bin/why3session
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
87 88 89
/bin/why3wc.opt
/bin/why3wc.byte
/bin/why3wc
Francois Bobot's avatar
Francois Bobot committed
90 91 92

# /doc/
/doc/version.tex
MARCHE Claude's avatar
MARCHE Claude committed
93
/doc/ocamldoc.sty
Francois Bobot's avatar
Francois Bobot committed
94 95 96 97
/doc/*whizzy*
/doc/manual.wdvi
/doc/manual.raux
/doc/manual.log
98
/doc/manual.lof
Francois Bobot's avatar
Francois Bobot committed
99 100 101 102 103 104 105
/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
106
/doc/manual.rel
MARCHE Claude's avatar
MARCHE Claude committed
107 108 109 110
/doc/manual.glg
/doc/manual.glo
/doc/manual.gls
/doc/manual.ist
111
/doc/manual.out
MARCHE Claude's avatar
MARCHE Claude committed
112
/doc/manual.image.out
Francois Bobot's avatar
Francois Bobot committed
113 114
/doc/*.haux
/doc/*.pdf
115
/doc/html/
Francois Bobot's avatar
Francois Bobot committed
116 117
/doc/*.hind
/doc/*.htoc
MARCHE Claude's avatar
MARCHE Claude committed
118 119 120
/doc/bnf
/doc/bnf.ml
/doc/*_bnf.tex
121
/doc/apidoc.tex
MARCHE Claude's avatar
MARCHE Claude committed
122
/doc/apidoc/
MARCHE Claude's avatar
MARCHE Claude committed
123
/doc/stdlibdoc/
Francois Bobot's avatar
Francois Bobot committed
124

125 126 127 128 129 130
# /lib
/lib/why3-cpulimit
/lib/why3-cpulimit.exe

# /lib/why3/
/lib/why3/META
131 132

# /lib/ocaml/
133
/lib/ocaml/why3__BigInt_compat.ml
134

Francois Bobot's avatar
Francois Bobot committed
135 136
# /share/
/share/emacs/semantic.cache
137
/share/Makefile.config
Francois Bobot's avatar
Francois Bobot committed
138 139

# /src/
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
140
/src/config.sh
Francois Bobot's avatar
Francois Bobot committed
141

142
# Coq tactic
143
/src/coq-tactic/coqCompat.ml
144 145
/src/coq-tactic/g_why3tac.ml
/src/coq-tactic/.why3-vo-*
Francois Bobot's avatar
Francois Bobot committed
146

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
147 148
# PVS
.pvscontext
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
149
orphaned-proofs.prf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
150 151 152
/lib/pvs/*/*.summary
pvsbin/

153
# Isabelle
MARCHE Claude's avatar
MARCHE Claude committed
154
/lib/isabelle/bool/
155
/lib/isabelle/int/
MARCHE Claude's avatar
MARCHE Claude committed
156
/lib/isabelle/number/
157 158 159
/lib/isabelle/list/
/lib/isabelle/map/
/lib/isabelle/set/
160

Francois Bobot's avatar
Francois Bobot committed
161 162 163 164
# /src/driver/
/src/driver/driver_lexer.ml
/src/driver/driver_parser.ml
/src/driver/driver_parser.mli
165
/src/driver/driver_parser.output
Francois Bobot's avatar
Francois Bobot committed
166 167 168 169 170

# /src/parser/
/src/parser/lexer.ml
/src/parser/parser.ml
/src/parser/parser.mli
171
/src/parser/parser.output
Francois Bobot's avatar
Francois Bobot committed
172

173
# /src/why3doc/
174
/src/why3doc/doc_lexer.ml
175

Francois Bobot's avatar
Francois Bobot committed
176
# /src/util/
177
/src/util/config.ml
Francois Bobot's avatar
Francois Bobot committed
178 179
/src/util/rc.ml

180 181 182
# /src/session
/src/session/xml.ml

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
183 184 185
# /src/tools
/src/tools/why3wc.ml

Andrei Paskevich's avatar
Andrei Paskevich committed
186 187 188 189 190
# /plugins/tptp/
/plugins/tptp/tptp_lexer.ml
/plugins/tptp/tptp_parser.ml
/plugins/tptp/tptp_parser.mli
/plugins/tptp/tptp_parser.output
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
191
/plugins/parser/dimacs.ml
Andrei Paskevich's avatar
Andrei Paskevich committed
192

193 194
# /drivers
/drivers/coq-realizations.aux
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
195
/drivers/pvs-realizations.aux
196
/drivers/isabelle-realizations.aux
197

Francois Bobot's avatar
Francois Bobot committed
198
# /tests/
199
/tests/test-jcf/
200
/tests/test-pgm-jcf/
MARCHE Claude's avatar
MARCHE Claude committed
201
/tests/test-claude/
202
/tests/test-and/
203 204
/tests/test-extraction/*
!/tests/test-extraction/main.ml
MARCHE Claude's avatar
MARCHE Claude committed
205 206

# /examples/
Andrei Paskevich's avatar
Andrei Paskevich committed
207 208 209 210 211 212
/examples/in_progress/course/
/examples/in_progress/wcet_hull/
/examples/in_progress/binary_search2/
/examples/in_progress/binary_search_c/
/examples/in_progress/next_digit_sum/
/examples/in_progress/vacid_0_red_black_trees_harness/
MARCHE Claude's avatar
MARCHE Claude committed
213
/examples/why3bench.html
MARCHE Claude's avatar
MARCHE Claude committed
214 215
/examples/why3regtests.err
/examples/why3regtests.out
MARCHE Claude's avatar
MARCHE Claude committed
216
/examples/*/*.opt
217
/examples/*/*.byte
218 219
/examples/in_progress/*/*.opt
/examples/in_progress/*/*.byte
MARCHE Claude's avatar
MARCHE Claude committed
220 221 222
/examples/*/*.html
/examples/*/*/*.html
/examples/*/*/*/*.html
223 224 225
/examples/*/style.css
/examples/*/*/style.css
/examples/*/*/*/style.css
226 227 228
/examples/*/*.tex
/examples/*/*/*.tex
/examples/*/*/*/*.tex
Andrei Paskevich's avatar
Andrei Paskevich committed
229 230
/examples/use_api/runstrat/makejob.opt
/examples/use_api/runstrat/runstrat.opt
231
/examples/vstte10_max_sum/*__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
232 233 234
/examples/euler001/*__*.ml
/examples/sudoku/*__*.ml
/examples/defunctionalization/*__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
235 236 237 238
/examples/vstte12_combinators/jsmain.js
/examples/vstte12_combinators/*__*.ml
/examples/in_progress/bigInt/jsmain.js
/examples/in_progress/bigInt/*__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
239 240
/examples/in_progress/mp/jsmain.js
/examples/in_progress/mp/*__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
241

242

243
# modules
244
/modules/string/
245
/modules/stack/
246
/modules/queue/
247
/modules/pqueue/
248 249
/modules/mach/array/
/modules/mach/int/
250

MARCHE Claude's avatar
MARCHE Claude committed
251

MARCHE Claude's avatar
MARCHE Claude committed
252 253 254 255 256 257
# jessie3
/src/jessie/.depend
/src/jessie/Jessie3_DEP
/src/jessie/autom4te.cache/
/src/jessie/config.log
/src/jessie/config.status
MARCHE Claude's avatar
MARCHE Claude committed
258
/src/jessie/Makefile
MARCHE Claude's avatar
MARCHE Claude committed
259
/src/jessie/literals.ml
MARCHE Claude's avatar
MARCHE Claude committed
260
/src/jessie/ptests_local_config.ml
MARCHE Claude's avatar
MARCHE Claude committed
261
/src/jessie/tests/basic/frama_c_journal.ml
MARCHE Claude's avatar
MARCHE Claude committed
262
/src/jessie/tests/basic/result/*.log
263
/src/jessie/tests/demo/result/*.log
264
/trash