.gitignore 6.04 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 15
*.cmt
*.cmti
16
*.annot
Andrei Paskevich's avatar
Andrei Paskevich committed
17
*.dep
18 19 20
*.vo
*.vd
*.glob
21
.*.aux
22
*.elc
MARCHE Claude's avatar
MARCHE Claude committed
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
MARCHE Claude's avatar
MARCHE Claude committed
39 40
/why3regtests.err
/why3regtests.out
Andrei Paskevich's avatar
Andrei Paskevich committed
41
/.merlin
Francois Bobot's avatar
Francois Bobot committed
42

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

Francois Bobot's avatar
Francois Bobot committed
56
# /bin/
57 58 59 60 61 62 63 64 65
/bin/why3.byte
/bin/why3.opt
/bin/why3
/bin/why3ide.byte
/bin/why3ide.opt
/bin/why3ide
/bin/why3config.byte
/bin/why3config.opt
/bin/why3config
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/why3replay.byte
/bin/why3replay.opt
/bin/why3replay
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
# /lib
126 127 128 129
/lib/why3cpulimit
/lib/why3cpulimit.exe
/lib/why3server
/lib/why3server.exe
130 131 132

# /lib/why3/
/lib/why3/META
133 134

# /lib/ocaml/
135
/lib/ocaml/why3__BigInt_compat.ml
136

Francois Bobot's avatar
Francois Bobot committed
137 138
# /share/
/share/emacs/semantic.cache
139
/share/Makefile.config
140 141 142
/share/drivers
/share/modules
/share/theories
Francois Bobot's avatar
Francois Bobot committed
143 144

# /src/
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
145
/src/config.sh
Francois Bobot's avatar
Francois Bobot committed
146

147
# Coq tactic
148
/src/coq-tactic/why3tac.ml
Francois Bobot's avatar
Francois Bobot committed
149

