?  search:
summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
blame | history | raw | HEAD
fix sessions and CE oracles
[why3.git] / Makefile.in
blob900076c2442110ec885742bf140a83720224b5db
1 ####################################################################
2 # #
3 # The Why3 Verification Platform / The Why3 Development Team #
4 # Copyright 2010-2023 -- Inria - CNRS - Paris-Saclay University #
5 # #
6 # This software is distributed under the terms of the GNU Lesser #
7 # General Public License version 2.1, with the special exception #
8 # on linking described in file LICENSE. #
9 # #
10 ####################################################################
11
12 VERBOSEMAKE ?= @enable_verbose_make@
13
14 ifeq ($(VERBOSEMAKE),yes)
15 SHOW = @true
16 HIDE =
17 else
18 SHOW = @echo
19 HIDE = @
20 endif
21
22 # install the binaries
23 DESTDIR =
24
25 prefix = @prefix@
26 exec_prefix = @exec_prefix@
27 datarootdir = @datarootdir@
28
29 BINDIR = $(DESTDIR)@bindir@
30 LIBDIR = $(DESTDIR)@libdir@
31 DATADIR = $(DESTDIR)@datarootdir@
32 MANDIR = $(DESTDIR)@mandir@
33 TOOLDIR = $(LIBDIR)/why3/commands
34
35 # OS specific stuff
36 EXE = @EXE@
37
38 # other variables
39 CC = @CC@
40 MKDIR_P = @MKDIR_P@
41 INSTALL = @INSTALL@
42 INSTALL_DATA = @INSTALL_DATA@
43
44 ifeq (@enable_ocamlfind@,yes)
45 OCAMLC = @OCAMLFIND@ ocamlc
46 OCAMLOPT = @OCAMLFIND@ ocamlopt
47 OCAMLDEP = @OCAMLFIND@ ocamldep
48 OCAMLDOC = @OCAMLFIND@ ocamldoc
49 else
50 OCAMLC = @OCAMLC@
51 OCAMLOPT = @OCAMLOPT@
52 OCAMLDEP = @OCAMLDEP@
53 OCAMLDOC = @OCAMLDOC@
54 endif
55
56 OCAMLFIND = @OCAMLFIND@
57 OCAMLLEX = @OCAMLLEX@
58 OCAMLYACC = @OCAMLYACC@
59 OCAMLLIB = @OCAMLLIB@
60 OCAMLINSTALLLIB = $(DESTDIR)@OCAMLINSTALLLIB@
61 OCAMLBEST = @OCAMLBEST@
62 OCAMLVERSION = @OCAMLVERSION@
63 COQC = @COQC@
64 COQDEP = @COQDEP@
65 COQFLAGS = @COQFLAGS@
66 FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@
67 MENHIR = @MENHIR@
68
69 DEPFLAGS = -slash
70
71 ifeq (@enable_why3_lib@,yes)
72 INCLUDES += -I lib/why3
73 endif
74 ifeq (@OCAMLBEST@,opt)
75 # the semantics of the -native flag changed in ocaml 4.03.0
76 #DEPFLAGS += -native
77 endif
78
79 ifeq (@OCAMLBEST@,opt)
80 SHAREDBEST=cmxs
81 else
82 SHAREDBEST=cma
83 endif
84
85 ifeq (@LATEX@,rubber)
86 LATEXCOMP=rubber --warn all --pdf
87 LATEXCLEAN=rubber --pdf --clean
88 endif
89
90 ifeq (@LATEX@,latexmk)
91 LATEXCOMP=LATEXOPTS= latexmk --pdf
92 LATEXCLEAN=LATEXOPTS= latexmk --pdf -C
93 endif
94
95 ifeq (@LATEX@,pdflatex)
96 LATEXCOMP=pdflatex
97 LATEXCLEAN=true
98 endif
99
100 SPHINX = @SPHINX@
101
102 EMACS = @EMACS@
103
104 #PSVIEWER = @PSVIEWER@
105 #PDFVIEWER = @PDFVIEWER@
106
107 EXTINCLUDES = @WHY3INCLUDE@ @REINCLUDE@ @ZIPINCLUDE@ @MENHIRINCLUDE@ @BIGINTINCLUDE@ @INFERINCLUDE@
108
109 # warnings are enabled and non fatal by default, except:
110 # - disabled:
111 # 4 Fragile pattern matching: matching that will remain complete even
112 # if additional constructors are added to one of the variant types
113 # matched.
114 # 9 Missing fields in a record pattern.
115 # 41 Ambiguous constructor or label name.
116 # 42 Reliance on type-directed disambiguation
117 # 44 Open statement shadows an already defined identifier.
118 # 45 Open statement shadows an already defined label or constructor.
119 # 52 The argument of this constructor should not be matched against a
120 # constant pattern; the actual value of the argument could change
121 # in the future.
122 # - fatal:
123 # 5 Partially applied function: expression whose result has function
124 # type and is ignored.
125 # 8 Partial match: missing cases in pattern-matching.
126 # 14 Illegal backslash escape in string
127 # 48 Implicit elimination of optional arguments.
128 # 50 Unexpected documentation comment.
129
130 WARNINGS = A-4-9-41-42-44-45-52@5@8@14@48@50
131
132 FLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g -thread $(INCLUDES)
133 OFLAGS = $(FLAGS)
134 BFLAGS = $(FLAGS)
135
136 ifeq (@enable_ocamlfind@,yes)
137 FLAGS += $(addprefix -package ,$(EXTPKGS))
138 OLINKFLAGS += -linkpkg -linkall
139 BLINKFLAGS += -linkpkg -linkall
140 else
141 FLAGS += $(EXTINCLUDES)
142 OLINKFLAGS = -linkall $(EXTCMXA)
143 BLINKFLAGS = -linkall $(EXTCMA)
144 endif
145
146
147 # see http://caml.inria.fr/mantis/view.php?id=4991
148 CMIHACK = -intf-suffix .cmi
149
150 CMP_CP = cmp -s $< $@ || cp $< $@
151
152 # external libraries common to all binaries
153
154 ifeq (@menhirlib_cmo@,yes)
155 EXTOBJS = menhirLib
156 EXTLIBS =
157 else
158 EXTOBJS =
159 EXTLIBS = menhirLib
160 endif
161
162 EXTLIBS += @RELIB@ unix zarith dynlink @ZIPLIB@ @WHY3LIB@ @INFERLIB@
163 EXTPKGS = menhirLib @RELIB@ unix zarith dynlink @ZIPLIB@ @MLMPFR@ @WHY3LIB@ @INFERPKG@ @SEXPLIB@ @SEXPLIBPPX@
164
165 EXTCMA = $(addsuffix .cmo,$(EXTOBJS)) $(addsuffix .cma,$(EXTLIBS))
166 EXTCMXA = $(addsuffix .cmx,$(EXTOBJS)) $(addsuffix .cmxa,$(EXTLIBS))
167
168 INSTALLED_LIB_EXTS = a cma cmx cmi cmxa cmxs cmt cmti
169 COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo annot dep conflicts
170
171 TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})
172
173 # Variables added for checking realizations
174 GENERATED_PREFIX_COQ="lib/coq"
175 GENERATED_PREFIX_ISABELLE=lib/isabelle
176
177 ifeq (@enable_why3_lib@,yes)
178 WHY3CMA = lib/why3/why3.cma
179 WHY3CMXA = lib/why3/why3.cmxa
180 else
181 WHY3CMA =
182 WHY3CMXA =
183 endif
184
185 ###############
186 # main target
187 ###############
188
189 ifeq (@enable_why3_lib@,yes)
190 all: @OCAMLBEST@
191 else
192 all:
193 endif
194
195 plugins: plugins.@OCAMLBEST@
196 opt: plugins.opt
197 byte: plugins.byte
198
199 ifeq (@enable_local@,yes)
200 all: install_local
201 endif
202
203 .PHONY: byte opt clean depend all install install-lib uninstall
204 .PHONY: install-bin install-data uninstall-bin uninstall-data
205 .PHONY: install-bash install-emacs install-framac
206 .PHONY: uninstall-bash uninstall-emacs uninstall-framac
207 .PHONY: ide install-ide uninstall-ide
208 .PHONY: coq install-coq uninstall-coq clean-coq
209 .PHONY: pvs install-pvs uninstall-pvs clean-pvs
210 .PHONY: install-isabelle clean-isabelle
211 .PHONY: plugins plugins.byte plugins.opt
212 .PHONY: trywhy3 clean-trywhy3
213
214 .SUFFIXES:
215
216 MAKEINC =
217 CLEANDIRS =
218 CLEANLIBS =
219 GENERATED =
220
221 ##############
222 # Why3 library
223 ##############
224
225 LIBGENERATED = \
226 src/util/config.ml \
227 src/util/rc.ml src/util/lexlib.ml src/util/mysexplib.ml \
228 src/util/json_parser.mli src/util/json_parser.ml \
229 src/util/json_lexer.ml src/util/mlmpfr_wrapper.ml \
230 src/parser/lexer.ml \
231 src/core/parser_tokens.mli src/core/parser_tokens.ml \
232 src/parser/parser.mli src/parser/parser.ml \
233 src/parser/parser_messages.ml \
234 src/driver/driver_parser.mli src/driver/driver_parser.ml \
235 src/driver/driver_lexer.ml \
236 src/driver/sexp.ml \
237 src/session/compress.ml src/session/xml.ml \
238 src/session/strategy_parser.ml
239
240 LIB_UTIL = exn_printer mysexplib config bigInt mlmpfr_wrapper util opt lists strings \
241 pp extmap extset exthtbl weakhtbl diffmap hcpt \
242 hashcons wstdlib getopt \
243 json_base json_parser json_lexer \
244 debug loc print_tree \
245 cmdline sysutil lexlib rc plugin bigInt number constant vector pqueue
246
247 ifeq (@enable_re@,no)
248 LIB_UTIL += re
249 endif
250
251 LIB_CORE = \
252 ident ty term pattern decl coercion theory \
253 parser_tokens keywords \
254 task pretty dterm env trans printer model_parser
255
256 LIB_DRIVER = prove_client whyconf call_provers driver_parser driver_lexer driver \
257 autodetection smtv2_model_defs sexp smtv2_model_parser
258
259 LIB_MLW = ity expr pdecl eval_match typeinv vc pmodule dexpr big_real \
260 pinterp_core rac pinterp check_ce
261
262 ifeq (@enable_infer@,yes)
263 LIB_INFER = o2oterm domain infer_why3 quant_domain union_find disjunctive_term_domain uf_domain infer_cfg infer_loop
264 endif
265
266 ifeq (@enable_bddinfer@,yes)
267 LIB_BDDINFER = bddparam abstract ast interp_expression infer why3infer
268 endif
269
270 LIB_EXTRACT = mltree compile mlinterp pdriver ml_printer \
271 c ocaml cakeml java
272
273 LIB_PARSER = ptree ptree_helpers glob typing \
274 parser_messages parser typing report lexer mlw_printer \
275 sexp_parser
276
277 LIB_TRANSFORM = simplify_formula inlining split_goal \
278 args_wrapper reduction_engine compute \
279 remove_unused detect_polymorphism \
280 eliminate_definition extensional \
281 abstract_quantifiers eliminate_unknown_types \
282 eliminate_unknown_lsymbols eliminate_symbol \
283 eliminate_inductive eliminate_let eliminate_if \
284 libencoding eliminate_algebraic discriminate encoding \
285 encoding_select encoding_guards_full encoding_tags_full \
286 encoding_guards encoding_tags encoding_twin \
287 encoding_sort simplify_array filter_trigger \
288 abstraction close_epsilon lift_epsilon \
289 eliminate_epsilon instantiate_predicate smoke_detector \
290 prop_curry eliminate_literal \
291 generic_arg_trans_utils case apply subst \
292 introduction ind_itp destruct cut congruence \
293 induction induction_pr prepare_for_counterexmp \
294 reflection keep_only_arithmetic
295
296 LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\
297 pvs isabelle \
298 simplify gappa cvc3 yices mathematica
299
300 LIB_SESSION = compress xml termcode session_itp \
301 strategy strategy_parser controller_itp \
302 server_utils itp_communication \
303 itp_server json_util unix_scheduler
304
305 LIB_CMIONLY = driver/driver_ast
306
307 LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \
308 $(addprefix src/core/, $(LIB_CORE)) \
309 $(addprefix src/driver/, $(LIB_DRIVER)) \
310 $(addprefix src/mlw/, $(LIB_MLW)) \
311 $(addprefix src/infer/, $(LIB_INFER)) \
312 $(addprefix src/bddinfer/, $(LIB_BDDINFER)) \
313 $(addprefix src/extract/, $(LIB_EXTRACT)) \
314 $(addprefix src/parser/, $(LIB_PARSER)) \
315 $(addprefix src/transform/, $(LIB_TRANSFORM)) \
316 $(addprefix src/printer/, $(LIB_PRINTER)) \
317 $(addprefix src/session/, $(LIB_SESSION))
318
319 LIBDIRS = util core driver mlw extract parser transform printer session
320
321 ifeq (@enable_infer@,yes)
322 LIBDIRS += infer
323 endif
324
325 ifeq (@enable_bddinfer@,yes)
326 LIBDIRS += bddinfer
327 endif
328
329 LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
330
331 LIBDEP = $(addsuffix .dep, $(LIBMODULES)) $(LIB_CMIONLY:%=src/%.dep)
332 LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
333 LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
334 LIBCMI = $(addsuffix .cmi, $(LIBMODULES)) $(LIB_CMIONLY:%=src/%.cmi)
335
336 $(LIBDEP) $(LIBCMO) $(LIBCMX) $(LIBCMI): INCLUDES += $(LIBINCLUDES)
337 $(LIBCMX): OFLAGS += -for-pack Why3
338
339 $(LIBDEP): $(LIBGENERATED)
340
341 src/parser/ptree.cmx src/parser/ptree.cmo: FLAGS += -w -70
342 src/util/mysexplib.cmx src/util/mysexplib.cmo: FLAGS += -w -70
343
344 # Mlmpfr
345
346 ifeq (@enable_mpfr@,yes)
347
348 ifeq (@old_mpfr@,yes)
349 src/util/mlmpfr_wrapper.ml: src/util/mlmpfr_old.ml Makefile
350 $(CMP_CP)
351 else ifeq (@enable_mpfr@,yes)
352 src/util/mlmpfr_wrapper.ml: src/util/mlmpfr_real.ml Makefile
353 $(CMP_CP)
354 endif
355
356 else
357 src/util/mlmpfr_wrapper.ml: src/util/mlmpfr_dummy.ml Makefile
358 $(CMP_CP)
359 endif
360
361 # Ocamlzip
362
363 ifeq (@enable_zip@,yes)
364 src/session/compress.ml: src/session/compress_z.ml Makefile
365 $(CMP_CP)
366 else
367 src/session/compress.ml: src/session/compress_none.ml Makefile
368 $(CMP_CP)
369 endif
370
371 # sexp_conv
372
373 ifeq (@enable_sexp@, yes)
374 src/util/mysexplib.ml: src/util/mysexplib-real.ml Makefile
375 $(CMP_CP)
376 else
377 src/util/mysexplib.ml: src/util/mysexplib-dummy.ml Makefile
378 $(CMP_CP)
379 endif
380
381 .PHONY: initialize_messages update-parsing-error-handling
382
383 PARSERS=src/parser/parser_common.mly src/parser/parser.mly
384
385 src/parser/parser_messages.ml: src/parser/handcrafted.messages
386 @rm -f src/parser/parser_messages.ml src/parser/parser_messages.ml.tmp
387 @$(MENHIR) --explain --strict $(PARSERS) --base src/parser/parser --update-errors \
388 src/parser/handcrafted.messages > src/parser/handcrafted.messages.temp
389 @if ! diff -b src/parser/handcrafted.messages src/parser/handcrafted.messages.temp > /dev/null; then \
390 echo "Parsing error handling must be updated, the file 'src/parser/handcrafted.messages.temp' \
391 contains an updated version that must be checked before replacing 'src/parser/handcrafted.messages'"; \
392 exit 1; \
393 fi
394 @rm -f src/parser/handcrafted.messages.temp
395 $(MENHIR) --explain --strict $(PARSERS) --base src/parser/parser --compile-errors \
396 src/parser/handcrafted.messages > src/parser/parser_messages.ml
397
398 clean::
399 rm -f src/parser/parser_messages.ml.tmp src/parser/handcrafted.messages.temp
400
401 # debug optimisation ppx
402
403 ifeq (@enable_ppx@,yes)
404 src/util/ppx_debug_optim: src/util/debug_optim.ml
405 $(SHOW) 'Linking $@'
406 $(HIDE) $(OCAMLFIND) opt -package compiler-libs.common -linkpkg src/util/debug_optim.ml -o $@
407
408 src/transform/reflection.cmx: src/util/ppx_debug_optim
409 src/transform/reflection.cmx: OFLAGS += -ppx src/util/ppx_debug_optim
410 src/extract/mlinterp.cmx: src/util/ppx_debug_optim
411 src/extract/mlinterp.cmx: OFLAGS += -ppx src/util/ppx_debug_optim
412
413 clean::
414 rm -f src/util/ppx_debug_optim
415 endif
416
417 # Re
418
419 ifeq (@enable_re@,no)
420 src/util/re.ml: src/util/recompat.ml Makefile
421 $(CMP_CP)
422 LIBGENERATED += src/util/re.ml
423 endif
424 GENERATED += src/util/re.ml
425
426 # build targets
427
428 byte: lib/why3/why3.cma
429 opt: lib/why3/why3.cmxa lib/why3/why3.cmxs
430
431 lib/why3/why3.cma: lib/why3/why3.cmo
432 lib/why3/why3.cmxa: lib/why3/why3.cmx
433 lib/why3/why3.cmxs: lib/why3/why3.cmx
434
435 lib/why3/why3.cmo: $(LIBCMO)
436 $(SHOW) 'Linking $@'
437 $(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
438
439 lib/why3/why3.cmx: $(LIBCMX) lib/why3/why3.cmo
440 $(SHOW) 'Linking $@'
441 $(HIDE)$(OCAMLOPT) $(OFLAGS) $(CMIHACK) -pack -o $@ $(filter %.cmx, $^)
442
443 # clean and depend
444
445 MAKEINC += $(LIBDEP)
446
447 CLEANDIRS += src $(addprefix src/, $(LIBDIRS))
448 CLEANLIBS += lib/why3/why3
449 GENERATED += $(LIBGENERATED)
450
451 ###############
452 # installation
453 ###############
454
455 uninstall-data::
456 rm -rf $(DATADIR)/why3
457
458 install-data::
459 $(MKDIR_P) $(DATADIR)/why3
460 $(MKDIR_P) $(DATADIR)/why3/vim
461 $(MKDIR_P) $(DATADIR)/why3/vim/ftdetect
462 $(MKDIR_P) $(DATADIR)/why3/vim/syntax
463 $(MKDIR_P) $(DATADIR)/why3/lang
464 $(MKDIR_P) $(DATADIR)/why3/stdlib
465 $(MKDIR_P) $(DATADIR)/why3/stdlib/mach
466 $(MKDIR_P) $(DATADIR)/why3/stdlib/mach/java
467 $(MKDIR_P) $(DATADIR)/why3/drivers
468 $(MKDIR_P) $(DATADIR)/why3/extraction_drivers
469 $(INSTALL_DATA) stdlib/*.mlw $(DATADIR)/why3/stdlib
470 $(INSTALL_DATA) stdlib/mach/*.mlw $(DATADIR)/why3/stdlib/mach
471 $(INSTALL_DATA) stdlib/mach/java/*.mlw $(DATADIR)/why3/stdlib/mach/java
472 $(INSTALL_DATA) drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
473 $(INSTALL_DATA) extraction_drivers/*.drv $(DATADIR)/why3/extraction_drivers
474 $(INSTALL_DATA) LICENSE $(DATADIR)/why3/
475 $(INSTALL_DATA) share/provers-detection-data.conf $(DATADIR)/why3/
476 $(INSTALL_DATA) share/why3session.dtd $(DATADIR)/why3
477 $(INSTALL_DATA) share/Makefile.config $(DATADIR)/why3
478 $(INSTALL_DATA) share/vim/ftdetect/why3.vim $(DATADIR)/why3/vim/ftdetect/why3.vim
479 $(INSTALL_DATA) share/vim/syntax/why3.vim $(DATADIR)/why3/vim/syntax/why3.vim
480 $(INSTALL_DATA) share/lang/why3.lang $(DATADIR)/why3/lang/why3.lang
481 $(INSTALL_DATA) share/lang/why3c.lang $(DATADIR)/why3/lang/why3c.lang
482 $(INSTALL_DATA) share/lang/why3py.lang $(DATADIR)/why3/lang/why3py.lang
483 $(INSTALL_DATA) share/lang/coma.lang $(DATADIR)/why3/lang/coma.lang
484
485 ifeq (@enable_local@,yes)
486 else
487 install:: install-bin install-data
488
489 uninstall:: uninstall-bin uninstall-data
490 rm -rf $(LIBDIR)/why3
491 endif
492
493 uninstall-lib:
494 if test -d $(OCAMLINSTALLLIB) -a -w $(OCAMLINSTALLLIB); then \
495 rm -rf $(OCAMLINSTALLLIB)/why3; \
496 fi
497
498 uninstall:: uninstall-lib
499
500 install-lib::
501 $(MKDIR_P) $(OCAMLINSTALLLIB)/why3
502 $(INSTALL_DATA) $(wildcard $(addprefix lib/why3/why3., $(INSTALLED_LIB_EXTS))) \
503 lib/why3/META $(OCAMLINSTALLLIB)/why3
504
505 ##################
506 # Why3 emacs mode
507 ##################
508
509 %.elc: %.el
510 $(EMACS) --batch --no-init-file -f batch-byte-compile $<
511
512 clean::
513 rm -f share/emacs/why3.elc
514
515 uninstall-emacs:
516 rm -f $(DATADIR)/emacs/site-lisp/why3.el
517 rm -f $(DATADIR)/emacs/site-lisp/why3.elc
518
519 uninstall:: uninstall-emacs
520
521 install-emacs:
522 $(MKDIR_P) $(DATADIR)/emacs/site-lisp/
523 $(INSTALL_DATA) share/emacs/why3.el $(DATADIR)/emacs/site-lisp/why3.el
524 ifeq (@enable_emacs_compilation@,yes)
525 $(INSTALL_DATA) share/emacs/why3.elc $(DATADIR)/emacs/site-lisp/why3.elc
526 endif
527
528 install:: install-emacs
529
530 ifeq (@enable_emacs_compilation@,yes)
531 all: share/emacs/why3.elc
532 endif
533
534
535 ##################
536 # Why3 plugins
537 ##################
538
539 PLUGGENERATED = \
540 plugins/tptp/tptp_lexer.ml \
541 plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli \
542 plugins/coma/coma_lexer.ml \
543 plugins/coma/coma_parser.ml plugins/coma/coma_parser.mli \
544 plugins/python/py_lexer.ml \
545 plugins/python/py_parser.ml plugins/python/py_parser.mli \
546 plugins/microc/mc_lexer.ml \
547 plugins/microc/mc_parser.ml plugins/microc/mc_parser.mli \
548 plugins/cfg/cfg_lexer.ml \
549 plugins/cfg/cfg_parser.ml plugins/cfg/cfg_parser.mli \
550 plugins/parser/dimacs.ml
551
552 PLUG_PARSER = genequlin dimacs
553 PLUG_PRINTER =
554 PLUG_TRANSFORM =
555 PLUG_STRATEGIES = forward_propagation
556 PLUG_TPTP = tptp_parser tptp_typing tptp_lexer tptp_printer
557 PLUG_COMA = coma_logic coma_syntax coma_parser coma_lexer coma_typing coma_main
558 PLUG_PYTHON = py_parser py_lexer py_main
559 PLUG_MICROC = mc_parser mc_lexer mc_printer mc_main
560 PLUG_CFG = cfg_parser cfg_lexer cfg_paths subregion_analysis cfg_main
561 ifeq (@enable_stackify@,yes)
562 PLUG_CFG += stackify cfg_stackify
563 endif
564
565 PLUG_CMIONLY = tptp/tptp_ast python/py_ast microc/mc_ast cfg/cfg_ast
566
567 PLUGINS = genequlin dimacs tptp python microc coma cfg forward_propagation
568
569 TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
570 COMAMODULES = $(addprefix plugins/coma/, $(PLUG_COMA))
571 PYTHONMODULES = $(addprefix plugins/python/, $(PLUG_PYTHON))
572 MICROCMODULES = $(addprefix plugins/microc/, $(PLUG_MICROC))
573 CFGMODULES = $(addprefix plugins/cfg/, $(PLUG_CFG))
574
575 TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
576 TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
577
578 COMACMO = $(addsuffix .cmo, $(COMAMODULES))
579 COMACMX = $(addsuffix .cmx, $(COMAMODULES))
580
581 PYTHONCMO = $(addsuffix .cmo, $(PYTHONMODULES))
582 PYTHONCMX = $(addsuffix .cmx, $(PYTHONMODULES))
583
584 MICROCCMO = $(addsuffix .cmo, $(MICROCMODULES))
585 MICROCCMX = $(addsuffix .cmx, $(MICROCMODULES))
586
587 ifeq (@enable_hypothesis_selection@,yes)
588 PLUG_TRANSFORM += hypothesis_selection
589 PLUGINS += hypothesis_selection
590
591 lib/plugins/hypothesis_selection.cmxs: EXTINCLUDES += -I @OCAMLGRAPHLIB@
592 lib/plugins/hypothesis_selection.cma: EXTINCLUDES += -I @OCAMLGRAPHLIB@
593 lib/plugins/hypothesis_selection.cmxs: EXTLIBS += graph.cmxa
594 lib/plugins/hypothesis_selection.cma: EXTOBJS += graph.cma
595 ifeq (@enable_ocamlfind@,yes)
596 lib/plugins/hypothesis_selection.cmxs: FLAGS += -package ocamlgraph -dontlink "$(EXTPKGS)" -linkpkg
597 lib/plugins/hypothesis_selection.cma: FLAGS += -package ocamlgraph -dontlink "$(EXTPKGS)" -linkpkg
598 endif
599 endif
600
601 PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
602 $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
603 $(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
604 $(addprefix plugins/strategies/, $(PLUG_STRATEGIES)) \
605 $(TPTPMODULES) $(COMAMODULES) \
606 $(PYTHONMODULES) $(MICROCMODULES) $(CFGMODULES)
607
608 PLUGDEP = $(addsuffix .dep, $(PLUGMODULES)) $(PLUG_CMIONLY:%=plugins/%.dep)
609 PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
610 PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
611 PLUGCMI = $(addsuffix .cmi, $(PLUGMODULES)) $(PLUG_CMIONLY:%=plugins/%.cmi)
612
613 PLUGDIRS = parser printer transform strategies tptp coma python microc cfg
614 PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))
615
616 ifeq (@enable_stackify@,yes)
617 plugins/cfg/stackify.cmx: EXTINCLUDES += -I @OCAMLGRAPHLIB@
618 plugins/cfg/stackify.cmo: EXTINCLUDES += -I @OCAMLGRAPHLIB@
619 plugins/cfg/stackify.cmx: EXTLIBS += graph.cmxa
620 plugins/cfg/stackify.cmo: EXTOBJS += graph.cma
621 ifeq (@enable_ocamlfind@,yes)
622 plugins/cfg/stackify.cmx: FLAGS += -package ocamlgraph
623 plugins/cfg/stackify.cmo: FLAGS += -package ocamlgraph
624 lib/plugins/cfg.cmxs: FLAGS += -package ocamlgraph -dontlink "$(EXTPKGS)" -linkpkg
625 lib/plugins/cfg.cma: FLAGS += -package ocamlgraph -dontlink "$(EXTPKGS)" -linkpkg
626 endif
627 endif
628
629 $(PLUGDEP) $(PLUGCMO) $(PLUGCMX) $(PLUGCMI): INCLUDES += $(PLUGINCLUDES)
630
631 $(PLUGDEP): $(PLUGGENERATED)
632
633 LIBPLUGCMA = $(PLUGINS:%=lib/plugins/%.cma)
634 LIBPLUGCMXS = $(PLUGINS:%=lib/plugins/%.cmxs)
635
636 plugins.byte: $(LIBPLUGCMA)
637 plugins.opt : $(LIBPLUGCMXS)
638
639 lib/plugins:
640 mkdir lib/plugins
641
642 lib/plugins/%.cmxs: | lib/plugins
643 $(SHOW) 'Linking $@'
644 $(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
645
646 lib/plugins/%.cma: | lib/plugins
647 $(SHOW) 'Linking $@'
648 $(HIDE)$(OCAMLC) $(BFLAGS) -a -o $@ $^
649
650 $(PLUG_PARSER:%=lib/plugins/%.cmxs): lib/plugins/%.cmxs: plugins/parser/%.cmx
651 $(PLUG_PARSER:%=lib/plugins/%.cma): lib/plugins/%.cma: plugins/parser/%.cmo
652 $(PLUG_PRINTER:%=lib/plugins/%.cmxs): lib/plugins/%.cmxs: plugins/printer/%.cmx
653 $(PLUG_PRINTER:%=lib/plugins/%.cma): lib/plugins/%.cma: plugins/printer/%.cmo
654 $(PLUG_TRANSFORM:%=lib/plugins/%.cmxs): lib/plugins/%.cmxs: plugins/transform/%.cmx
655 $(PLUG_TRANSFORM:%=lib/plugins/%.cma): lib/plugins/%.cma: plugins/transform/%.cmo
656 $(PLUG_STRATEGIES:%=lib/plugins/%.cmxs): lib/plugins/%.cmxs: plugins/strategies/%.cmx
657 $(PLUG_STRATEGIES:%=lib/plugins/%.cma): lib/plugins/%.cma: plugins/strategies/%.cmo
658 lib/plugins/tptp.cmxs: $(TPTPCMX)
659 lib/plugins/tptp.cma: $(TPTPCMO)
660 lib/plugins/coma.cmxs: $(COMACMX)
661 lib/plugins/coma.cma: $(COMACMO)
662 lib/plugins/python.cmxs: $(PYTHONCMX)
663 lib/plugins/python.cma: $(PYTHONCMO)
664 lib/plugins/microc.cmxs: $(MICROCCMX)
665 lib/plugins/microc.cma: $(MICROCCMO)
666 lib/plugins/cfg.cmxs: $(addsuffix .cmx, $(CFGMODULES))
667 lib/plugins/cfg.cma: $(addsuffix .cmo, $(CFGMODULES))
668
669 # depend and clean targets
670
671 MAKEINC += $(PLUGDEP)
672
673 CLEANDIRS += plugins $(addprefix plugins/, $(PLUGDIRS)) lib/plugins
674 GENERATED += $(PLUGGENERATED)
675
676 uninstall-bin::
677 rm -f $(PLUGINS:%=$(LIBDIR)/why3/plugins/%.cma)
678 rm -f $(PLUGINS:%=$(LIBDIR)/why3/plugins/%.cmxs)
679
680 install-bin::
681 $(MKDIR_P) $(LIBDIR)/why3/plugins
682 $(INSTALL_DATA) $(wildcard $(LIBPLUGCMA) $(LIBPLUGCMXS)) $(LIBDIR)/why3/plugins
683
684 ###############
685 # Why3 commands
686 ###############
687
688 TOOLSGENERATED = src/tools/why3wc.ml
689
690 TOOLS_BIN = \
691 why3config why3execute why3extract why3prove \
692 why3realize why3replay why3show why3wc why3bench
693
694 TOOLS_FILES = main $(TOOLS_BIN)
695
696 TOOLSMODULES = $(addprefix src/tools/, $(TOOLS_FILES))
697
698 TOOLSDEP = $(addsuffix .dep, $(TOOLSMODULES))
699 TOOLSCMO = $(addsuffix .cmo, $(TOOLSMODULES))
700 TOOLSCMX = $(addsuffix .cmx, $(TOOLSMODULES))
701
702 $(TOOLSDEP) $(TOOLSCMO) $(TOOLSCMX): INCLUDES += -I src/tools
703
704 $(TOOLSDEP): $(TOOLSGENERATED)
705
706 byte: bin/why3.byte $(TOOLS_BIN:%=bin/%.cma)
707 opt: bin/why3.opt $(TOOLS_BIN:%=bin/%.cmxs)
708
709 bin/why3.opt: $(WHY3CMXA) src/tools/main.cmx
710 bin/why3.byte: $(WHY3CMA) src/tools/main.cmo
711
712 $(TOOLS_BIN:%=bin/%.cma): bin/%.cma: src/tools/%.cmo
713 $(TOOLS_BIN:%=bin/%.cmxs): bin/%.cmxs: src/tools/%.cmx
714
715 uninstall-bin::
716 rm -f $(BINDIR)/why3$(EXE)
717 rm -f $(TOOLS_BIN:%=bin/%.$(SHAREDBEST))
718
719 install-bin::
720 $(MKDIR_P) $(BINDIR)
721 $(INSTALL) bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
722 $(MKDIR_P) $(TOOLDIR)
723 $(INSTALL_DATA) $(TOOLS_BIN:%=bin/%.$(SHAREDBEST)) $(TOOLDIR)
724
725 install_local:: bin/why3$(EXE) $(TOOLS_BIN:%=bin/%.$(SHAREDBEST))
726
727 bin/why3$(EXE): bin/why3.@OCAMLBEST@
728 ln -sf $(notdir $<) $@
729
730 install_local:: share/drivers share/extraction_drivers share/stdlib
731
732 share/drivers share/extraction_drivers share/stdlib: share/%:
733 ln -snf ../$* $@
734
735 MAKEINC += $(TOOLSDEP)
736
737 CLEANDIRS += src/tools
738 GENERATED += $(TOOLSGENERATED)
739
740 clean::
741 rm -f bin/why3*
742
743 ##############
744 # Why3server #
745 ##############
746
747 SERVER_MODULES := logging arraylist options queue readbuf request \
748 proc writebuf server-unix server-win
749
750 CPULIM_MODULES := cpulimit-unix cpulimit-win
751
752 SERVER_O := $(SERVER_MODULES:%=src/server/%.o)
753
754 CPULIM_O := $(CPULIM_MODULES:%=src/server/%.o)
755
756 TOOLS = lib/why3server$(EXE) lib/why3cpulimit$(EXE)
757
758 all: $(TOOLS)
759
760 lib/why3server$(EXE): $(SERVER_O)
761 $(CC) -Wall -o $@ $^
762
763 lib/why3cpulimit$(EXE): $(CPULIM_O)
764 $(CC) -Wall -o $@ $^
765
766 %.o: %.c
767 $(CC) -Wall -O -g -o $@ -c $<
768
769 uninstall-bin::
770 rm -f $(LIBDIR)/why3/why3server$(EXE) $(LIBDIR)/why3/why3cpulimit$(EXE)
771 rm -f $(LIBDIR)/why3/why3-call-pvs
772
773 install-bin::
774 $(MKDIR_P) $(LIBDIR)/why3
775 $(INSTALL) lib/why3server$(EXE) $(LIBDIR)/why3/why3server$(EXE)
776 $(INSTALL) lib/why3cpulimit$(EXE) $(LIBDIR)/why3/why3cpulimit$(EXE)
777 $(INSTALL) lib/why3-call-pvs $(LIBDIR)/why3/why3-call-pvs
778
779 clean::
780 rm -f $(SERVER_O) $(CPULIM_O) $(TOOLS)
781
782 ##########
783 # gallery
784 ##########
785
786 # we export exactly the programs that have a why3session.xml file
787
788 .PHONY: gallery gallery-simple gallery-subs
789
790 gallery: gallery-simple gallery-subs
791
792 gallery-simple:
793 @if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
794 @cd examples/; \
795 for x in `git ls-files */why3session.xml` ; do \
796 f=`dirname $$x`; \
797 if echo $$f | grep -q -e '\(_vc_sp\|^bignum\)$$'; then continue; fi; \
798 echo "exporting $$f"; \
799 mkdir -p $(GALLERYDIR)/$$f; \
800 WHY3CONFIG="" ../bin/why3.@OCAMLBEST@ session html $$x -o $(GALLERYDIR)/$$f; \
801 cp $$f.mlw $(GALLERYDIR)/$$f/; \
802 rm -f $(GALLERYDIR)/$$f/$$f.zip; \
803 git archive --format=zip -o $(GALLERYDIR)/$$f/$$f.zip HEAD $$f.mlw $$f; \
804 done
805
806 GALLERYSUBS=WP_revisited verifythis_2016_matrix_multiplication avl double_wp prover multiprecision
807
808 gallery-subs:
809 @if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
810 @for d in $(GALLERYSUBS) ; do \
811 echo "exporting examples/$$d"; \
812 mkdir -p $(GALLERYDIR)/$$d; \
813 cd examples/$$d; \
814 WHY3CONFIG="" ../../bin/why3.@OCAMLBEST@ doc --no-stdlib --no-load-default-plugins -L ../../stdlib -L . --stdlib-url https://www.why3.org/stdlib/ --warn-off=unused_variable *.mlw -o $(GALLERYDIR)/$$d; \
815 cd ..; \
816 rm -f $(GALLERYDIR)/$$d/$$d.zip; \
817 git archive --format=zip -o $(GALLERYDIR)/$$d/$$d.zip HEAD $$d; \
818 cd ..; \
819 done
820
821 ########
822 # XML DTD validation
823 ########
824
825 .PHONY: xml-validate xml-validate-local
826
827 xml-validate:
828 @for x in `find examples/ -name why3session.xml`; do \
829 xmllint --noout --valid $$x 2>&1 | head -1; \
830 done
831
832 xml-validate-local:
833 @for x in `find examples/ -name why3session.xml -print`; do \
834 xmllint --nonet --noout --path share --valid $$x 2>&1 | sed -e '/I.O error/d' | head -1; \
835 done
836
837 ###############
838 # IDE
839 ###############
840
841 IDEGENERATED =
842 GENERATED += $(IDEGENERATED)
843
844 ifeq (@enable_ide@,yes)
845
846 IDE_FILES =
847
848 ifeq (@enable_statmemprof@,yes)
849 IDE_FILES += statmemprof
850
851 bin/why3ide.cmxs bin/why3ide.cma: EXTPKGS += @STATMEMPROFPKG@
852 endif
853
854 IDE_FILES += gconfig ide_utils why3ide
855
856 IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
857
858 IDEDEP = $(addsuffix .dep, $(IDEMODULES))
859 IDECMO = $(addsuffix .cmo, $(IDEMODULES))
860 IDECMX = $(addsuffix .cmx, $(IDEMODULES))
861
862 $(IDEDEP) $(IDECMO) $(IDECMX): INCLUDES += -I src/ide
863
864 $(IDEDEP): $(IDEGENERATED)
865
866 # build targets
867
868 byte: bin/why3ide.cma
869 opt: bin/why3ide.cmxs
870
871 bin/why3ide.cmxs bin/why3ide.cma: FLAGS += $(addprefix -package ,@LABLGTKPKG@) -dontlink "$(EXTPKGS)" -linkpkg
872
873 bin/why3ide.cmxs: $(IDECMX)
874 bin/why3ide.cma: $(IDECMO)
875
876 # depend and clean targets
877
878 MAKEINC += $(IDEDEP)
879
880 CLEANDIRS += src/ide
881
882 ide: bin/why3ide.$(SHAREDBEST)
883
884 uninstall-ide:
885 rm -f $(TOOLDIR)/why3ide.$(SHAREDBEST)
886 rm -rf $(DATADIR)/why3/images
887
888 uninstall:: uninstall-ide
889
890 install-ide:
891 $(MKDIR_P) $(TOOLDIR)
892 $(INSTALL_DATA) bin/why3ide.$(SHAREDBEST) $(TOOLDIR)
893 $(MKDIR_P) $(DATADIR)/why3/images
894 for i in share/images/*.rc; do \
895 d=`basename $$i .rc`; \
896 $(INSTALL_DATA) $$i $(DATADIR)/why3/images; \
897 $(MKDIR_P) $(DATADIR)/why3/images/$$d; \
898 $(INSTALL_DATA) share/images/$$d/* $(DATADIR)/why3/images/$$d; \
899 done
900 $(INSTALL_DATA) share/images/*.png $(DATADIR)/why3/images
901
902 install:: install-ide
903
904 install_local:: bin/why3ide.$(SHAREDBEST)
905
906 endif
907
908 ###############
909 # WEBSERV
910 ###############
911
912 WEBSERV_FILES = wserver why3web
913
914 WEBSERVMODULES = $(addprefix src/ide/, $(WEBSERV_FILES))
915
916 WEBSERVDEP = $(addsuffix .dep, $(WEBSERVMODULES))
917 WEBSERVCMO = $(addsuffix .cmo, $(WEBSERVMODULES))
918 WEBSERVCMX = $(addsuffix .cmx, $(WEBSERVMODULES))
919
920 $(WEBSERVDEP) $(WEBSERVCMO) $(WEBSERVCMX): INCLUDES += -I src/ide
921
922 # build targets
923
924 byte: bin/why3webserver.cma
925 opt: bin/why3webserver.cmxs
926
927 bin/why3webserver.cmxs: $(WEBSERVCMX)
928 bin/why3webserver.cma: $(WEBSERVCMO)
929
930 # depend and clean targets
931
932 MAKEINC += $(WEBSERVDEP)
933
934 CLEANDIRS += src/ide
935
936 uninstall-bin::
937 rm -f $(TOOLDIR)/why3webserver.$(SHAREDBEST)
938
939 install-bin::
940 $(MKDIR_P) $(TOOLDIR)
941 $(INSTALL_DATA) bin/why3webserver.$(SHAREDBEST) $(TOOLDIR)
942
943 install_local:: bin/why3webserver.$(SHAREDBEST)
944
945
946 ###############
947 # Session
948 ###############
949
950 SESSION_FILES = why3session_lib why3session_info \
951 why3session_html why3session_latex why3session_update \
952 why3session_output why3session_create why3session_main
953 # TODO: why3session_copy why3session_rm why3session_csv why3session_run
954 # why3session_output
955
956 SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
957
958 SESSIONDEP = $(addsuffix .dep, $(SESSIONMODULES))
959 SESSIONCMO = $(addsuffix .cmo, $(SESSIONMODULES))
960 SESSIONCMX = $(addsuffix .cmx, $(SESSIONMODULES))
961
962 $(SESSIONDEP) $(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session
963
964 # build targets
965
966 byte: bin/why3session.cma
967 opt: bin/why3session.cmxs
968
969 bin/why3session.cmxs: $(SESSIONCMX)
970 bin/why3session.cma: $(SESSIONCMO)
971
972 # depend and clean targets
973
974 MAKEINC += $(SESSIONDEP)
975
976 CLEANDIRS += src/why3session
977
978 uninstall-bin::
979 rm -f $(TOOLDIR)/why3session.$(SHAREDBEST)
980
981 install-bin::
982 $(MKDIR_P) $(TOOLDIR)
983 $(INSTALL_DATA) bin/why3session.$(SHAREDBEST) $(TOOLDIR)
984
985 install_local:: bin/why3session.$(SHAREDBEST)
986
987 ###############
988 # Why3 Shell
989 ###############
990
991 SHELL_FILES = why3shell
992
993 SHELLMODULES = $(addprefix src/tools/, $(SHELL_FILES))
994
995 SHELLDEP = $(addsuffix .dep, $(SHELLMODULES))
996 SHELLCMO = $(addsuffix .cmo, $(SHELLMODULES))
997 SHELLCMX = $(addsuffix .cmx, $(SHELLMODULES))
998
999 $(SHELLDEP) $(SHELLCMO) $(SHELLCMX): INCLUDES += -I src/tools
1000
1001 # build targets
1002
1003 byte: bin/why3shell.cma
1004 opt: bin/why3shell.cmxs
1005
1006 bin/why3shell.cmxs: $(SHELLCMX)
1007 bin/why3shell.cma: $(SHELLCMO)
1008
1009 # depend and clean targets
1010
1011 MAKEINC += $(SHELLDEP)
1012
1013 uninstall-bin::
1014 rm -f $(TOOLDIR)/why3shell.$(SHAREDBEST)
1015
1016 install-bin::
1017 $(MKDIR_P) $(TOOLDIR)
1018 $(INSTALL_DATA) bin/why3shell.$(SHAREDBEST) $(TOOLDIR)
1019
1020 install_local:: bin/why3shell.$(SHAREDBEST)
1021
1022 ####################
1023 # Coq realizations
1024 ####################
1025
1026 COQVERSIONSPECIFIC=
1027
1028 COQVERSIONSPECIFICTARGETS=$(addprefix lib/coq/, $(COQVERSIONSPECIFIC))
1029
1030 $(COQVERSIONSPECIFICTARGETS): %: %.@coq_compat_version@
1031 $(CMP_CP)
1032
1033 clean-coq::
1034 rm -f $(COQVERSIONSPECIFICTARGETS)
1035
1036 COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power NumOf
1037 COQLIBS_INT_ALL_FILES = Exponentiation $(COQLIBS_INT_FILES)
1038 COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES))
1039
1040 COQLIBS_BOOL_FILES = Bool
1041 COQLIBS_BOOL = $(addprefix lib/coq/bool/, $(COQLIBS_BOOL_FILES))
1042
1043 ifeq (@enable_coq_fp_libs@,yes)
1044 COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt PowerReal Real RealInfix Square Trigonometry Truncate
1045 else
1046 COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt PowerReal Real RealInfix Square Trigonometry
1047 endif
1048 COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
1049
1050 COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
1051 COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
1052
1053 COQLIBS_SET_FILES = Set Cardinal Fset FsetInduction FsetInt FsetSum SetApp SetAppInt SetImp SetImpInt
1054 COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
1055
1056 COQLIBS_MAP_FILES = Map Const MapExt Occ MapPermut MapInjection
1057 COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES))
1058
1059 COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt NthNoOpt RevAppend Combine Distinct NumOcc Permut
1060 COQLIBS_LIST = $(addprefix lib/coq/list/, $(COQLIBS_LIST_FILES))
1061
1062 COQLIBS_OPTION_FILES = Option
1063 COQLIBS_OPTION = $(addprefix lib/coq/option/, $(COQLIBS_OPTION_FILES))
1064
1065 COQLIBS_BV_FILES = Pow2int BV_Gen
1066 COQLIBS_BV = $(addprefix lib/coq/bv/, $(COQLIBS_BV_FILES))
1067
1068 ifeq (@enable_coq_fp_libs@,yes)
1069 COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
1070 COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
1071 COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
1072
1073 COQLIBS_IEEEFLOAT_FILES = RoundingMode GenericFloat Float32 Float64
1074 COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES))
1075 endif
1076
1077 COQLIBS_FOR_DRIVERS_FILES = ComputerOfEuclideanDivision
1078 COQLIBS_FOR_DRIVERS = $(addprefix lib/coq/for_drivers/, $(COQLIBS_FOR_DRIVERS_FILES))
1079
1080 COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd lib/coq/WellFounded $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_FP) $(COQLIBS_BV) $(COQLIBS_IEEEFLOAT) $(COQLIBS_FOR_DRIVERS)
1081
1082 %.vo: %.v
1083 $(SHOW) 'Coqc $<'
1084 $(HIDE)$(COQC) $(COQFLAGS) -R lib/coq Why3 $<
1085
1086 %.vd: %.v
1087 $(SHOW) 'Coqdep $<'
1088 $(HIDE)$(COQDEP) -R lib/coq Why3 $< $(TOTARGET)
1089
1090 COQV = $(addsuffix .v, $(COQLIBS_FILES))
1091 COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
1092 COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
1093
1094 coq: $(COQVO) drivers/coq-realizations.aux lib/coq/version
1095
1096 clean-coq::
1097 rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES)) lib/coq/version \
1098 $(foreach f,$(COQLIBS_FILES),$(dir $f).$(notdir $f).aux)
1099
1100 drivers/coq-realizations.aux: Makefile
1101 $(SHOW) 'Generate $@'
1102 $(HIDE)(echo "(* generated automatically at compilation time *)"; \
1103 echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \
1104 echo 'theory HighOrd meta "realized_theory" "HighOrd", "" end'; \
1105 echo 'theory WellFounded meta "realized_theory" "WellFounded", "" end'; \
1106 for f in $(COQLIBS_INT_FILES); do \
1107 echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
1108 for f in $(COQLIBS_BOOL_FILES); do \
1109 echo 'theory bool.'"$$f"' meta "realized_theory" "bool.'"$$f"'", "" end'; done; \
1110 for f in $(COQLIBS_REAL_FILES); do \
1111 echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
1112 for f in $(COQLIBS_NUMBER_FILES); do \
1113 echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
1114 for f in $(COQLIBS_SET_FILES); do \
1115 echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
1116 for f in $(COQLIBS_MAP_FILES); do \
1117 echo 'theory map.'"$$f"' meta "realized_theory" "map.'"$$f"'", "" end'; done; \
1118 for f in $(COQLIBS_LIST_FILES); do \
1119 echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
1120 for f in $(COQLIBS_OPTION_FILES); do \
1121 echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
1122 for f in $(COQLIBS_BV_FILES); do \
1123 echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \
1124 for f in $(COQLIBS_IEEEFLOAT_FILES); do \
1125 echo 'theory ieee_float.'"$$f"' meta "realized_theory" "ieee_float.'"$$f"'", "" end'; done; \
1126 for f in $(COQLIBS_FP_FILES); do \
1127 echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
1128 for f in $(COQLIBS_FOR_DRIVERS_FILES); do \
1129 echo 'theory for_drivers.'"$$f"' meta "realized_theory" "for_drivers.'"$$f"'", "" end'; done; \
1130 ) > $@
1131
1132 update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-bv update-coq-ieee_float update-coq-for-drivers
1133
1134 LOCAL_STDLIB=-L stdlib --no-stdlib --no-load-default-plugins
1135
1136 update-coq-int: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/int.mlw
1137 for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T int.$$f -o $(GENERATED_PREFIX_COQ)/int/; done
1138
1139 update-coq-bool: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/bool.mlw
1140 for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T bool.$$f -o $(GENERATED_PREFIX_COQ)/bool/; done
1141
1142 update-coq-real: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/real.mlw
1143 for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T real.$$f -o $(GENERATED_PREFIX_COQ)/real/; done
1144
1145 update-coq-number: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/number.mlw
1146 for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T number.$$f -o $(GENERATED_PREFIX_COQ)/number/; done
1147
1148 update-coq-set: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/set.mlw
1149 for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T set.$$f -o $(GENERATED_PREFIX_COQ)/set/; done
1150
1151 update-coq-map: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/map.mlw
1152 for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T map.$$f -o $(GENERATED_PREFIX_COQ)/map/; done
1153
1154 update-coq-list: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/list.mlw
1155 for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T list.$$f -o $(GENERATED_PREFIX_COQ)/list/; done
1156
1157 update-coq-option: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/option.mlw
1158 for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T option.$$f -o $(GENERATED_PREFIX_COQ)/option/; done
1159
1160 update-coq-bv: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/bv.mlw
1161 for f in $(COQLIBS_BV_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T bv.$$f -o $(GENERATED_PREFIX_COQ)/bv/; done
1162
1163 update-coq-for-drivers: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/for_drivers.mlw
1164 for f in $(COQLIBS_FOR_DRIVERS_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T for_drivers.$$f -o $(GENERATED_PREFIX_COQ)/for_drivers/; done
1165
1166 update-coq-ieee_float: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/ieee_float.mlw
1167 for f in $(COQLIBS_IEEEFLOAT_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T ieee_float.$$f -o $(GENERATED_PREFIX_COQ)/ieee_float/; done
1168
1169 update-coq-fp: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/floating_point.mlw
1170 for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T floating_point.$$f -o $(GENERATED_PREFIX_COQ)/floating_point/; done
1171
1172 ifeq (@enable_coq_libs@,yes)
1173
1174 uninstall-coq:
1175 rm -rf $(LIBDIR)/why3/coq
1176
1177 install-coq:
1178 $(MKDIR_P) $(LIBDIR)/why3/coq
1179 $(INSTALL_DATA) lib/coq/version $(LIBDIR)/why3/coq/
1180 $(INSTALL_DATA) lib/coq/BuiltIn.vo lib/coq/HighOrd.vo lib/coq/WellFounded.vo $(LIBDIR)/why3/coq/
1181 $(MKDIR_P) $(LIBDIR)/why3/coq/int
1182 $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/
1183 $(MKDIR_P) $(LIBDIR)/why3/coq/bool
1184 $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_BOOL)) $(LIBDIR)/why3/coq/bool/
1185 $(MKDIR_P) $(LIBDIR)/why3/coq/real
1186 $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
1187 $(MKDIR_P) $(LIBDIR)/why3/coq/number
1188 $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_NUMBER)) $(LIBDIR)/why3/coq/number/
1189 $(MKDIR_P) $(LIBDIR)/why3/coq/set
1190 $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_SET)) $(LIBDIR)/why3/coq/set/
1191 $(MKDIR_P) $(LIBDIR)/why3/coq/map
1192 $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_MAP)) $(LIBDIR)/why3/coq/map/
1193 $(MKDIR_P) $(LIBDIR)/why3/coq/list
1194 $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_LIST)) $(LIBDIR)/why3/coq/list/
1195 $(MKDIR_P) $(LIBDIR)/why3/coq/option
1196 $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_OPTION)) $(LIBDIR)/why3/coq/option/
1197 $(MKDIR_P) $(LIBDIR)/why3/coq/bv
1198 $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_BV)) $(LIBDIR)/why3/coq/bv/
1199 ifeq (@enable_coq_fp_libs@,yes)
1200 $(MKDIR_P) $(LIBDIR)/why3/coq/floating_point
1201 $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
1202 $(MKDIR_P) $(LIBDIR)/why3/coq/ieee_float
1203 $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_IEEEFLOAT)) $(LIBDIR)/why3/coq/ieee_float/
1204 endif
1205 $(MKDIR_P) $(LIBDIR)/why3/coq/for_drivers
1206 $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_FOR_DRIVERS)) $(LIBDIR)/why3/coq/for_drivers/
1207 $(MKDIR_P) $(DATADIR)/why3/drivers
1208 $(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
1209
1210 install:: install-coq
1211
1212 all: coq
1213
1214 ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq"
1215 MAKEINC += $(COQVD)
1216 endif
1217
1218 endif
1219
1220 install-data::
1221 $(MKDIR_P) $(DATADIR)/why3/drivers
1222 $(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
1223
1224 all: drivers/coq-realizations.aux
1225
1226 clean:: clean-coq
1227 rm -f drivers/coq-realizations.aux
1228
1229 ####################
1230 # PVS realizations
1231 ####################
1232
1233 PVSLIBS_INT_FILES = Int Abs MinMax ComputerDivision EuclideanDivision
1234 PVSLIBS_INT = $(addprefix lib/pvs/int/, $(PVSLIBS_INT_FILES))
1235
1236 PVSLIBS_REAL_FILES = Abs FromInt MinMax Real Square ExpLog Trigonometry \
1237 PowerInt
1238 # RealInfix
1239 PVSLIBS_REAL = $(addprefix lib/pvs/real/, $(PVSLIBS_REAL_FILES))
1240
1241 PVSLIBS_LIST_FILES =
1242 # Nth
1243 PVSLIBS_LIST = $(addprefix lib/pvs/int/, $(PVSLIBS_LIST_FILES))
1244
1245 PVSLIBS_NUMBER_FILES = # Divisibility Gcd Parity Prime
1246 PVSLIBS_NUMBER = $(addprefix lib/pvs/number/, $(PVSLIBS_NUMBER_FILES))
1247
1248 PVSLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
1249 PVSLIBS_FP_ALL_FILES = $(PVSLIBS_FP_FILES)
1250 PVSLIBS_FP = $(addprefix lib/pvs/floating_point/, $(PVSLIBS_FP_ALL_FILES))
1251
1252 PVSLIBS_FILES = $(PVSLIBS_INT) $(PVSLIBS_REAL) $(PVSLIBS_LIST) \
1253 $(PVSLIBS_NUMBER) $(PVSLIBS_FP)
1254
1255 update-pvs: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/pvs-realizations.aux
1256 for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D pvs-realize -T int.$$f -o lib/pvs/int/; done
1257 for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D pvs-realize -T real.$$f -o lib/pvs/real/; done
1258 for f in $(PVSLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D pvs-realize -T list.$$f -o lib/pvs/list/; done
1259 for f in $(PVSLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D pvs-realize -T number.$$f -o lib/pvs/number/; done
1260 for f in $(PVSLIBS_FP_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D pvs-realize -T floating_point.$$f -o lib/pvs/floating_point/; done
1261
1262 drivers/pvs-realizations.aux: Makefile
1263 $(SHOW) 'Generate $@'
1264 $(HIDE)(echo "(* generated automatically at compilation time *)"; \
1265 for f in $(PVSLIBS_INT_FILES); do \
1266 echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
1267 for f in $(PVSLIBS_REAL_FILES); do \
1268 echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
1269 for f in $(PVSLIBS_LIST_FILES); do \
1270 echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
1271 for f in $(PVSLIBS_NUMBER_FILES); do \
1272 echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
1273 for f in $(PVSLIBS_FP_FILES); do \
1274 echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
1275 ) > $@
1276
1277 pvs: lib/pvs/version
1278
1279 clean-pvs:
1280 rm -f lib/pvs/version
1281
1282 ifeq (@enable_pvs_libs@,yes)
1283
1284 uninstall-pvs:
1285 rm -rf $(LIBDIR)/why3/pvs
1286
1287 install-pvs:
1288 $(MKDIR_P) $(LIBDIR)/why3/pvs
1289 $(INSTALL_DATA) lib/pvs/version $(LIBDIR)/why3/pvs/
1290 $(MKDIR_P) $(LIBDIR)/why3/pvs/int
1291 $(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_INT)) $(LIBDIR)/why3/pvs/int/
1292 $(INSTALL_DATA) $(addsuffix .prf, $(PVSLIBS_INT)) $(LIBDIR)/why3/pvs/int/
1293 $(MKDIR_P) $(LIBDIR)/why3/pvs/real
1294 $(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_REAL)) $(LIBDIR)/why3/pvs/real/
1295 $(INSTALL_DATA) $(addsuffix .prf, $(PVSLIBS_REAL)) $(LIBDIR)/why3/pvs/real/
1296 $(MKDIR_P) $(LIBDIR)/why3/pvs/floating_point/
1297 $(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_FP)) $(LIBDIR)/why3/pvs/floating_point/
1298 $(MKDIR_P) $(DATADIR)/why3/drivers/
1299 $(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
1300
1301 install:: install-pvs
1302
1303 all: pvs
1304
1305 endif
1306
1307 install-data::
1308 $(MKDIR_P) $(DATADIR)/why3/drivers/
1309 $(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
1310
1311 all: drivers/pvs-realizations.aux
1312
1313 clean:: clean-pvs
1314 rm -f drivers/pvs-realizations.aux
1315
1316 #######################
1317 # Isabelle realizations
1318 #######################
1319
1320
1321 ISABELLEVERSIONSPECIFIC=ROOT why3.ML Why3_BV.thy Why3_Map.thy
1322
1323 ISABELLEVERSIONSPECIFICTARGETS=$(addprefix lib/isabelle/, $(ISABELLEVERSIONSPECIFIC))
1324
1325 ISABELLEREALIZEDRV=isabelle-realize
1326 ISABELLEREALIZEDRVPATH=drivers/$(ISABELLEREALIZEDRV).drv
1327
1328 $(ISABELLEVERSIONSPECIFICTARGETS): %: %.@ISABELLEVERSION@
1329 $(CMP_CP)
1330
1331 clean-isabelle::
1332 rm -f $(ISABELLEVERSIONSPECIFICTARGETS)
1333
1334 ISABELLELIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
1335 ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/int/, $(ISABELLELIBS_INT_FILES)))
1336
1337 ISABELLELIBS_BOOL_FILES = Bool
1338 ISABELLELIBS_BOOL = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/bool/, $(ISABELLELIBS_BOOL_FILES)))
1339
1340 ISABELLELIBS_REAL_FILES = Real RealInfix Abs MinMax FromInt Truncate Square ExpLog Trigonometry PowerInt # not yet realized : PowerReal Hyperbolic Polar
1341 ISABELLELIBS_REAL = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/real/, $(ISABELLELIBS_REAL_FILES)))
1342
1343 ISABELLELIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
1344 ISABELLELIBS_NUMBER = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/number/, $(ISABELLELIBS_NUMBER_FILES)))
1345
1346 ISABELLELIBS_SET_FILES = Set Fset
1347 ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/set/, $(ISABELLELIBS_SET_FILES)))
1348
1349 ISABELLELIBS_MAP_FILES = Map Const Occ MapPermut MapInjection
1350 ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/map/, $(ISABELLELIBS_MAP_FILES)))
1351
1352 ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt RevAppend Combine Distinct NumOcc Permut
1353 ISABELLELIBS_LIST = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/list/, $(ISABELLELIBS_LIST_FILES)))
1354
1355 ISABELLELIBS_BV_FILES = Pow2int
1356 # BV8 BV16 BV32 BV64 BVConverter_32_64 BVConverter_16_64 BVConverter_8_64 BVConverter_16_32 BVConverter_8_32 BVConverter_8_16
1357 ISABELLELIBS_BV = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/bv/, $(ISABELLELIBS_BV_FILES)))
1358
1359 ISABELLELIBS = $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
1360
1361 drivers/isabelle-realizations.aux: Makefile
1362 $(SHOW) 'Generate $@'
1363 $(HIDE)(echo "(* generated automatically at compilation time *)"; \
1364 echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \
1365 for f in $(ISABELLELIBS_INT_FILES); do \
1366 echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
1367 for f in $(ISABELLELIBS_BOOL_FILES); do \
1368 echo 'theory bool.'"$$f"' meta "realized_theory" "bool.'"$$f"'", "" end'; done; \
1369 for f in $(ISABELLELIBS_REAL_FILES); do \
1370 echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
1371 for f in $(ISABELLELIBS_NUMBER_FILES); do \
1372 echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
1373 for f in $(ISABELLELIBS_SET_FILES); do \
1374 echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
1375 for f in $(ISABELLELIBS_MAP_FILES); do \
1376 echo 'theory map.'"$$f"' meta "realized_theory" "map.'"$$f"'", "" end'; done; \
1377 for f in $(ISABELLELIBS_LIST_FILES); do \
1378 echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
1379 for f in $(ISABELLELIBS_OPTION_FILES); do \
1380 echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
1381 for f in $(ISABELLELIBS_BV_FILES); do \
1382 echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \
1383 ) > $@
1384
1385 ifeq (@enable_local@,yes)
1386 ISABELLE_TARGET_DIR=`pwd`/lib/isabelle
1387 else
1388 ISABELLE_TARGET_DIR=$(LIBDIR)/why3/isabelle
1389 endif
1390
1391 $(GENERATED_PREFIX_ISABELLE)/realizations: $(ISABELLELIBS)
1392 $(HIDE)sha1sum $^ | sed -e "s,$(GENERATED_PREFIX_ISABELLE)/,," > $@
1393
1394 update-isabelle: $(GENERATED_PREFIX_ISABELLE)/realizations
1395
1396 $(ISABELLELIBS_INT): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1397 $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/int.mlw
1398 $(SHOW) "Generating Isabelle realization for int.$(notdir $(basename $@))"
1399 $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/int
1400 $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/int/
1401
1402 $(ISABELLELIBS_BOOL): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1403 $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/bool.mlw
1404 $(SHOW) "Generating Isabelle realization for bool.$(notdir $(basename $@))"
1405 $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/bool
1406 $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bool/
1407
1408 $(ISABELLELIBS_REAL): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1409 $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/real.mlw
1410 $(SHOW) "Generating Isabelle realization for real.$(notdir $(basename $@))"
1411 $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/real
1412 $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/real/
1413
1414 $(ISABELLELIBS_NUMBER): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1415 $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/number.mlw
1416 $(SHOW) "Generating Isabelle realization for number.$(notdir $(basename $@))"
1417 $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/number
1418 $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/number/
1419
1420 $(ISABELLELIBS_SET): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1421 $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/set.mlw
1422 $(SHOW) "Generating Isabelle realization for set.$(notdir $(basename $@))"
1423 $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/set
1424 $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/set/
1425
1426 $(ISABELLELIBS_MAP): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1427 $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/map.mlw
1428 $(SHOW) "Generating Isabelle realization for map.$(notdir $(basename $@))"
1429 $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/map
1430 $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/map/
1431
1432 $(ISABELLELIBS_LIST): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1433 $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/list.mlw
1434 $(SHOW) "Generating Isabelle realization for list.$(notdir $(basename $@))"
1435 $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/list
1436 $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/list/
1437
1438 $(ISABELLELIBS_OPTION): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1439 $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/option.mlw
1440 $(SHOW) "Generating Isabelle realization for option.$(notdir $(basename $@))"
1441 $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/option
1442 $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/option/
1443
1444 $(ISABELLELIBS_BV): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1445 $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/bv.mlw
1446 $(SHOW) "Generating Isabelle realization for bv.$(notdir $(basename $@))"
1447 $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/bv
1448 $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bv/
1449
1450 ifeq (@enable_isabelle_libs@,yes)
1451
1452 $(GENERATED_PREFIX_ISABELLE)/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(ISABELLELIBS)
1453 ifneq (@enable_local@,yes)
1454 cp -r $(GENERATED_PREFIX_ISABELLE) "$(LIBDIR)/why3"
1455 endif
1456 @(if isabelle components -l | grep -q "$(ISABELLE_TARGET_DIR)$$"; then \
1457 echo "Building the Why3 heap for Isabelle/HOL:"; \
1458 isabelle build -bc Why3; \
1459 touch $@; \
1460 else \
1461 echo "[Warning] Cannot pre-build the Isabelle heap because"; \
1462 echo " the Isabelle component configuration does not contain"; \
1463 echo " [$(ISABELLE_TARGET_DIR)]"; \
1464 fi)
1465
1466 install-isabelle: $(GENERATED_PREFIX_ISABELLE)/last_build
1467
1468 install_local:: install-isabelle
1469 install:: install-isabelle
1470
1471 endif
1472
1473 all: drivers/isabelle-realizations.aux
1474
1475 install-data::
1476 $(INSTALL_DATA) drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/
1477
1478 clean-isabelle::
1479 rm -f $(GENERATED_PREFIX_ISABELLE)/*/*.xml
1480
1481 clean:: clean-isabelle
1482 rm -f drivers/isabelle-realizations.aux
1483
1484 #######################
1485 # Isabelle client
1486 #######################
1487
1488 ISABELLEC_FILES := isabelle_client_main
1489
1490 ISABELLECMODULES := $(addprefix src/isabelle-client/, $(ISABELLEC_FILES))
1491 ISABELLECDEP = $(addsuffix .dep, $(ISABELLECMODULES))
1492 ISABELLECCMO = $(addsuffix .cmo, $(ISABELLECMODULES))
1493 ISABELLECCMX = $(addsuffix .cmx, $(ISABELLECMODULES))
1494
1495 $(ISABELLECDEP) $(ISABELLECCMO) $(ISABELLECCMX): INCLUDES += -I src/isabelle-client -I src/util
1496
1497 depend: $(ISABELLECDEP)
1498 CLEANDIRS += src/isabelle-client
1499
1500 # build targets
1501
1502 byte: bin/isabelle_client.byte
1503 opt: bin/isabelle_client.opt
1504
1505 bin/isabelle_client.opt: lib/why3/why3.cmxa $(ISABELLECCMX)
1506
1507 bin/isabelle_client.byte: lib/why3/why3.cma $(ISABELLECCMO)
1508
1509 install-bin::
1510 cp -f bin/isabelle_client.@OCAMLBEST@ $(BINDIR)/isabelle_client$(EXE)
1511
1512 uninstall-bin::
1513 rm -f $(BINDIR)/isabelle_client$(EXE)
1514
1515 MAKEINC += $(ISABELLECDEP)
1516
1517 clean::
1518 rm -f bin/isabelle_client.byte bin/isabelle_client.opt bin/isabelle_client
1519
1520 ################
1521 # Jessie3 plugin
1522 ################
1523
1524 ifeq (@enable_frama_c@,yes)
1525
1526 nobyte: jessie.byte
1527 noopt: jessie.opt
1528
1529 jessie.byte: src/jessie/Makefile $(WHY3CMA)
1530 @$(MAKE) -C src/jessie Jessie3.cma
1531
1532 jessie.opt: src/jessie/Makefile $(WHY3CMXA)
1533 @$(MAKE) -C src/jessie Jessie3.cmxs
1534
1535 uninstall-framac:
1536 rm -f $(FRAMAC_LIBDIR)/plugins/Jessie3.*
1537
1538 uninstall:: uninstall-framac
1539
1540 install-framac:
1541 $(MKDIR_P) $(FRAMAC_LIBDIR)/plugins/
1542 $(INSTALL_DATA) $(wildcard $(addprefix src/jessie/Jessie3., $(INSTALLED_LIB_EXTS))) \
1543 $(FRAMAC_LIBDIR)/plugins/
1544
1545 install:: install-framac
1546
1547 clean::
1548 $(MAKE) -C src/jessie clean
1549
1550 endif
1551
1552 ###############
1553 # Why3 pp
1554 ###############
1555
1556 PRETTYPRINT_FILES = why3pp
1557
1558 PRETTYPRINTMODULES = $(addprefix src/tools/, $(PRETTYPRINT_FILES))
1559
1560 PRETTYPRINTDEP = $(addsuffix .dep, $(PRETTYPRINTMODULES))
1561 PRETTYPRINTCMO = $(addsuffix .cmo, $(PRETTYPRINTMODULES))
1562 PRETTYPRINTCMX = $(addsuffix .cmx, $(PRETTYPRINTMODULES))
1563
1564 $(PRETTYPRINTDEP) $(PRETTYPRINTCMO) $(PRETTYPRINTCMX): INCLUDES += -I src/tools
1565
1566 # build targets
1567
1568 byte: bin/why3pp.cma
1569 opt: bin/why3pp.cmxs
1570
1571 bin/why3pp.cmxs: $(PRETTYPRINTCMX)
1572 bin/why3pp.cma: $(PRETTYPRINTCMO)
1573
1574 # depend and clean targets
1575
1576 MAKEINC += $(PRETTYPRINTDEP)
1577
1578 uninstall-bin::
1579 rm -f $(TOOLDIR)/why3pp.$(SHAREDBEST)
1580
1581 install-bin::
1582 $(MKDIR_P) $(TOOLDIR)
1583 $(INSTALL_DATA) bin/why3pp.$(SHAREDBEST) $(TOOLDIR)
1584
1585 install_local:: bin/why3pp.$(SHAREDBEST)
1586
1587 #########
1588 # why3doc
1589 #########
1590
1591 WHY3DOCGENERATED = src/why3doc/doc_lexer.ml
1592
1593 WHY3DOC_FILES = doc_html doc_def doc_lexer doc_main
1594
1595 WHY3DOCMODULES = $(addprefix src/why3doc/, $(WHY3DOC_FILES))
1596
1597 WHY3DOCDEP = $(addsuffix .dep, $(WHY3DOCMODULES))
1598 WHY3DOCCMO = $(addsuffix .cmo, $(WHY3DOCMODULES))
1599 WHY3DOCCMX = $(addsuffix .cmx, $(WHY3DOCMODULES))
1600
1601 $(WHY3DOCDEP) $(WHY3DOCCMO) $(WHY3DOCCMX): INCLUDES += -I src/why3doc
1602
1603 $(WHY3DOCDEP): $(WHY3DOCGENERATED)
1604
1605 # build targets
1606
1607 byte: bin/why3doc.cma
1608 opt: bin/why3doc.cmxs
1609
1610 bin/why3doc.cmxs: $(WHY3DOCCMX)
1611 bin/why3doc.cma: $(WHY3DOCCMO)
1612
1613 # depend and clean targets
1614
1615 MAKEINC += $(WHY3DOCDEP)
1616
1617 CLEANDIRS += src/why3doc
1618 GENERATED += $(WHY3DOCGENERATED)
1619
1620 uninstall-bin::
1621 rm -f $(TOOLDIR)/why3doc.$(SHAREDBEST)
1622
1623 install-bin::
1624 $(MKDIR_P) $(TOOLDIR)
1625 $(INSTALL_DATA) bin/why3doc.$(SHAREDBEST) $(TOOLDIR)
1626
1627 install_local:: bin/why3doc.$(SHAREDBEST)
1628
1629 #########
1630 # trywhy3
1631 #########
1632
1633 ifeq ($(DEBUGJS),yes)
1634 JSOO_DEBUG=--pretty --debug-info --source-map
1635 JS_MAPS=trywhy3.map why3_worker.map
1636 else
1637 JSOO_DEBUG=
1638 JS_MAPS=
1639 endif
1640
1641 TRYWHY3_FILES = json_base json_parser json_lexer bindings shortener trywhy3 why3_worker worker_proto
1642
1643 TRYWHY3MODULES = $(addprefix src/trywhy3/, $(TRYWHY3_FILES))
1644
1645 TRYWHY3DEP = $(addsuffix .dep, $(TRYWHY3MODULES))
1646 TRYWHY3CMO = $(addsuffix .cmo, $(TRYWHY3MODULES))
1647 TRYWHY3CMI = $(addsuffix .cmi, $(TRYWHY3MODULES))
1648
1649 $(TRYWHY3DEP) $(TRYWHY3CMO) $(TRYWHY3CMI): INCLUDES += -I src/trywhy3
1650
1651 TRYWHY3_COMMON_PACK = \
1652 trywhy3.js trywhy3.html trywhy3.css trywhy3_custom.css \
1653 help_whyml.html help_python.html help_micro-C.html \
1654 why3_worker.js \
1655 examples/ \
1656 $(JS_MAPS)
1657
1658 TRYWHY3_SMALL_PACK = \
1659 $(TRYWHY3_COMMON_PACK) \
1660 mode-why3.js
1661
1662 TRYWHY3_FULL_PACK = \
1663 $(TRYWHY3_COMMON_PACK) \
1664 alt-ergo-worker.js \
1665 ace-builds/src-min-noconflict/ace.js \
1666 ace-builds/src-min-noconflict/mode-why3.js \
1667 ace-builds/src-min-noconflict/mode-python.js \
1668 ace-builds/src-min-noconflict/mode-c_cpp.js \
1669 ace-builds/src-min-noconflict/theme-chrome.js
1670
1671 trywhy3.tar.gz: $(addprefix src/trywhy3/, $(TRYWHY3_SMALL_PACK))
1672 tar czf $@ -C src $(addprefix trywhy3/, $(TRYWHY3_SMALL_PACK))
1673
1674 trywhy3-full.tar.gz: $(addprefix src/trywhy3/, $(TRYWHY3_FULL_PACK))
1675 tar czf $@ -C src $(addprefix trywhy3/, $(TRYWHY3_FULL_PACK))
1676
1677 trywhy3: src/trywhy3/trywhy3.js src/trywhy3/why3_worker.js
1678
1679 src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
1680 js_of_ocaml $(JSOO_DEBUG) --Werror $<
1681
1682 src/trywhy3/trywhy3.byte: $(addprefix src/trywhy3/, json_base.cmo json_parser.cmo json_lexer.cmo bindings.cmo worker_proto.cmo shortener.cmo trywhy3.cmo)
1683 $(OCAMLFIND) ocamlc -o $@ -package js_of_ocaml -package menhirLib -linkpkg $^
1684
1685 src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte src/trywhy3/trywhy3.conf src/trywhy3/try_alt_ergo.drv
1686 js_of_ocaml $(JSOO_DEBUG) --Werror --extern-fs -I . -I src/trywhy3 \
1687 --file=trywhy3.conf:/ \
1688 --file=try_alt_ergo.drv:/ \
1689 `find stdlib -name "*.mlw" -exec printf " --file=%s:/%s" {} {} ";"` \
1690 +dynlink.js +toplevel.js +zarith_stubs_js/biginteger.js +zarith_stubs_js/runtime.js $< || rm -f $@
1691
1692 src/trywhy3/why3_worker.byte: $(WHY3CMA) $(PYTHONCMO) $(MICROCCMO) \
1693 $(addprefix src/trywhy3/, bindings.cmo worker_proto.cmo why3_worker.cmo)
1694 $(OCAMLFIND) ocamlc $(filter-out -thread,$(BFLAGS)) -package js_of_ocaml -o $@ -linkpkg $^
1695
1696 src/trywhy3/%.cmo: src/trywhy3/%.ml
1697 $(OCAMLFIND) ocamlc $(BFLAGS) -c $<
1698
1699 src/trywhy3/%.cmi: src/trywhy3/%.mli
1700 $(OCAMLFIND) ocamlc $(BFLAGS) -c $<
1701
1702 $(addprefix src/trywhy3/, worker_proto.cmo why3_worker.cmo): BFLAGS += -package js_of_ocaml
1703
1704 $(addprefix src/trywhy3/, bindings.cmo trywhy3.cmo): BFLAGS += -package js_of_ocaml -package js_of_ocaml-ppx
1705
1706 TRYWHY3JSON_FILES = json_base json_parser json_lexer
1707 TRYWHY3JSON = $(TRYWHY3JSON_FILES:%=src/trywhy3/%.ml) $(TRYWHY3JSON_FILES:%=src/trywhy3/%.mli)
1708
1709 $(TRYWHY3JSON): src/trywhy3/%: src/util/%
1710 cp $< $@
1711
1712 GENERATED += $(TRYWHY3JSON)
1713
1714 $(TRYWHY3DEP): $(TRYWHY3JSON)
1715
1716 MAKEINC += $(TRYWHY3DEP)
1717
1718 clean-trywhy3:
1719 rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte \
1720 src/trywhy3/why3_worker.js src/trywhy3/why3_worker.byte \
1721 trywhy3.tar.gz
1722
1723 clean:: clean-trywhy3
1724
1725 CLEANDIRS += src/trywhy3
1726
1727
1728 #########
1729 # why3webserver and full web/js interface
1730 #########
1731
1732 ifeq (@enable_web_ide@,yes)
1733
1734 JSOCAMLCW=$(OCAMLFIND) ocamlc -package js_of_ocaml -package js_of_ocaml-ppx \
1735 -I src/ide
1736
1737 src/ide/why3_js.cmo: src/ide/why3_js.ml lib/why3/why3.cma
1738 $(JSOCAMLCW) $(BFLAGS) -c $<
1739
1740 src/ide/why3_js.byte: lib/why3/why3.cma src/ide/why3_js.cmo
1741 $(JSOCAMLCW) $(filter-out -thread,$(BFLAGS)) -o $@ -linkpkg $(BLINKFLAGS) $^
1742
1743 src/ide/why3_js.js: src/ide/why3_js.byte
1744 js_of_ocaml --Werror +dynlink.js +toplevel.js +zarith_stubs_js/biginteger.js +zarith_stubs_js/runtime.js $< || rm -f $@
1745
1746 web_ide: src/ide/why3_js.js
1747
1748 opt: bin/why3webserver.cmxs
1749 byte: bin/why3webserver.cma src/ide/why3_js.cmo
1750
1751 endif
1752
1753 ########
1754 # bench
1755 ########
1756
1757 .PHONY: bench test
1758
1759 bench:: bin/why3.@OCAMLBEST@ bin/why3config.$(SHAREDBEST) plugins $(TOOLS) \
1760 share/Makefile.config bin/why3extract.$(SHAREDBEST)
1761 bin/why3.@OCAMLBEST@ config list-provers | grep -q Alt-Ergo || \
1762 bin/why3.@OCAMLBEST@ config detect
1763 @echo "=== Check API examples ==="
1764 $(MAKE) bench-api
1765 @echo "=== Check examples ==="
1766 bash bench/bench -suffix ".@OCAMLBEST@"
1767 @echo "=== Check parsing messages ==="
1768 bench/parsing-bench
1769
1770 APITESTS = \
1771 clone \
1772 counterexample \
1773 create_session \
1774 logic \
1775 mlw_expr \
1776 mlw_tree \
1777 transform
1778
1779 ifeq (@enable_infer@,yes)
1780 APITESTS += mlw_tree_infer_invs
1781 endif
1782
1783 ifeq (@enable_infer@,yes)
1784 APITESTS += mlw_tree_bddinfer_invs
1785 endif
1786
1787 ifeq (@enable_sexp@,yes)
1788 APITESTS += epsilon
1789 endif
1790
1791 bench-api: $(addprefix test-api-, $(APITESTS))
1792
1793 clean::
1794 rm -rf bench/infer/*.out
1795 rm -rf bench/bddinfer/*.out
1796 rm -rf bench/check-ce/*.out
1797
1798 ###############
1799 # test targets
1800 ###############
1801
1802 test-itp.opt: src/printer/itp.ml lib/why3/why3.cmxa
1803 $(if $(QUIET),@echo 'Ocamlopt $<' &&) \
1804 $(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(OLINKFLAGS) lib/why3/why3.cmxa $<
1805
1806 test-api-%.byte: examples/use_api/%.ml lib/why3/why3.cma
1807 $(SHOW) 'Ocaml $<'
1808 $(HIDE)($(OCAMLC) -o $@ -I lib/why3 $(BFLAGS) $(BLINKFLAGS) lib/why3/why3.cma $<) \
1809 || (printf "Compilation failed for API test $@. Please fix it.\n"; exit 2)
1810
1811 test-api-%.opt: examples/use_api/%.ml lib/why3/why3.cmxa
1812 $(SHOW) 'Ocamlopt $<'
1813 $(HIDE)($(OCAMLOPT) -o $@ -I lib/why3 $(OFLAGS) $(OLINKFLAGS) lib/why3/why3.cmxa $<) \
1814 || (printf "Compilation failed for API test $@. Please fix it.\n"; exit 2)
1815
1816 test-api-%: test-api-%.@OCAMLBEST@
1817 $(HIDE)mkdir -p examples/use_api/results
1818 $(HIDE)(./$< | sed -e 's/^\(Versions of Alt-Ergo found: \).*$$/\1<hidden>/' \
1819 -e 's/0\.0[0-9]/<hidden>/g;s/[0-9]\+ steps/<hidden> steps/' \
1820 > examples/use_api/results/$@.stdout ) \
1821 || (printf "Execution failed for API test $<. Please fix it.\n"; exit 2)
1822 $(HIDE)(diff -u examples/use_api/oracles/$@.stdout examples/use_api/results/$@.stdout) \
1823 || (printf "Oracle updated for API test $<. Please review it.\n"; cp examples/use_api/results/$@.stdout examples/use_api/oracles/$@.stdout )
1824 $(HIDE)rm -f $< why3session.xml why3shapes why3shapes.gz
1825
1826
1827 #test-shape: lib/why3/why3.cma
1828 # ocaml -I lib/why3 $(INCLUDES) $(BLINKFLAGS) $? examples/test_shape.ml
1829
1830
1831 ################
1832 # documentation
1833 ################
1834
1835 .PHONY: doc predoc update-doc-png clean-doc
1836
1837 doc/generated/drivers-all.dot: drivers/*.drv drivers/*.gen
1838 doc/drv_depgraph $^ > $@
1839
1840 doc/generated/drivers-%.dot: doc/generated/drivers-all.dot
1841 ccomps -X $(NODE) $< > $@
1842
1843 doc/generated/drivers-smt.dot: NODE = smt-libv2.gen
1844 doc/generated/drivers-tptp.dot: NODE = tptp.gen
1845 doc/generated/drivers-coq.dot: NODE = coq-common.gen
1846 doc/generated/drivers-isabelle.dot: NODE = isabelle-common.gen
1847 doc/generated/drivers-pvs.dot: NODE = pvs-common.gen
1848
1849 DRVDOT = $(patsubst %,doc/generated/drivers-%.dot, smt tptp coq isabelle pvs)
1850
1851 DOC = index zebibliography genindex \
1852 foreword starting whyml api install manpages syntaxref vcgen \
1853 input_formats exec itp technical changes
1854
1855 DOCRST = $(DOC:%=doc/%.rst) doc/whyml2java.inc doc/manual.bib
1856
1857 LIBDOT = $(patsubst %,doc/generated/library-%.dot, int array)
1858
1859 doc/generated/library-%.dot: stdlib/%.mlw
1860 bin/why3 pp --output=dep $< | tred > $@
1861
1862 predoc: $(DRVDOT) $(LIBDOT) java-examples
1863
1864 java-examples:
1865 ${MAKE} -C doc/javaexamples all
1866
1867 clean-java-examples:
1868 ${MAKE} -C doc/javaexamples clean
1869
1870 update-doc-png:
1871 export UBUNTU_MENUPROXY=0; \
1872 export WHY3CONFIG=doc/why3ide-doc.conf; \
1873 export WHY3LOADPATH=stdlib; \
1874 export GTK_THEME=Adwaita; \
1875 export WAYLAND_DISPLAY=; \
1876 sed -n -e 's/^.. %EXECUTE \(.*\)/\1/p' $(DOCRST) | $(SHELL) -e
1877
1878 ifeq (@enable_doc@,yes)
1879
1880 doc: doc/html/index.html
1881
1882 TESTSAPIDOC = $(addsuffix .ml, $(addprefix examples/use_api/, $(APITESTS)))
1883
1884 doc/html/index.html: $(DOCRST) $(DRVDOT) $(LIBDOT) $(TESTSAPIDOC) java-examples doc/conf.py
1885 $(SPHINX) -b html -d doc/.doctrees doc doc/html
1886
1887 doc/latex/manual.tex: $(DOCRST) $(DRVDOT) $(LIBDOT) $(TESTSAPIDOC) java-examples doc/conf.py
1888 $(SPHINX) -b latex -d doc/.doctrees doc doc/latex
1889
1890 ifeq (@enable_pdf_doc@,yes)
1891
1892 doc: doc/latex/manual.pdf
1893
1894 doc/latex/manual.pdf: doc/latex/manual.tex
1895 @echo "running LaTeX compilation..."
1896 cd doc/latex; $(LATEXCOMP) manual.tex >/dev/null
1897 ifeq (@LATEX@,pdflatex)
1898 @cd doc/latex; if grep 'may have changed. Rerun to get' manual.log; then \
1899 makeindex manual; \
1900 echo "running LaTeX again to try to fix references..."; \
1901 pdflatex manual >/dev/null; \
1902 fi
1903 @cd doc/latex; if grep 'may have changed. Rerun to get' manual.log; then \
1904 echo "running LaTeX again to try to fix references..."; \
1905 pdflatex manual >/dev/null; \
1906 fi
1907 endif
1908
1909 endif
1910
1911 else
1912
1913 doc:
1914
1915 endif
1916
1917 clean-doc: clean-java-examples
1918 rm -rf doc/html doc/latex
1919 rm -rf doc/generated/*.dot
1920
1921 clean:: clean-doc
1922
1923 ##########
1924 # API DOC
1925 ##########
1926
1927 .PHONY: apidoc apidot
1928
1929 MODULESTODOC = \
1930 util/util util/opt util/lists util/strings util/getopt \
1931 util/extmap util/extset util/exthtbl \
1932 util/weakhtbl util/wstdlib util/rc util/debug \
1933 util/loc util/pp util/bigInt util/number \
1934 util/mlmpfr_wrapper \
1935 core/ident core/ty core/term core/decl core/coercion core/theory \
1936 core/env core/task core/trans core/pretty core/printer \
1937 core/model_parser \
1938 parser/ptree.ml \
1939 parser/ptree_helpers parser/typing parser/mlw_printer \
1940 driver/whyconf driver/call_provers driver/driver \
1941 transform/args_wrapper \
1942 mlw/ity mlw/expr mlw/pdecl mlw/pmodule mlw/vc \
1943 mlw/pinterp_core mlw/rac mlw/pinterp mlw/check_ce \
1944 session/session_itp session/controller_itp \
1945 session/itp_communication session/itp_server \
1946 session/strategy
1947
1948 ifeq (@enable_bddinfer@,yes)
1949 MODULESTODOC += bddinfer/why3infer
1950 endif
1951
1952 FILESTODOC = $(subst .ml.mli,.ml,$(MODULESTODOC:%=src/%.mli))
1953
1954 DOCFLAGS = -sort $(INCLUDES) $(LIBINCLUDES)
1955
1956 ifeq (@enable_ocamlfind@,yes)
1957 DOCFLAGS += $(addprefix -package ,$(EXTPKGS))
1958 else
1959 DOCFLAGS += $(EXTINCLUDES)
1960 endif
1961
1962 doc/apidoc:
1963 mkdir -p doc/apidoc
1964
1965 apidoc: doc/apidoc $(FILESTODOC)
1966 $(OCAMLDOC) $(DOCFLAGS) -d doc/apidoc -charset utf-8 -html \
1967 -t "Why3 API documentation" -keep-code $(FILESTODOC)
1968
1969 # could we include also the dependency graph ? -- someone
1970 # At least we can give a way to create it -- francois
1971
1972 apidot: doc/apidoc/dg.svg doc/apidoc/dg.png
1973
1974 #The sed remove configuration for dot that gives bad result
1975 doc/apidoc/dg.dot: doc/apidoc $(FILESTODOC)
1976 $(OCAMLDOC) $(DOCFLAGS) -o doc/apidoc/dg.dot.tmp -dot $(FILESTODOC)
1977 sed -e "s/ \(size\|ratio\|rotate\|fontsize\).*$$//" doc/apidoc/dg.dot.tmp \
1978 | tred > doc/apidoc/dg.dot
1979 rm -f doc/apidoc/dg.dot.tmp
1980
1981 doc/apidoc/dg.svg: doc/apidoc/dg.dot
1982 dot -T svg $< > $@
1983
1984 doc/apidoc/dg.png: doc/apidoc/dg.dot
1985 dot -T png $< > $@
1986
1987 doc/apidoc.tex: $(FILESTODOC)
1988 $(OCAMLDOC) $(DOCFLAGS) -o doc/apidoc.tex -latex -noheader -notrailer $(FILESTODOC)
1989
1990 clean::
1991 rm -f doc/apidoc/*
1992
1993 ##########
1994 # Install rules for bash completions
1995 ##########
1996
1997 uninstall-bash:
1998 if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then \
1999 rm -f /etc/bash_completion.d/why3; \
2000 fi
2001
2002 uninstall:: uninstall-bash
2003
2004 install-bash::
2005 if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then \
2006 $(INSTALL) share/bash/why3 /etc/bash_completion.d; \
2007 fi
2008
2009 install:: install-bash
2010
2011 ##########
2012 # Stdlib formatted with why3doc
2013 ##########
2014
2015 .PHONY: stdlibdoc
2016
2017 STDMACHLIBS = \
2018 array bv c float fxp int matrix onetime peano tagset \
2019 java/lang java/util
2020
2021 STDLIBS = \
2022 algebra array \
2023 bag bintree bool bv \
2024 cursor \
2025 exn \
2026 floating_point fmap function \
2027 graph hashtbl \
2028 ieee_float int io \
2029 list \
2030 map matrix \
2031 number \
2032 ocaml option \
2033 pigeon pqueue \
2034 queue \
2035 random real ref regexp relations \
2036 seq set stack string \
2037 tree \
2038 ufloat \
2039 witness \
2040 $(addprefix mach/, $(STDMACHLIBS))
2041
2042 # NO NEED DOC:
2043 # debug: too basic, needs large improvement
2044 # tptp: for TPTP provers ?
2045 # for_drivers: used only in drivers
2046
2047 STDLIBFILES = $(patsubst %,stdlib/%.mlw, $(STDLIBS))
2048
2049 # TODO: remove the hack about int.mlw once it has become builtin
2050 stdlibdoc: $(STDLIBFILES) bin/why3.@OCAMLBEST@ bin/why3doc.$(SHAREDBEST)
2051 mkdir -p doc/stdlibdoc
2052 sed -e "s/use Int/use int.Int/" stdlib/int.mlw > int.mlw
2053 rm -f doc/stdlibdoc/style.css
2054 WHY3CONFIG="" bin/why3.@OCAMLBEST@ doc $(LOCAL_STDLIB) \
2055 -o doc/stdlibdoc --title="Why3 Standard Library" \
2056 $(subst stdlib/int.mlw,int.mlw,$(STDLIBFILES))
2057 rm int.mlw
2058 cd doc/stdlibdoc; \
2059 for f in stdlib.*.html; \
2060 do mv "$$f" "$${f#stdlib.}"; done
2061 sed -i -e "s#stdlib.##g" doc/stdlibdoc/index.html
2062 sed -i -e "s#int\.\(<a href=\"\)int\.html#\1#g" doc/stdlibdoc/int.html
2063
2064 clean::
2065 rm -f doc/stdlibdoc/*
2066
2067 ################
2068 # generic rules
2069 ################
2070
2071 %.cmi: %.mli
2072 $(SHOW) 'Ocamlc $<'
2073 $(HIDE)$(OCAMLC) -c $(BFLAGS) $<
2074
2075 # suppress "unused rec" warning for Menhir-produced files
2076 %.cmo: %.ml %.mly
2077 $(SHOW) 'Ocamlc $<'
2078 $(HIDE)$(OCAMLC) -c $(BFLAGS) -w -39 $<
2079
2080 # suppress "unused rec" warning for Menhir-produced files
2081 %.cmx: %.ml %.mly
2082 $(SHOW) 'Ocamlopt $<'
2083 $(HIDE)$(OCAMLOPT) -c $(OFLAGS) -w -39 $(CMIHACK) $<
2084
2085 %.cmo: %.ml
2086 $(SHOW) 'Ocamlc $<'
2087 $(HIDE)$(OCAMLC) -c $(BFLAGS) $<
2088
2089 %.cmx: %.ml %.mli
2090 $(SHOW) 'Ocamlopt $<'
2091 $(HIDE)$(OCAMLOPT) -c $(OFLAGS) $<
2092
2093 %.cmx: %.ml
2094 $(SHOW) 'Ocamlopt $<'
2095 $(HIDE)$(OCAMLOPT) -c $(OFLAGS) $(CMIHACK) $<
2096
2097 %.cma:
2098 $(SHOW) 'Linking $@'
2099 $(HIDE)$(OCAMLC) -a $(BFLAGS) -o $@ $^
2100
2101 %.cmxa:
2102 $(SHOW) 'Linking $@'
2103 $(HIDE)$(OCAMLOPT) -a $(OFLAGS) -o $@ $^
2104
2105 %.cmxs:
2106 $(SHOW) 'Linking $@'
2107 $(HIDE)$(OCAMLOPT) -shared $(OFLAGS) -o $@ $^
2108
2109 %.ml: %.mll
2110 $(SHOW) 'Ocamllex $<'
2111 $(HIDE)$(OCAMLLEX) $<
2112
2113 # the % below are not a typo; they are a way to force Make to consider all the targets at once
2114 src/c%re/parser_tokens.ml src/c%re/parser_tokens.mli: src/parser/parser_common.mly
2115 $(SHOW) 'Menhir $^'
2116 $(HIDE)$(MENHIR) --base src/core/parser_tokens --only-tokens $^
2117
2118 src/p%rser/parser.ml src/p%rser/parser.mli: $(PARSERS)
2119 $(SHOW) 'Menhir $^'
2120 $(HIDE)$(MENHIR) --table --explain --strict --base src/parser/parser \
2121 --external-tokens Parser_tokens $^
2122
2123 pl%gins/cfg/cfg_parser.ml pl%gins/cfg/cfg_parser.mli: src/parser/parser_common.mly plugins/cfg/cfg_parser.mly
2124 $(SHOW) 'Menhir $^'
2125 $(HIDE)$(MENHIR) --table --explain --strict --base plugins/cfg/cfg_parser $^
2126 $(HIDE)for f in plugins/cfg/cfg_parser.mli plugins/cfg/cfg_parser.ml; do (echo "open Why3"; cat $$f) > $$f.new && mv $$f.new $$f; done
2127
2128 pl%gins/coma/coma_parser.ml pl%gins/coma/coma_parser.mli: src/parser/parser_common.mly plugins/coma/coma_parser.mly
2129 $(SHOW) 'Menhir $^'
2130 $(HIDE)$(MENHIR) --table --explain --strict --base plugins/coma/coma_parser $^
2131 $(HIDE)for f in plugins/coma/coma_parser.mli plugins/coma/coma_parser.ml; do (echo "open Why3"; cat $$f) > $$f.new && mv $$f.new $$f; done
2132
2133 %.ml %.mli: %.mly
2134 $(SHOW) 'Menhir $<'
2135 $(HIDE)$(MENHIR) --table --explain --strict $<
2136
2137 %.dep: %.ml %.mli
2138 $(SHOW) 'Ocamldep $<'
2139 $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(INCLUDES) $< $<i $(TOTARGET)
2140
2141 %.dep: %.ml
2142 $(SHOW) 'Ocamldep $<'
2143 $(HIDE)($(OCAMLDEP) $(DEPFLAGS) $(INCLUDES) $<; \
2144 echo '$*.cmx : $*.cmi'; \
2145 echo '$*.cmi : $*.cmo') $(TOTARGET)
2146
2147 %.dep: %.mli
2148 $(SHOW) 'Ocamldep $<'
2149 $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(INCLUDES) $< $(TOTARGET)
2150
2151 bin/%.opt:
2152 $(SHOW) 'Linking $@'
2153 $(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
2154
2155 bin/%.byte:
2156 $(SHOW) 'Linking $@'
2157 $(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
2158
2159 # .ml4.ml:
2160 # $(CAMLP4) pr_o.cmo -impl $< > $@
2161
2162 # jc/jc_ai.ml: jc/jc_annot_inference.ml jc/jc_annot_fail.ml Makefile
2163 # if test "@enable_apron@" = "yes" ; then \
2164 # echo "# 1 \"jc/jc_annot_inference.ml\"" > jc/jc_ai.ml; \
2165 # cat jc/jc_annot_inference.ml >> jc/jc_ai.ml; \
2166 # else \
2167 # echo "# 1 \"jc/jc_annot_fail.ml\"" > jc/jc_ai.ml; \
2168 # cat jc/jc_annot_fail.ml >> jc/jc_ai.ml; \
2169 # fi
2170
2171 # %_why.v: %.mlw $(BINARY)
2172 # $(BINARY) -coq $*.mlw
2173
2174 # %_why.pvs: %.mlw $(BINARY)
2175 # $(BINARY) -pvs $*.mlw
2176
2177 # Emacs tags
2178 ############
2179
2180 tags:
2181 find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
2182 etags "--regex-ocaml=/let[ \t]+\([^ \t]+\)/\1/" \
2183 "--regex-ocaml=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
2184 "--regex-ocaml=/and[ \t]+\([^ \t]+\)/\1/" \
2185 "--regex-ocaml=/type[ \t]+\([^ \t]+\)/\1/" \
2186 "--regex-ocaml=/exception[ \t]+\([^ \t]+\)/\1/" \
2187 "--regex-ocaml=/val[ \t]+\([^ \t]+\)/\1/" \
2188 "--regex-ocaml=/module[ \t]+\([^ \t]+\)/\1/"
2189
2190 otags:
2191 find \( -name '*.ml' -or -name '*.mli' \) -print0 | xargs -0 otags
2192 # otags src/*.mli src/*.ml c/*.mli c/*.ml intf/*.mli intf/*.ml
2193
2194 # the previous seems broken. This one is intented for vi(m) users, but could
2195 # be adapted for emacs (remove the -vi option ?)
2196 otags-vi:
2197 find \( -name '*.ml' -or -name '*.mli' \) -print0 | xargs -0 otags -vi
2198
2199 wc:
2200 ocamlwc -p src/*.ml* src/*/*.ml*
2201
2202 #dep: depend
2203 # cat .depend* | ocamldot | dot -Tpdf > dep.pdf
2204 # $(PDFVIEWER) dep.pdf
2205
2206 # distrib
2207 #########
2208
2209 NAME = why3-@VERSION@
2210 # see .gitattributes for the list of files that are not distributed
2211 MORE_DIST = configure
2212
2213 dist: $(MORE_DIST)
2214 rm -f distrib/$(NAME).tar.gz
2215 mkdir -p distrib/
2216 git archive --format=tar --prefix=$(NAME)/ -o distrib/$(NAME).tar HEAD
2217 tar rf distrib/$(NAME).tar --transform="s,^,$(NAME)/," --mtime="$$(date -Iseconds -d "`git show -s --format=%ci` +1 second")" --owner=0 --group=0 $(MORE_DIST)
2218 gzip -n -f --best distrib/$(NAME).tar
2219
2220
2221 ###############
2222 # file headers
2223 ###############
2224
2225 headers:
2226 headache -c misc/headache_config.txt -h misc/header.txt \
2227 Makefile.in configure.in \
2228 src/*/*.ml src/*/*.ml[ily] \
2229 plugins/*/*.ml plugins/*/*.ml[ily] \
2230 lib/coq/*.v lib/coq/*/*.v \
2231 src/server/*.[ch] \
2232 examples/use_api/*.ml
2233
2234 #########
2235 # myself
2236 #########
2237
2238 AUTOCONF_FILES = \
2239 Makefile \
2240 src/jessie/Makefile \
2241 src/config.sh \
2242 .merlin \
2243 src/jessie/.merlin \
2244 lib/why3/META \
2245 lib/coq/version \
2246 lib/pvs/version
2247
2248 $(AUTOCONF_FILES): %: %.in config.status
2249 ./config.status chmod --file $@
2250
2251 src/util/config.ml share/Makefile.config: src/config.sh
2252 $(SHOW) 'Generate $@'
2253 $(HIDE)BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
2254
2255 clean::
2256 rm -f share/Makefile.config
2257
2258 config.status: configure
2259 ./config.status --recheck
2260
2261 configure: configure.in
2262 autoconf -f
2263
2264 ###################
2265 # clean and depend
2266 ###################
2267
2268 .PHONY: distclean
2269
2270 distclean: clean
2271 rm -f config.status config.cache config.log \
2272 src/util/config.ml $(AUTOCONF_FILES)
2273
2274 ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
2275 ifneq "$(MAKECMDGOALS)" "depend"
2276 -include $(MAKEINC)
2277 endif
2278 endif
2279
2280 depend: $(MAKEINC)
2281
2282 clean::
2283 rm -f $(GENERATED)
2284 $(foreach d,$(CLEANDIRS),rm -f $(addprefix $(d)/*.,$(COMPILED_LIB_EXTS));)
2285 $(foreach p,$(CLEANLIBS),rm -f $(addprefix $(p).,$(COMPILED_LIB_EXTS));)
2286
2287 detect-unused:
2288 @L1=$$(mktemp); \
2289 L2=$$(mktemp); \
2290 for d in `find examples/ -name 'why3session.xml' -printf '%h\n'`; do \
2291 sed -n -e 's/.*proof.*name="\([^"]*\)".*/\1/p' $$d/why3session.xml | sort > $$L1; \
2292 (cd $$d; git ls-files) | grep -v -e '^why3session.xml' -e '^why3shapes' -e '^[.]gitignore' -e '^Makefile' -e '[.]ml$$' -e '[.]html$$' | sed -e 's/[.]prf$$/.pvs/;s/[.]thy$$/.xml/' | sort -u > $$L2; \
2293 diff -u --label="$$d/why3session.xml" --label="$$d/" $$L1 $$L2 || echo; \
2294 done; \
2295 rm $$L1 $$L2
2296
2297 ##################################################################
2298 # Building the Why3 platform with ocamlbuild (OCaml 3.10 needed) #
2299 ##################################################################
2300
2301 # There used to be targets here but they are no longer useful.
2302
2303 # To build using Ocamlbuild:
2304 # 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
2305 # are generated.
2306 # 2) Run Ocamlbuild with any target to generate the sanitization script.
2307 # 3) Run ./sanitize to delete the generated files that shouldn't be generated
2308 # (i.e. all lexers and parsers).
2309 # 4) Run Ocamlbuild with the target you need, for example:
2310 # ocamlbuild jc/jc_main.native
2311
2312 # You can also use the Makefile ./build.makefile which has some handy targets.
A platform for deductive program verification