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