.gitignore 6.69 KB
Newer Older
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
1

2
*.tmp
Claude Marche's avatar
Claude Marche committed
3
*~
4
*.bak
Francois Bobot's avatar
Francois Bobot committed
5
*.o
6
*.a
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre 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 15
*.cmt
*.cmti
16
*.annot
17
*.dep
18 19 20
*.vo
*.vd
*.glob
21
.*.aux
22
*.elc
23
*.summary
François Bobot's avatar
François Bobot committed
24
\#*\#
25

Francois Bobot's avatar
Francois Bobot committed
26 27 28 29 30 31
# /
/config.status
/config.log
/autom4te.cache
/Makefile
/configure
32
/install-sh
Francois Bobot's avatar
Francois Bobot committed
33 34 35 36 37
/semantic.cache
/TAGS
/output_why3
/output_coq
/dep.pdf
MARCHE Claude's avatar
MARCHE Claude committed
38
/distrib
39 40
/why3regtests.err
/why3regtests.out
Andrei Paskevich's avatar
Andrei Paskevich committed
41
/.merlin
Guillaume Melquiond's avatar
Guillaume Melquiond committed
42
/src/jessie/.merlin
Francois Bobot's avatar
Francois Bobot committed
43

44 45 46 47 48 49 50 51
# /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/
52 53 54
/bench/programs/good/loops/
/bench/programs/good/po/
/bench/valid/list/
55
/bench/ce/*.out
56
/bench/parsing/bad/*.out
57

Francois Bobot's avatar
Francois Bobot committed
58
# /bin/
59 60 61 62 63 64 65 66 67
/bin/why3.byte
/bin/why3.opt
/bin/why3
/bin/why3ide.byte
/bin/why3ide.opt
/bin/why3ide
/bin/why3config.byte
/bin/why3config.opt
/bin/why3config
68 69
/bin/why3doc.byte
/bin/why3doc.opt
70
/bin/why3doc
71 72 73
/bin/why3extract.byte
/bin/why3extract.opt
/bin/why3extract
74 75 76
/bin/why3execute.byte
/bin/why3execute.opt
/bin/why3execute
77 78 79
/bin/why3prove.byte
/bin/why3prove.opt
/bin/why3prove
80 81 82
/bin/why3realize.byte
/bin/why3realize.opt
/bin/why3realize
83 84 85
/bin/why3replay.byte
/bin/why3replay.opt
/bin/why3replay
86
/bin/why3session.opt
87
/bin/why3session.byte
88
/bin/why3session
MARCHE Claude's avatar
MARCHE Claude committed
89 90 91
/bin/why3shell.opt
/bin/why3shell.byte
/bin/why3shell
92 93 94
/bin/why3wc.opt
/bin/why3wc.byte
/bin/why3wc
95 96 97
/bin/why3webserver.opt
/bin/why3webserver.byte
/bin/why3webserver
98 99 100
/bin/isabelle_client.opt
/bin/isabelle_client.byte
/bin/isabelle_client
Francois Bobot's avatar
Francois Bobot committed
101 102 103

# /doc/
/doc/version.tex
104
/doc/ocamldoc.sty
Francois Bobot's avatar
Francois Bobot committed
105 106 107 108
/doc/*whizzy*
/doc/manual.wdvi
/doc/manual.raux
/doc/manual.log
109
/doc/manual.lof
Francois Bobot's avatar
Francois Bobot committed
110 111 112 113 114 115 116
/doc/manual.toc
/doc/manual.aux
/doc/manual.bbl
/doc/manual.blg
/doc/manual.ind
/doc/manual.ilg
/doc/manual.idx
117
/doc/manual.rel
MARCHE Claude's avatar
MARCHE Claude committed
118 119 120 121
/doc/manual.glg
/doc/manual.glo
/doc/manual.gls
/doc/manual.ist
122
/doc/manual.out
MARCHE Claude's avatar
MARCHE Claude committed
123
/doc/manual.image.out
Leon Gondelman's avatar
Leon Gondelman committed
124
/doc/manual.synctex.gz
Francois Bobot's avatar
Francois Bobot committed
125 126
/doc/*.haux
/doc/*.pdf
127
/doc/generated/
128
/doc/html/
Francois Bobot's avatar
Francois Bobot committed
129 130
/doc/*.hind
/doc/*.htoc
MARCHE Claude's avatar
MARCHE Claude committed
131 132
/doc/bnf
/doc/bnf.ml
133
/doc/apidoc.tex
MARCHE Claude's avatar
MARCHE Claude committed
134
/doc/apidoc/
MARCHE Claude's avatar
MARCHE Claude committed
135
/doc/stdlibdoc/
Leon Gondelman's avatar
Leon Gondelman committed
136
/doc/texput.log
137
/doc/extract_ocaml_code
138 139
/doc/*__*.ml
/doc/*_bnf.tex
Francois Bobot's avatar
Francois Bobot committed
140

141
# /lib
Andrei Paskevich's avatar
Andrei Paskevich committed
142 143
/lib/why3-cpulimit
/lib/why3-cpulimit.exe
144 145 146 147
/lib/why3cpulimit
/lib/why3cpulimit.exe
/lib/why3server
/lib/why3server.exe
148 149 150

# /lib/why3/
/lib/why3/META
151

Francois Bobot's avatar
Francois Bobot committed
152 153
# /share/
/share/emacs/semantic.cache
154
/share/Makefile.config
155
/share/drivers
156
/share/stdlib
Francois Bobot's avatar
Francois Bobot committed
157 158

# /src/
Andrei Paskevich's avatar
Andrei Paskevich committed
159
/src/config.sh
Francois Bobot's avatar
Francois Bobot committed
160

161
# Coq
162
/lib/coq/version
163

Jean-Christophe's avatar
Jean-Christophe committed
164 165
# PVS
.pvscontext
Jean-Christophe's avatar
Jean-Christophe committed
166
orphaned-proofs.prf
167
/lib/pvs/version
Jean-Christophe's avatar
Jean-Christophe committed
168 169 170
/lib/pvs/*/*.summary
pvsbin/

