.gitignore 5.19 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
*.elc
MARCHE Claude's avatar
MARCHE Claude committed
22
*.summary
François Bobot's avatar
François Bobot committed
23
\#*\#
24

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

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

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

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

122 123 124 125 126 127
# /lib
/lib/why3-cpulimit
/lib/why3-cpulimit.exe

# /lib/why3/
/lib/why3/META
128 129

# /lib/ocaml/
130
/lib/ocaml/why3__BigInt_compat.ml
131

Francois Bobot's avatar
Francois Bobot committed
132 133
# /share/
/share/emacs/semantic.cache
134
/share/Makefile.config
135 136 137
/share/drivers
/share/modules
/share/theories
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/why3tac.ml
144
/src/coq-tactic/.why3-vo-*
Francois Bobot's avatar
Francois Bobot committed
145

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

152
# Isabelle
MARCHE Claude's avatar
MARCHE Claude committed
153
/lib/isabelle/bool/
154
/lib/isabelle/int/
MARCHE Claude's avatar
MARCHE Claude committed
155
/lib/isabelle/number/
156 157
/lib/isabelle/list/
/lib/isabelle/map/
158
/lib/isabelle/real/
159
/lib/isabelle/set/
160 161 162
/lib/isabelle/Tools/why3
/lib/isabelle/Why3_Number.thy
/lib/isabelle/why3.ML
MARCHE Claude's avatar
MARCHE Claude committed
163
/lib/isabelle/last_build
164

Francois Bobot's avatar
Francois Bobot committed
165 166 167 168
# /src/driver/
/src/driver/driver_lexer.ml
/src/driver/driver_parser.ml
/src/driver/driver_parser.mli
169
/src/driver/driver_parser.conflicts
170 171 172
/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
173 174 175 176 177

# /src/parser/
/src/parser/lexer.ml
/src/parser/parser.ml
/src/parser/parser.mli
178
/src/parser/parser.conflicts
Francois Bobot's avatar
Francois Bobot committed
179

180
# /src/why3doc/
181
/src/why3doc/doc_lexer.ml
182

Francois Bobot's avatar
Francois Bobot committed
183
# /src/util/
184
/src/util/config.ml
185
/src/util/lexlib.ml
Francois Bobot's avatar
Francois Bobot committed
186 187
/src/util/rc.ml

188 189
# /src/session
/src/session/xml.ml
190
/src/session/compress.ml
191
/src/session/strategy_parser.ml
192

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
193 194 195
# /src/tools
/src/tools/why3wc.ml

Andrei Paskevich's avatar
Andrei Paskevich committed
196 197 198 199
# /plugins/tptp/
/plugins/tptp/tptp_lexer.ml
/plugins/tptp/tptp_parser.ml
/plugins/tptp/tptp_parser.mli
200
/plugins/tptp/tptp_parser.conflicts
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
201
/plugins/parser/dimacs.ml
Andrei Paskevich's avatar
Andrei Paskevich committed
202

203 204
# /drivers
/drivers/coq-realizations.aux
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
205
/drivers/pvs-realizations.aux
206
/drivers/isabelle-realizations.aux
207

Francois Bobot's avatar
Francois Bobot committed
208
# /tests/
209
/tests/test-jcf/
210
/tests/test-pgm-jcf/
MARCHE Claude's avatar
MARCHE Claude committed
211
/tests/test-claude/
212
/tests/test-and/
213 214
/tests/test-extraction/*
!/tests/test-extraction/main.ml
MARCHE Claude's avatar
MARCHE Claude committed
215 216

# /examples/
Andrei Paskevich's avatar
Andrei Paskevich committed
217 218 219 220 221
/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/
MARCHE Claude's avatar
MARCHE Claude committed
222
/examples/why3bench.html
MARCHE Claude's avatar
MARCHE Claude committed
223 224
/examples/why3regtests.err
/examples/why3regtests.out
MARCHE Claude's avatar
MARCHE Claude committed
225
/examples/*/*.opt
226
/examples/*/*.byte
227 228
/examples/in_progress/*/*.opt
/examples/in_progress/*/*.byte
MARCHE Claude's avatar
MARCHE Claude committed
229
/examples/*.html
MARCHE Claude's avatar
MARCHE Claude committed
230
/examples/*/*.html
231
!/examples/*/index.html
MARCHE Claude's avatar
MARCHE Claude committed
232
/examples/*/*/*.html
233
!/examples/*/*/index.html
MARCHE Claude's avatar
MARCHE Claude committed
234
/examples/*/*/*/*.html
235
!/examples/*/*/*/index.html
MARCHE Claude's avatar
MARCHE Claude committed
236
/examples/style.css
237 238 239
/examples/*/style.css
/examples/*/*/style.css
/examples/*/*/*/style.css
240 241 242
/examples/*/*.tex
/examples/*/*/*.tex
/examples/*/*/*/*.tex
Andrei Paskevich's avatar
Andrei Paskevich committed
243 244
/examples/use_api/runstrat/makejob.opt
/examples/use_api/runstrat/runstrat.opt
245
/examples/vstte10_max_sum/*__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
246 247
/examples/euler001/*__*.ml
/examples/sudoku/*__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
248
/examples/sudoku/jsmain.js
MARCHE Claude's avatar
MARCHE Claude committed
249 250
/examples/in_progress/sudoku_reloaded/*__*.ml
/examples/in_progress/sudoku_reloaded/jsmain.js
MARCHE Claude's avatar
MARCHE Claude committed
251 252
/examples/gcd/*__*.ml
/examples/gcd/jsmain.js
MARCHE Claude's avatar
MARCHE Claude committed
253
/examples/defunctionalization/*__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
254 255 256 257
/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
258 259
/examples/in_progress/mp/jsmain.js
/examples/in_progress/mp/*__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
260 261
/examples/in_progress/prover/build/*__*.ml
/examples/in_progress/prover/.depend
262
/examples/in_progress/prover/build/prover
263

264
# modules
265
/modules/string/
266
/modules/stack/
267
/modules/queue/
268
/modules/pqueue/
269 270
/modules/mach/array/
/modules/mach/int/
271

272 273 274
# Try Why3
/src/trywhy3/trywhy3.js
/src/trywhy3/trywhy3.byte
MARCHE Claude's avatar
MARCHE Claude committed
275 276
/src/trywhy3/index.en.html
/src/trywhy3/index.fr.html
277
/src/trywhy3/index.html
MARCHE Claude's avatar
MARCHE Claude committed
278
/src/trywhy3/ace-builds
279 280
/src/trywhy3/*.png
/src/trywhy3/alt-ergo-1.00-private-2015-01-29
MARCHE Claude's avatar
MARCHE Claude committed
281

MARCHE Claude's avatar
MARCHE Claude committed
282 283
# jessie3
/src/jessie/config.log
MARCHE Claude's avatar
MARCHE Claude committed
284
/src/jessie/Makefile
MARCHE Claude's avatar
MARCHE Claude committed
285
/src/jessie/literals.ml
MARCHE Claude's avatar
MARCHE Claude committed
286
/src/jessie/tests/ptests_config
MARCHE Claude's avatar
MARCHE Claude committed
287
/src/jessie/tests/basic/result/*.log
288
/src/jessie/tests/demo/result/*.log
MARCHE Claude's avatar
MARCHE Claude committed
289

290
/trash