MARCHE Claude's avatar
MARCHE Claude committed
150 151
# Coq

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
152 153
# PVS
.pvscontext
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
154
orphaned-proofs.prf
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
155 156 157
/lib/pvs/*/*.summary
pvsbin/

158
# Isabelle
MARCHE Claude's avatar
MARCHE Claude committed
159
/lib/isabelle/bool/
160
/lib/isabelle/int/
MARCHE Claude's avatar
MARCHE Claude committed
161
/lib/isabelle/number/
162 163
/lib/isabelle/list/
/lib/isabelle/map/
164
/lib/isabelle/real/
165
/lib/isabelle/set/
Stefan Berghofer's avatar
Stefan Berghofer committed
166
/lib/isabelle/ROOT
Stefan Berghofer's avatar
Stefan Berghofer committed
167
/lib/isabelle/Why3_BV.thy
168
/lib/isabelle/Why3_Number.thy
Stefan Berghofer's avatar
Stefan Berghofer committed
169
/lib/isabelle/Why3_Real.thy
170
/lib/isabelle/Why3_Set.thy
171
/lib/isabelle/why3.ML
MARCHE Claude's avatar
MARCHE Claude committed
172
/lib/isabelle/last_build
173
/lib/isabelle/bv
174

Francois Bobot's avatar
Francois Bobot committed
175 176 177 178
# /src/driver/
/src/driver/driver_lexer.ml
/src/driver/driver_parser.ml
/src/driver/driver_parser.mli
179
/src/driver/driver_parser.conflicts
180 181 182
/src/driver/parse_smtv2_model_lexer.ml
/src/driver/parse_smtv2_model_parser.ml
/src/driver/parse_smtv2_model_parser.mli
Francois Bobot's avatar
Francois Bobot committed
183 184 185 186 187

# /src/parser/
/src/parser/lexer.ml
/src/parser/parser.ml
/src/parser/parser.mli
188
/src/parser/parser.conflicts
Francois Bobot's avatar
Francois Bobot committed
189

190
# /src/why3doc/
191
/src/why3doc/doc_lexer.ml
192

Francois Bobot's avatar
Francois Bobot committed
193
# /src/util/
194
/src/util/config.ml
195
/src/util/lexlib.ml
Francois Bobot's avatar
Francois Bobot committed
196
/src/util/rc.ml
197 198
/src/util/json_parser.mli
/src/util/json_parser.ml
Francois Bobot's avatar
Francois Bobot committed
199

200 201
# /src/session
/src/session/xml.ml
202
/src/session/compress.ml
203
/src/session/strategy_parser.ml
204

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
205 206 207
# /src/tools
/src/tools/why3wc.ml

Andrei Paskevich's avatar
Andrei Paskevich committed
208 209 210 211
# /plugins/tptp/
/plugins/tptp/tptp_lexer.ml
/plugins/tptp/tptp_parser.ml
/plugins/tptp/tptp_parser.mli
212
/plugins/tptp/tptp_parser.conflicts
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
213
/plugins/parser/dimacs.ml
Andrei Paskevich's avatar
Andrei Paskevich committed
214

215 216 217 218 219
# /plugins/python/
/plugins/python/py_lexer.ml
/plugins/python/py_parser.ml
/plugins/python/py_parser.mli
/plugins/python/test/
220
/plugins/python/py_parser.conflicts
221

222 223
# /drivers
/drivers/coq-realizations.aux
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
224
/drivers/pvs-realizations.aux
225
/drivers/isabelle-realizations.aux
226

Francois Bobot's avatar
Francois Bobot committed
227
# /tests/
228
/tests/test-jcf/
229
/tests/test-pgm-jcf/
MARCHE Claude's avatar
MARCHE Claude committed
230
/tests/test-claude/
231
/tests/test-and/
232 233
/tests/test-extraction/*
!/tests/test-extraction/main.ml
234 235
/tests/python/*/why3session.xml
/tests/python/*/why3shapes.gz
MARCHE Claude's avatar
MARCHE Claude committed
236 237

# /examples/
Andrei Paskevich's avatar
Andrei Paskevich committed
238 239 240 241 242
/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/
243 244 245 246
/examples/in_progress/prover/bench/*/*.out
/examples/in_progress/prover/bench/*/*.txt
/examples/in_progress/prover/bench1
/examples/in_progress/prover/bench2
MARCHE Claude's avatar
MARCHE Claude committed
247
/examples/why3bench.html
MARCHE Claude's avatar
MARCHE Claude committed
248 249
/examples/why3regtests.err
/examples/why3regtests.out
MARCHE Claude's avatar
MARCHE Claude committed
250
/examples/*/*.opt
251
/examples/*/*.byte
252 253
/examples/in_progress/*/*.opt
/examples/in_progress/*/*.byte
MARCHE Claude's avatar
MARCHE Claude committed
254
/examples/*.html
MARCHE Claude's avatar
MARCHE Claude committed
255
/examples/*/*.html
256
!/examples/*/index.html
MARCHE Claude's avatar
MARCHE Claude committed
257
/examples/*/*/*.html
258
!/examples/*/*/index.html
MARCHE Claude's avatar
MARCHE Claude committed
259
/examples/*/*/*/*.html
260
!/examples/*/*/*/index.html
MARCHE Claude's avatar
MARCHE Claude committed
261
/examples/style.css
262 263 264
/examples/*/style.css
/examples/*/*/style.css
/examples/*/*/*/style.css
265 266 267
/examples/*/*.tex
/examples/*/*/*.tex
/examples/*/*/*/*.tex
Andrei Paskevich's avatar
Andrei Paskevich committed
268 269
/examples/use_api/runstrat/makejob.opt
/examples/use_api/runstrat/runstrat.opt
270
/examples/vstte10_max_sum/*__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
271 272
/examples/euler001/*__*.ml
/examples/sudoku/*__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
273
/examples/sudoku/jsmain.js
MARCHE Claude's avatar
MARCHE Claude committed
274 275
/examples/in_progress/sudoku_reloaded/*__*.ml
/examples/in_progress/sudoku_reloaded/jsmain.js
MARCHE Claude's avatar
MARCHE Claude committed
276 277
/examples/gcd/*__*.ml
/examples/gcd/jsmain.js
MARCHE Claude's avatar
MARCHE Claude committed
278
/examples/defunctionalization/*__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
279 280 281 282
/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
283 284
/examples/in_progress/mp/jsmain.js
/examples/in_progress/mp/*__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
285 286
/examples/in_progress/prover/build/*__*.ml
/examples/in_progress/prover/.depend
287
/examples/in_progress/prover/build/prover
288

289
# modules
290
/modules/string/
291
/modules/stack/
292
/modules/queue/
293
/modules/pqueue/
294 295
/modules/mach/array/
/modules/mach/int/
296
/modules/python/
297

298 299
# Try Why3
/src/trywhy3/trywhy3.byte
300
/src/trywhy3/trywhy3.js
301
/src/trywhy3/trywhy3.map
302 303
/src/trywhy3/alt_ergo_worker.byte
/src/trywhy3/alt_ergo_worker.js
304
/src/trywhy3/alt_ergo_worker.map
305 306
/src/trywhy3/why3_worker.byte
/src/trywhy3/why3_worker.js
307
/src/trywhy3/why3_worker.map
MARCHE Claude's avatar
MARCHE Claude committed
308 309
/src/trywhy3/index.en.html
/src/trywhy3/index.fr.html
310
/src/trywhy3/index.html
311
/src/trywhy3/ace-builds/
312
/src/trywhy3/*.png
313
/src/trywhy3/alt-ergo*
314
/src/trywhy3/fontawesome/
MARCHE Claude's avatar
MARCHE Claude committed
315

316 317 318 319
# IDE
/src/ide/fontawesome
/src/ide/ace-builds

MARCHE Claude's avatar
MARCHE Claude committed
320 321
# jessie3
/src/jessie/config.log
MARCHE Claude's avatar
MARCHE Claude committed
322
/src/jessie/Makefile
MARCHE Claude's avatar
MARCHE Claude committed
323
/src/jessie/literals.ml
MARCHE Claude's avatar
MARCHE Claude committed
324
/src/jessie/tests/ptests_config
MARCHE Claude's avatar
MARCHE Claude committed
325
/src/jessie/tests/basic/result/*.log
326
/src/jessie/tests/demo/result/*.log
MARCHE Claude's avatar
MARCHE Claude committed
327

328
/trash
329
trywhy3.tar.gz