171
# Isabelle
MARCHE Claude's avatar
MARCHE Claude committed
172
/lib/isabelle/bool/
173
/lib/isabelle/int/
MARCHE Claude's avatar
MARCHE Claude committed
174
/lib/isabelle/number/
175 176
/lib/isabelle/list/
/lib/isabelle/map/
177
/lib/isabelle/real/
178
/lib/isabelle/set/
179
/lib/isabelle/Why3_Number.thy
180
/lib/isabelle/Why3_Real.thy
181
/lib/isabelle/why3.ML
182
/lib/isabelle/last_build
183
/lib/isabelle/bv
184

Francois Bobot's avatar
Francois Bobot committed
185 186 187 188
# /src/driver/
/src/driver/driver_lexer.ml
/src/driver/driver_parser.ml
/src/driver/driver_parser.mli
189
/src/driver/driver_parser.conflicts
190 191 192
/src/driver/parse_smtv2_model_lexer.ml
/src/driver/parse_smtv2_model_parser.ml
/src/driver/parse_smtv2_model_parser.mli
193
/src/driver/parse_smtv2_model_parser.conflicts
Francois Bobot's avatar
Francois Bobot committed
194 195 196 197 198

# /src/parser/
/src/parser/lexer.ml
/src/parser/parser.ml
/src/parser/parser.mli
199
/src/parser/parser.conflicts
200 201
/src/parser/handcrafted.messages.temp
/src/parser/parser_messages.ml
Francois Bobot's avatar
Francois Bobot committed
202

203
# /src/why3doc/
204
/src/why3doc/doc_lexer.ml
205

Francois Bobot's avatar
Francois Bobot committed
206
# /src/util/
207
/src/util/config.ml
208
/src/util/lexlib.ml
Francois Bobot's avatar
Francois Bobot committed
209
/src/util/rc.ml
210
/src/util/json_lexer.ml
211 212
/src/util/json_parser.mli
/src/util/json_parser.ml
213
/src/util/json_parser.conflicts
214 215
/src/util/mlmpfr_wrapper.ml
/src/util/ppx_debug_optim
Francois Bobot's avatar
Francois Bobot committed
216

217 218
# /src/session
/src/session/xml.ml
219
/src/session/compress.ml
220
/src/session/strategy_parser.ml
221

222 223 224
# /src/tools
/src/tools/why3wc.ml

225
# /src/ide
226
/src/ide/gtkcompat.ml
227 228 229
/src/ide/why3_js.byte
/src/ide/why3_js.js

Andrei Paskevich's avatar
Andrei Paskevich committed
230 231 232 233
# /plugins/tptp/
/plugins/tptp/tptp_lexer.ml
/plugins/tptp/tptp_parser.ml
/plugins/tptp/tptp_parser.mli
234
/plugins/tptp/tptp_parser.conflicts
235
/plugins/parser/dimacs.ml
Andrei Paskevich's avatar
Andrei Paskevich committed
236

237 238 239 240 241
# /plugins/python/
/plugins/python/py_lexer.ml
/plugins/python/py_parser.ml
/plugins/python/py_parser.mli
/plugins/python/test/
242
/plugins/python/py_parser.conflicts
243

244 245 246 247 248 249 250
# /plugins/microc/
/plugins/microc/mc_lexer.ml
/plugins/microc/mc_parser.ml
/plugins/microc/mc_parser.mli
/plugins/microc/test/
/plugins/microc/mc_parser.conflicts

251 252
# /drivers
/drivers/coq-realizations.aux
Jean-Christophe's avatar
Jean-Christophe committed
253
/drivers/pvs-realizations.aux
254
/drivers/isabelle-realizations.aux
255

