.gitignore 3.89 KB
Newer Older
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre 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 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
*.annot
Andrei Paskevich's avatar
Andrei Paskevich committed
15
*.dep
16 17 18
*.vo
*.vd
*.glob
François Bobot's avatar
François Bobot committed
19
\#*\#
20

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

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

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

# /doc/
/doc/version.tex
MARCHE Claude's avatar
MARCHE Claude committed
80
/doc/ocamldoc.sty
Francois Bobot's avatar
Francois Bobot committed
81 82 83 84
/doc/*whizzy*
/doc/manual.wdvi
/doc/manual.raux
/doc/manual.log
85
/doc/manual.lof
Francois Bobot's avatar
Francois Bobot committed
86 87 88 89 90 91 92
/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
93
/doc/manual.rel
MARCHE Claude's avatar
MARCHE Claude committed
94 95 96 97
/doc/manual.glg
/doc/manual.glo
/doc/manual.gls
/doc/manual.ist
98
/doc/manual.out
MARCHE Claude's avatar
MARCHE Claude committed
99
/doc/manual.image.out
Francois Bobot's avatar
Francois Bobot committed
100 101
/doc/*.haux
/doc/*.pdf
102
/doc/html/
Francois Bobot's avatar
Francois Bobot committed
103 104
/doc/*.hind
/doc/*.htoc
MARCHE Claude's avatar
MARCHE Claude committed
105 106 107
/doc/bnf
/doc/bnf.ml
/doc/*_bnf.tex
108
/doc/apidoc.tex
MARCHE Claude's avatar
MARCHE Claude committed
109
/doc/apidoc/
MARCHE Claude's avatar
MARCHE Claude committed
110
/doc/stdlibdoc/
Francois Bobot's avatar
Francois Bobot committed
111

112 113 114 115 116 117
# /lib
/lib/why3-cpulimit
/lib/why3-cpulimit.exe

# /lib/why3/
/lib/why3/META
118 119 120

# /lib/ocaml/
/lib/ocaml/why3__BigInt.ml
121

Francois Bobot's avatar
Francois Bobot committed
122 123 124 125
# /share/
/share/emacs/semantic.cache

# /src/
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
126
/src/config.sh
Francois Bobot's avatar
Francois Bobot committed
127

128
# Coq tactic
129
/src/coq-tactic/coqCompat.ml
130 131
/src/coq-tactic/g_why3tac.ml
/src/coq-tactic/.why3-vo-*
Francois Bobot's avatar
Francois Bobot committed
132

Jean-Christophe's avatar
Jean-Christophe committed
133 134
# PVS
.pvscontext
Jean-Christophe's avatar
Jean-Christophe committed
135
orphaned-proofs.prf
Jean-Christophe's avatar
Jean-Christophe committed
136 137 138
/lib/pvs/*/*.summary
pvsbin/

139 140 141 142 143
# Isabelle
/lib/isabelle/int/
/lib/isabelle/list/
/lib/isabelle/map/
/lib/isabelle/set/
144

Francois Bobot's avatar
Francois Bobot committed
145 146 147 148
# /src/driver/
/src/driver/driver_lexer.ml
/src/driver/driver_parser.ml
/src/driver/driver_parser.mli
149
/src/driver/driver_parser.output
Francois Bobot's avatar
Francois Bobot committed
150 151 152 153 154

# /src/parser/
/src/parser/lexer.ml
/src/parser/parser.ml
/src/parser/parser.mli
155
/src/parser/parser.output
Francois Bobot's avatar
Francois Bobot committed
156

157
# /src/why3doc/
158
/src/why3doc/doc_lexer.ml
159

Francois Bobot's avatar
Francois Bobot committed
160
# /src/util/
161
/src/util/config.ml
Francois Bobot's avatar
Francois Bobot committed
162 163
/src/util/rc.ml

164 165 166
# /src/session
/src/session/xml.ml

Andrei Paskevich's avatar
Andrei Paskevich committed
167 168 169 170 171
# /plugins/tptp/
/plugins/tptp/tptp_lexer.ml
/plugins/tptp/tptp_parser.ml
/plugins/tptp/tptp_parser.mli
/plugins/tptp/tptp_parser.output
172
/plugins/parser/dimacs.ml
Andrei Paskevich's avatar
Andrei Paskevich committed
173

174 175
# /drivers
/drivers/coq-realizations.aux
Jean-Christophe's avatar
Jean-Christophe committed
176
/drivers/pvs-realizations.aux
177
/drivers/isabelle-realizations.aux
178

Francois Bobot's avatar
Francois Bobot committed
179
# /tests/
180
/tests/test-jcf/
181
/tests/test-pgm-jcf/
MARCHE Claude's avatar
MARCHE Claude committed
182
/tests/test-claude/
183
/tests/test-and/
MARCHE Claude's avatar
MARCHE Claude committed
184 185

# /examples/
Andrei Paskevich's avatar
Andrei Paskevich committed
186 187 188 189 190 191
/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
192
/examples/why3bench.html
MARCHE Claude's avatar
MARCHE Claude committed
193 194
/examples/why3regtests.err
/examples/why3regtests.out
MARCHE Claude's avatar
MARCHE Claude committed
195
/examples/*/*.opt
196
/examples/*/*.byte
197 198
/examples/in_progress/*/*.opt
/examples/in_progress/*/*.byte
MARCHE Claude's avatar
MARCHE Claude committed
199 200 201
/examples/*/*.html
/examples/*/*/*.html
/examples/*/*/*/*.html
202 203 204
/examples/*/style.css
/examples/*/*/style.css
/examples/*/*/*/style.css
205 206 207
/examples/*/*.tex
/examples/*/*/*.tex
/examples/*/*/*/*.tex
Andrei Paskevich's avatar
Andrei Paskevich committed
208 209
/examples/use_api/runstrat/makejob.opt
/examples/use_api/runstrat/runstrat.opt
210
/examples/euler001/euler001__*.ml
211
/examples/euler001/Makefile
212
/examples/sudoku/sudoku__*.ml
213
/examples/in_progress/defunctionalization/defunctionalization__*.ml
214

215
# modules
216
/modules/string/
217
/modules/stack/
218
/modules/queue/
219
/modules/pqueue/
220 221
/modules/mach/array/
/modules/mach/int/
222

223 224 225 226 227 228
# 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
229
/src/jessie/Makefile
MARCHE Claude's avatar
MARCHE Claude committed
230
/src/jessie/literals.ml
231
/src/jessie/ptests_local_config.ml
MARCHE Claude's avatar
MARCHE Claude committed
232
/src/jessie/tests/basic/result/*.log
233
/src/jessie/tests/demo/result/*.log
234
/trash