Francois Bobot's avatar
Francois Bobot committed
256
# /tests/
257
/tests/test-jcf/
258
/tests/test-pgm-jcf/
259
/tests/test-claude/
260
/tests/test-and/
261 262
/tests/test-extraction/*
!/tests/test-extraction/main.ml
263 264
/tests/python/*/why3session.xml
/tests/python/*/why3shapes.gz
265 266
/tests/microc/*/why3session.xml
/tests/microc/*/why3shapes.gz
267 268

# /examples/
Andrei Paskevich's avatar
Andrei Paskevich committed
269 270 271 272 273
/examples/in_progress/course/
/examples/in_progress/wcet_hull/
/examples/in_progress/binary_search2/
/examples/in_progress/binary_search_c/
/examples/in_progress/vacid_0_red_black_trees_harness/
274
/examples/why3bench.html
MARCHE Claude's avatar
MARCHE Claude committed
275 276
/examples/why3regtests.err
/examples/why3regtests.out
277
/examples/*/*.opt
278
/examples/*/*.byte
279 280
/examples/in_progress/*/*.opt
/examples/in_progress/*/*.byte
MARCHE Claude's avatar
MARCHE Claude committed
281
/examples/*.html
282
/examples/*/*.html
283
!/examples/*/index.html
284
/examples/*/*/*.html
285
!/examples/*/*/index.html
286
/examples/*/*/*/*.html
287
!/examples/*/*/*/index.html
MARCHE Claude's avatar
MARCHE Claude committed
288
/examples/style.css
289 290 291
/examples/*/style.css
/examples/*/*/style.css
/examples/*/*/*/style.css
292 293 294
/examples/*/*.tex
/examples/*/*/*.tex
/examples/*/*/*/*.tex
Andrei Paskevich's avatar
Andrei Paskevich committed
295 296
/examples/use_api/runstrat/makejob.opt
/examples/use_api/runstrat/runstrat.opt
297 298 299
/examples/vstte10_max_sum/vstte10_max_sum.ml
/examples/euler001/euler001.ml
/examples/sudoku/sudoku.ml
MARCHE Claude's avatar
MARCHE Claude committed
300
/examples/sudoku/jsmain.js
MARCHE Claude's avatar
MARCHE Claude committed
301 302
/examples/in_progress/sudoku_reloaded/*__*.ml
/examples/in_progress/sudoku_reloaded/jsmain.js
303
/examples/gcd/euclideanAlgorithm63.ml
MARCHE Claude's avatar
MARCHE Claude committed
304
/examples/gcd/jsmain.js
305
/examples/defunctionalization/defunctionalization.ml
MARCHE Claude's avatar
MARCHE Claude committed
306
/examples/vstte12_combinators/jsmain.js
307
/examples/vstte12_combinators/vstte12_combinators.ml
MARCHE Claude's avatar
MARCHE Claude committed
308 309
/examples/in_progress/bigInt/jsmain.js
/examples/in_progress/bigInt/*__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
310 311
/examples/in_progress/mp/jsmain.js
/examples/in_progress/mp/*__*.ml
312
/examples/prover/.depend
313 314
/examples/prover/prover
/examples/prover/prover.ml
315 316 317 318
/examples/prover/bench/*/*.out
/examples/prover/bench/*/*.txt
/examples/prover/bench1
/examples/prover/bench2
MARCHE Claude's avatar
MARCHE Claude committed
319 320
/examples/prover/macro_generator/depend
/examples/prover/macro_generator/build
321

322 323
# Try Why3
/src/trywhy3/trywhy3.byte
324
/src/trywhy3/trywhy3.js
325
/src/trywhy3/trywhy3.map
326 327
/src/trywhy3/alt_ergo_worker.byte
/src/trywhy3/alt_ergo_worker.js
328
/src/trywhy3/alt_ergo_worker.map
329 330
/src/trywhy3/why3_worker.byte
/src/trywhy3/why3_worker.js
331
/src/trywhy3/why3_worker.map
332 333
/src/trywhy3/index.en.html
/src/trywhy3/index.fr.html
334
/src/trywhy3/index.html
335
/src/trywhy3/ace-builds/
336
/src/trywhy3/*.png
337
/src/trywhy3/alt-ergo*
338
/src/trywhy3/fontawesome/
MARCHE Claude's avatar
MARCHE Claude committed
339

340 341 342 343
# IDE
/src/ide/fontawesome
/src/ide/ace-builds

344 345
# jessie3
/src/jessie/config.log
MARCHE Claude's avatar
MARCHE Claude committed
346
/src/jessie/Makefile
MARCHE Claude's avatar
MARCHE Claude committed
347
/src/jessie/literals.ml
348
/src/jessie/tests/ptests_config
MARCHE Claude's avatar
MARCHE Claude committed
349
/src/jessie/tests/basic/result/*.log
350
/src/jessie/tests/demo/result/*.log
351

352
/trash
353
trywhy3.tar.gz