Makefile.in

   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@ @NUMINCLUDE@ @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 nums dynlink @ZIPLIB@ @WHY3LIB@ @INFERLIB@
 163 EXTPKGS = menhirLib @RELIB@ unix num 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
 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 \
 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/drivers
 467         $(MKDIR_P) $(DATADIR)/why3/extraction_drivers
 468         $(INSTALL_DATA) stdlib/*.mlw $(DATADIR)/why3/stdlib
 469         $(INSTALL_DATA) stdlib/mach/*.mlw $(DATADIR)/why3/stdlib/mach
 470         $(INSTALL_DATA) drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
 471         $(INSTALL_DATA) extraction_drivers/*.drv $(DATADIR)/why3/extraction_drivers
 472         $(INSTALL_DATA) LICENSE $(DATADIR)/why3/
 473         $(INSTALL_DATA) share/provers-detection-data.conf $(DATADIR)/why3/
 474         $(INSTALL_DATA) share/why3session.dtd $(DATADIR)/why3
 475         $(INSTALL_DATA) share/Makefile.config $(DATADIR)/why3
 476         $(INSTALL_DATA) share/vim/ftdetect/why3.vim $(DATADIR)/why3/vim/ftdetect/why3.vim
 477         $(INSTALL_DATA) share/vim/syntax/why3.vim $(DATADIR)/why3/vim/syntax/why3.vim
 478         $(INSTALL_DATA) share/lang/why3.lang $(DATADIR)/why3/lang/why3.lang
 479         $(INSTALL_DATA) share/lang/why3c.lang $(DATADIR)/why3/lang/why3c.lang
 480         $(INSTALL_DATA) share/lang/why3py.lang $(DATADIR)/why3/lang/why3py.lang
 481         $(INSTALL_DATA) share/lang/coma.lang $(DATADIR)/why3/lang/coma.lang
 482
 483 ifeq (@enable_local@,yes)
 484 else
 485 install:: install-bin install-data
 486
 487 uninstall:: uninstall-bin uninstall-data
 488         rm -rf $(LIBDIR)/why3
 489 endif
 490
 491 uninstall-lib:
 492         if test -d $(OCAMLINSTALLLIB) -a -w $(OCAMLINSTALLLIB); then \
 493           rm -rf $(OCAMLINSTALLLIB)/why3; \
 494         fi
 495
 496 uninstall:: uninstall-lib
 497
 498 install-lib::
 499         $(MKDIR_P) $(OCAMLINSTALLLIB)/why3
 500         $(INSTALL_DATA) $(wildcard $(addprefix lib/why3/why3., $(INSTALLED_LIB_EXTS))) \
 501                 lib/why3/META $(OCAMLINSTALLLIB)/why3
 502
 503 ##################
 504 # Why3 emacs mode
 505 ##################
 506
 507 %.elc: %.el
 508         $(EMACS) --batch --no-init-file -f batch-byte-compile $<
 509
 510 clean::
 511         rm -f share/emacs/why3.elc
 512
 513 uninstall-emacs:
 514         rm -f $(DATADIR)/emacs/site-lisp/why3.el
 515         rm -f $(DATADIR)/emacs/site-lisp/why3.elc
 516
 517 uninstall:: uninstall-emacs
 518
 519 install-emacs:
 520         $(MKDIR_P) $(DATADIR)/emacs/site-lisp/
 521         $(INSTALL_DATA) share/emacs/why3.el $(DATADIR)/emacs/site-lisp/why3.el
 522 ifeq (@enable_emacs_compilation@,yes)
 523         $(INSTALL_DATA) share/emacs/why3.elc $(DATADIR)/emacs/site-lisp/why3.elc
 524 endif
 525
 526 install:: install-emacs
 527
 528 ifeq (@enable_emacs_compilation@,yes)
 529 all: share/emacs/why3.elc
 530 endif
 531
 532
 533 ##################
 534 # Why3 plugins
 535 ##################
 536
 537 PLUGGENERATED = \
 538         plugins/tptp/tptp_lexer.ml \
 539         plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli \
 540         plugins/coma/coma_lexer.ml \
 541         plugins/coma/coma_parser.ml plugins/coma/coma_parser.mli \
 542         plugins/python/py_lexer.ml \
 543         plugins/python/py_parser.ml plugins/python/py_parser.mli \
 544         plugins/microc/mc_lexer.ml \
 545         plugins/microc/mc_parser.ml plugins/microc/mc_parser.mli \
 546         plugins/cfg/cfg_lexer.ml \
 547         plugins/cfg/cfg_parser.ml plugins/cfg/cfg_parser.mli \
 548         plugins/parser/dimacs.ml
 549
 550 PLUG_PARSER = genequlin dimacs
 551 PLUG_PRINTER =
 552 PLUG_TRANSFORM =
 553 PLUG_STRATEGIES = forward_propagation
 554 PLUG_TPTP = tptp_parser tptp_typing tptp_lexer tptp_printer
 555 PLUG_COMA = coma_logic coma_syntax coma_parser coma_lexer coma_typing coma_main
 556 PLUG_PYTHON = py_parser py_lexer py_main
 557 PLUG_MICROC = mc_parser mc_lexer mc_printer mc_main
 558 PLUG_CFG = cfg_parser cfg_lexer cfg_paths subregion_analysis cfg_main
 559 ifeq (@enable_stackify@,yes)
 560 PLUG_CFG += stackify cfg_stackify
 561 endif
 562
 563 PLUG_CMIONLY = tptp/tptp_ast python/py_ast microc/mc_ast cfg/cfg_ast
 564
 565 PLUGINS = genequlin dimacs tptp python microc coma cfg forward_propagation
 566
 567 TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
 568 COMAMODULES = $(addprefix plugins/coma/, $(PLUG_COMA))
 569 PYTHONMODULES = $(addprefix plugins/python/, $(PLUG_PYTHON))
 570 MICROCMODULES = $(addprefix plugins/microc/, $(PLUG_MICROC))
 571 CFGMODULES = $(addprefix plugins/cfg/, $(PLUG_CFG))
 572
 573 TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
 574 TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
 575
 576 COMACMO = $(addsuffix .cmo, $(COMAMODULES))
 577 COMACMX = $(addsuffix .cmx, $(COMAMODULES))
 578
 579 PYTHONCMO = $(addsuffix .cmo, $(PYTHONMODULES))
 580 PYTHONCMX = $(addsuffix .cmx, $(PYTHONMODULES))
 581
 582 MICROCCMO = $(addsuffix .cmo, $(MICROCMODULES))
 583 MICROCCMX = $(addsuffix .cmx, $(MICROCMODULES))
 584
 585 ifeq (@enable_hypothesis_selection@,yes)
 586 PLUG_TRANSFORM += hypothesis_selection
 587 PLUGINS += hypothesis_selection
 588
 589 lib/plugins/hypothesis_selection.cmxs: EXTINCLUDES += -I @OCAMLGRAPHLIB@
 590 lib/plugins/hypothesis_selection.cma:  EXTINCLUDES += -I @OCAMLGRAPHLIB@
 591 lib/plugins/hypothesis_selection.cmxs: EXTLIBS += graph.cmxa
 592 lib/plugins/hypothesis_selection.cma:  EXTOBJS += graph.cma
 593 ifeq (@enable_ocamlfind@,yes)
 594 lib/plugins/hypothesis_selection.cmxs: FLAGS += -package ocamlgraph -dontlink "$(EXTPKGS)" -linkpkg
 595 lib/plugins/hypothesis_selection.cma:  FLAGS += -package ocamlgraph -dontlink "$(EXTPKGS)" -linkpkg
 596 endif
 597 endif
 598
 599 PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
 600               $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
 601               $(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
 602               $(addprefix plugins/strategies/, $(PLUG_STRATEGIES)) \
 603               $(TPTPMODULES) $(COMAMODULES) \
 604               $(PYTHONMODULES) $(MICROCMODULES) $(CFGMODULES)
 605
 606 PLUGDEP = $(addsuffix .dep, $(PLUGMODULES)) $(PLUG_CMIONLY:%=plugins/%.dep)
 607 PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
 608 PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
 609 PLUGCMI = $(addsuffix .cmi, $(PLUGMODULES)) $(PLUG_CMIONLY:%=plugins/%.cmi)
 610
 611 PLUGDIRS = parser printer transform strategies tptp coma python microc cfg
 612 PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))
 613
 614 ifeq (@enable_stackify@,yes)
 615 plugins/cfg/stackify.cmx: EXTINCLUDES += -I @OCAMLGRAPHLIB@
 616 plugins/cfg/stackify.cmo: EXTINCLUDES += -I @OCAMLGRAPHLIB@
 617 plugins/cfg/stackify.cmx: EXTLIBS += graph.cmxa
 618 plugins/cfg/stackify.cmo: EXTOBJS += graph.cma
 619 ifeq (@enable_ocamlfind@,yes)
 620 plugins/cfg/stackify.cmx: FLAGS += -package ocamlgraph
 621 plugins/cfg/stackify.cmo: FLAGS += -package ocamlgraph
 622 lib/plugins/cfg.cmxs: FLAGS += -package ocamlgraph -dontlink "$(EXTPKGS)" -linkpkg
 623 lib/plugins/cfg.cma:  FLAGS += -package ocamlgraph -dontlink "$(EXTPKGS)" -linkpkg
 624 endif
 625 endif
 626
 627 $(PLUGDEP) $(PLUGCMO) $(PLUGCMX) $(PLUGCMI): INCLUDES += $(PLUGINCLUDES)
 628
 629 $(PLUGDEP): $(PLUGGENERATED)
 630
 631 LIBPLUGCMA =  $(PLUGINS:%=lib/plugins/%.cma)
 632 LIBPLUGCMXS = $(PLUGINS:%=lib/plugins/%.cmxs)
 633
 634 plugins.byte: $(LIBPLUGCMA)
 635 plugins.opt : $(LIBPLUGCMXS)
 636
 637 lib/plugins:
 638         mkdir lib/plugins
 639
 640 lib/plugins/%.cmxs: | lib/plugins
 641         $(SHOW) 'Linking  $@'
 642         $(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
 643
 644 lib/plugins/%.cma: | lib/plugins
 645         $(SHOW) 'Linking  $@'
 646         $(HIDE)$(OCAMLC) $(BFLAGS) -a -o $@ $^
 647
 648 $(PLUG_PARSER:%=lib/plugins/%.cmxs): lib/plugins/%.cmxs: plugins/parser/%.cmx
 649 $(PLUG_PARSER:%=lib/plugins/%.cma): lib/plugins/%.cma: plugins/parser/%.cmo
 650 $(PLUG_PRINTER:%=lib/plugins/%.cmxs): lib/plugins/%.cmxs: plugins/printer/%.cmx
 651 $(PLUG_PRINTER:%=lib/plugins/%.cma): lib/plugins/%.cma: plugins/printer/%.cmo
 652 $(PLUG_TRANSFORM:%=lib/plugins/%.cmxs): lib/plugins/%.cmxs: plugins/transform/%.cmx
 653 $(PLUG_TRANSFORM:%=lib/plugins/%.cma): lib/plugins/%.cma: plugins/transform/%.cmo
 654 $(PLUG_STRATEGIES:%=lib/plugins/%.cmxs): lib/plugins/%.cmxs: plugins/strategies/%.cmx
 655 $(PLUG_STRATEGIES:%=lib/plugins/%.cma): lib/plugins/%.cma: plugins/strategies/%.cmo
 656 lib/plugins/tptp.cmxs: $(TPTPCMX)
 657 lib/plugins/tptp.cma: $(TPTPCMO)
 658 lib/plugins/coma.cmxs: $(COMACMX)
 659 lib/plugins/coma.cma: $(COMACMO)
 660 lib/plugins/python.cmxs: $(PYTHONCMX)
 661 lib/plugins/python.cma: $(PYTHONCMO)
 662 lib/plugins/microc.cmxs: $(MICROCCMX)
 663 lib/plugins/microc.cma: $(MICROCCMO)
 664 lib/plugins/cfg.cmxs: $(addsuffix .cmx, $(CFGMODULES))
 665 lib/plugins/cfg.cma: $(addsuffix .cmo, $(CFGMODULES))
 666
 667 # depend and clean targets
 668
 669 MAKEINC += $(PLUGDEP)
 670
 671 CLEANDIRS += plugins $(addprefix plugins/, $(PLUGDIRS)) lib/plugins
 672 GENERATED += $(PLUGGENERATED)
 673
 674 uninstall-bin::
 675         rm -f $(PLUGINS:%=$(LIBDIR)/why3/plugins/%.cma)
 676         rm -f $(PLUGINS:%=$(LIBDIR)/why3/plugins/%.cmxs)
 677
 678 install-bin::
 679         $(MKDIR_P) $(LIBDIR)/why3/plugins
 680         $(INSTALL_DATA) $(wildcard $(LIBPLUGCMA) $(LIBPLUGCMXS)) $(LIBDIR)/why3/plugins
 681
 682 ###############
 683 # Why3 commands
 684 ###############
 685
 686 TOOLSGENERATED = src/tools/why3wc.ml
 687
 688 TOOLS_BIN = \
 689         why3config why3execute why3extract why3prove \
 690         why3realize why3replay why3show why3wc why3bench
 691
 692 TOOLS_FILES = main $(TOOLS_BIN)
 693
 694 TOOLSMODULES = $(addprefix src/tools/, $(TOOLS_FILES))
 695
 696 TOOLSDEP = $(addsuffix .dep, $(TOOLSMODULES))
 697 TOOLSCMO = $(addsuffix .cmo, $(TOOLSMODULES))
 698 TOOLSCMX = $(addsuffix .cmx, $(TOOLSMODULES))
 699
 700 $(TOOLSDEP) $(TOOLSCMO) $(TOOLSCMX): INCLUDES += -I src/tools
 701
 702 $(TOOLSDEP): $(TOOLSGENERATED)
 703
 704 byte: bin/why3.byte $(TOOLS_BIN:%=bin/%.cma)
 705 opt:  bin/why3.opt  $(TOOLS_BIN:%=bin/%.cmxs)
 706
 707 bin/why3.opt: $(WHY3CMXA) src/tools/main.cmx
 708 bin/why3.byte: $(WHY3CMA) src/tools/main.cmo
 709
 710 $(TOOLS_BIN:%=bin/%.cma):  bin/%.cma:  src/tools/%.cmo
 711 $(TOOLS_BIN:%=bin/%.cmxs): bin/%.cmxs: src/tools/%.cmx
 712
 713 uninstall-bin::
 714         rm -f $(BINDIR)/why3$(EXE)
 715         rm -f $(TOOLS_BIN:%=bin/%.$(SHAREDBEST))
 716
 717 install-bin::
 718         $(MKDIR_P) $(BINDIR)
 719         $(INSTALL) bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
 720         $(MKDIR_P) $(TOOLDIR)
 721         $(INSTALL_DATA) $(TOOLS_BIN:%=bin/%.$(SHAREDBEST)) $(TOOLDIR)
 722
 723 install_local:: bin/why3$(EXE) $(TOOLS_BIN:%=bin/%.$(SHAREDBEST))
 724
 725 bin/why3$(EXE): bin/why3.@OCAMLBEST@
 726         ln -sf $(notdir $<) $@
 727
 728 install_local:: share/drivers share/extraction_drivers share/stdlib
 729
 730 share/drivers share/extraction_drivers share/stdlib: share/%:
 731         ln -snf ../$* $@
 732
 733 MAKEINC += $(TOOLSDEP)
 734
 735 CLEANDIRS += src/tools
 736 GENERATED += $(TOOLSGENERATED)
 737
 738 clean::
 739         rm -f bin/why3*
 740
 741 ##############
 742 # Why3server #
 743 ##############
 744
 745 SERVER_MODULES := logging arraylist options queue readbuf request \
 746                   proc writebuf server-unix server-win
 747
 748 CPULIM_MODULES := cpulimit-unix cpulimit-win
 749
 750 SERVER_O := $(SERVER_MODULES:%=src/server/%.o)
 751
 752 CPULIM_O := $(CPULIM_MODULES:%=src/server/%.o)
 753
 754 TOOLS = lib/why3server$(EXE) lib/why3cpulimit$(EXE)
 755
 756 all: $(TOOLS)
 757
 758 lib/why3server$(EXE): $(SERVER_O)
 759         $(CC) -Wall -o $@ $^
 760
 761 lib/why3cpulimit$(EXE): $(CPULIM_O)
 762         $(CC) -Wall -o $@ $^
 763
 764 %.o: %.c
 765         $(CC) -Wall -O -g -o $@ -c $<
 766
 767 uninstall-bin::
 768         rm -f $(LIBDIR)/why3/why3server$(EXE) $(LIBDIR)/why3/why3cpulimit$(EXE)
 769         rm -f $(LIBDIR)/why3/why3-call-pvs
 770
 771 install-bin::
 772         $(MKDIR_P) $(LIBDIR)/why3
 773         $(INSTALL) lib/why3server$(EXE) $(LIBDIR)/why3/why3server$(EXE)
 774         $(INSTALL) lib/why3cpulimit$(EXE) $(LIBDIR)/why3/why3cpulimit$(EXE)
 775         $(INSTALL) lib/why3-call-pvs $(LIBDIR)/why3/why3-call-pvs
 776
 777 clean::
 778         rm -f $(SERVER_O) $(CPULIM_O) $(TOOLS)
 779
 780 ##########
 781 # gallery
 782 ##########
 783
 784 # we export exactly the programs that have a why3session.xml file
 785
 786 .PHONY: gallery gallery-simple gallery-subs
 787
 788 gallery: gallery-simple gallery-subs
 789
 790 gallery-simple:
 791         @if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
 792         @cd examples/; \
 793         for x in `git ls-files */why3session.xml` ; do \
 794           f=`dirname $$x`; \
 795           if echo $$f | grep -q -e '\(_vc_sp\|^bignum\)$$'; then continue; fi; \
 796           echo "exporting $$f"; \
 797           mkdir -p $(GALLERYDIR)/$$f; \
 798           WHY3CONFIG="" ../bin/why3.@OCAMLBEST@ session html $$x -o $(GALLERYDIR)/$$f; \
 799           cp $$f.mlw $(GALLERYDIR)/$$f/; \
 800           rm -f $(GALLERYDIR)/$$f/$$f.zip; \
 801           git archive --format=zip -o $(GALLERYDIR)/$$f/$$f.zip HEAD $$f.mlw $$f; \
 802         done
 803
 804 GALLERYSUBS=WP_revisited verifythis_2016_matrix_multiplication avl double_wp prover multiprecision
 805
 806 gallery-subs:
 807         @if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
 808         @for d in $(GALLERYSUBS) ; do \
 809           echo "exporting examples/$$d"; \
 810           mkdir -p $(GALLERYDIR)/$$d; \
 811           cd examples/$$d; \
 812           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; \
 813           cd ..; \
 814           rm -f $(GALLERYDIR)/$$d/$$d.zip; \
 815           git archive --format=zip -o $(GALLERYDIR)/$$d/$$d.zip HEAD $$d; \
 816           cd ..; \
 817         done
 818
 819 ########
 820 # XML DTD validation
 821 ########
 822
 823 .PHONY: xml-validate xml-validate-local
 824
 825 xml-validate:
 826         @for x in `find examples/ -name why3session.xml`; do \
 827           xmllint --noout --valid $$x 2>&1 | head -1; \
 828         done
 829
 830 xml-validate-local:
 831         @for x in `find examples/ -name why3session.xml -print`; do \
 832           xmllint --nonet --noout --path share --valid $$x 2>&1 | sed -e '/I.O error/d' | head -1; \
 833         done
 834
 835 ###############
 836 # IDE
 837 ###############
 838
 839 IDEGENERATED =
 840 GENERATED += $(IDEGENERATED)
 841
 842 ifeq (@enable_ide@,yes)
 843
 844 IDE_FILES =
 845
 846 ifeq (@enable_statmemprof@,yes)
 847 IDE_FILES += statmemprof
 848
 849 bin/why3ide.cmxs bin/why3ide.cma: EXTPKGS += @STATMEMPROFPKG@
 850 endif
 851
 852 IDE_FILES += gconfig ide_utils why3ide
 853
 854 IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
 855
 856 IDEDEP = $(addsuffix .dep, $(IDEMODULES))
 857 IDECMO = $(addsuffix .cmo, $(IDEMODULES))
 858 IDECMX = $(addsuffix .cmx, $(IDEMODULES))
 859
 860 $(IDEDEP) $(IDECMO) $(IDECMX): INCLUDES += -I src/ide
 861
 862 $(IDEDEP): $(IDEGENERATED)
 863
 864 # build targets
 865
 866 byte: bin/why3ide.cma
 867 opt:  bin/why3ide.cmxs
 868
 869 bin/why3ide.cmxs bin/why3ide.cma: FLAGS += $(addprefix -package ,@LABLGTKPKG@) -dontlink "$(EXTPKGS)" -linkpkg
 870
 871 bin/why3ide.cmxs: $(IDECMX)
 872 bin/why3ide.cma:  $(IDECMO)
 873
 874 # depend and clean targets
 875
 876 MAKEINC += $(IDEDEP)
 877
 878 CLEANDIRS += src/ide
 879
 880 ide: bin/why3ide.$(SHAREDBEST)
 881
 882 uninstall-ide:
 883         rm -f $(TOOLDIR)/why3ide.$(SHAREDBEST)
 884         rm -rf $(DATADIR)/why3/images
 885
 886 uninstall:: uninstall-ide
 887
 888 install-ide:
 889         $(MKDIR_P) $(TOOLDIR)
 890         $(INSTALL_DATA) bin/why3ide.$(SHAREDBEST) $(TOOLDIR)
 891         $(MKDIR_P) $(DATADIR)/why3/images
 892         for i in share/images/*.rc; do \
 893              d=`basename $$i .rc`; \
 894              $(INSTALL_DATA) $$i $(DATADIR)/why3/images; \
 895              $(MKDIR_P) $(DATADIR)/why3/images/$$d; \
 896              $(INSTALL_DATA) share/images/$$d/* $(DATADIR)/why3/images/$$d; \
 897         done
 898         $(INSTALL_DATA) share/images/*.png $(DATADIR)/why3/images
 899
 900 install:: install-ide
 901
 902 install_local:: bin/why3ide.$(SHAREDBEST)
 903
 904 endif
 905
 906 ###############
 907 # WEBSERV
 908 ###############
 909
 910 WEBSERV_FILES = wserver why3web
 911
 912 WEBSERVMODULES = $(addprefix src/ide/, $(WEBSERV_FILES))
 913
 914 WEBSERVDEP = $(addsuffix .dep, $(WEBSERVMODULES))
 915 WEBSERVCMO = $(addsuffix .cmo, $(WEBSERVMODULES))
 916 WEBSERVCMX = $(addsuffix .cmx, $(WEBSERVMODULES))
 917
 918 $(WEBSERVDEP) $(WEBSERVCMO) $(WEBSERVCMX): INCLUDES += -I src/ide
 919
 920 # build targets
 921
 922 byte: bin/why3webserver.cma
 923 opt:  bin/why3webserver.cmxs
 924
 925 bin/why3webserver.cmxs: $(WEBSERVCMX)
 926 bin/why3webserver.cma:  $(WEBSERVCMO)
 927
 928 # depend and clean targets
 929
 930 MAKEINC += $(WEBSERVDEP)
 931
 932 CLEANDIRS += src/ide
 933
 934 uninstall-bin::
 935         rm -f $(TOOLDIR)/why3webserver.$(SHAREDBEST)
 936
 937 install-bin::
 938         $(MKDIR_P) $(TOOLDIR)
 939         $(INSTALL_DATA) bin/why3webserver.$(SHAREDBEST) $(TOOLDIR)
 940
 941 install_local:: bin/why3webserver.$(SHAREDBEST)
 942
 943
 944 ###############
 945 # Session
 946 ###############
 947
 948 SESSION_FILES = why3session_lib why3session_info \
 949                 why3session_html why3session_latex why3session_update  \
 950                 why3session_output why3session_create why3session_main
 951 # TODO: why3session_copy why3session_rm why3session_csv why3session_run
 952 #       why3session_output
 953
 954 SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
 955
 956 SESSIONDEP = $(addsuffix .dep, $(SESSIONMODULES))
 957 SESSIONCMO = $(addsuffix .cmo, $(SESSIONMODULES))
 958 SESSIONCMX = $(addsuffix .cmx, $(SESSIONMODULES))
 959
 960 $(SESSIONDEP) $(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session
 961
 962 # build targets
 963
 964 byte: bin/why3session.cma
 965 opt:  bin/why3session.cmxs
 966
 967 bin/why3session.cmxs: $(SESSIONCMX)
 968 bin/why3session.cma:  $(SESSIONCMO)
 969
 970 # depend and clean targets
 971
 972 MAKEINC += $(SESSIONDEP)
 973
 974 CLEANDIRS += src/why3session
 975
 976 uninstall-bin::
 977         rm -f $(TOOLDIR)/why3session.$(SHAREDBEST)
 978
 979 install-bin::
 980         $(MKDIR_P) $(TOOLDIR)
 981         $(INSTALL_DATA) bin/why3session.$(SHAREDBEST) $(TOOLDIR)
 982
 983 install_local:: bin/why3session.$(SHAREDBEST)
 984
 985 ###############
 986 # Why3 Shell
 987 ###############
 988
 989 SHELL_FILES = why3shell
 990
 991 SHELLMODULES = $(addprefix src/tools/, $(SHELL_FILES))
 992
 993 SHELLDEP = $(addsuffix .dep, $(SHELLMODULES))
 994 SHELLCMO = $(addsuffix .cmo, $(SHELLMODULES))
 995 SHELLCMX = $(addsuffix .cmx, $(SHELLMODULES))
 996
 997 $(SHELLDEP) $(SHELLCMO) $(SHELLCMX): INCLUDES += -I src/tools
 998
 999 # build targets
1000
1001 byte: bin/why3shell.cma
1002 opt:  bin/why3shell.cmxs
1003
1004 bin/why3shell.cmxs: $(SHELLCMX)
1005 bin/why3shell.cma:  $(SHELLCMO)
1006
1007 # depend and clean targets
1008
1009 MAKEINC += $(SHELLDEP)
1010
1011 uninstall-bin::
1012         rm -f $(TOOLDIR)/why3shell.$(SHAREDBEST)
1013
1014 install-bin::
1015         $(MKDIR_P) $(TOOLDIR)
1016         $(INSTALL_DATA) bin/why3shell.$(SHAREDBEST) $(TOOLDIR)
1017
1018 install_local:: bin/why3shell.$(SHAREDBEST)
1019
1020 ####################
1021 # Coq realizations
1022 ####################
1023
1024 COQVERSIONSPECIFIC=
1025
1026 COQVERSIONSPECIFICTARGETS=$(addprefix lib/coq/, $(COQVERSIONSPECIFIC))
1027
1028 $(COQVERSIONSPECIFICTARGETS): %: %.@coq_compat_version@
1029         $(CMP_CP)
1030
1031 clean-coq::
1032         rm -f $(COQVERSIONSPECIFICTARGETS)
1033
1034 COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power NumOf
1035 COQLIBS_INT_ALL_FILES = Exponentiation $(COQLIBS_INT_FILES)
1036 COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES))
1037
1038 COQLIBS_BOOL_FILES = Bool
1039 COQLIBS_BOOL = $(addprefix lib/coq/bool/, $(COQLIBS_BOOL_FILES))
1040
1041 ifeq (@enable_coq_fp_libs@,yes)
1042 COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt PowerReal Real RealInfix Square Trigonometry Truncate
1043 else
1044 COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt PowerReal Real RealInfix Square Trigonometry
1045 endif
1046 COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
1047
1048 COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
1049 COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
1050
1051 COQLIBS_SET_FILES = Set Cardinal Fset FsetInduction FsetInt FsetSum SetApp SetAppInt SetImp SetImpInt
1052 COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
1053
1054 COQLIBS_MAP_FILES = Map Const Occ MapPermut MapInjection
1055 COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES))
1056
1057 COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt NthNoOpt RevAppend Combine Distinct NumOcc Permut
1058 COQLIBS_LIST = $(addprefix lib/coq/list/, $(COQLIBS_LIST_FILES))
1059
1060 COQLIBS_OPTION_FILES = Option
1061 COQLIBS_OPTION = $(addprefix lib/coq/option/, $(COQLIBS_OPTION_FILES))
1062
1063 COQLIBS_BV_FILES = Pow2int BV_Gen
1064 COQLIBS_BV = $(addprefix lib/coq/bv/, $(COQLIBS_BV_FILES))
1065
1066 ifeq (@enable_coq_fp_libs@,yes)
1067 COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
1068 COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
1069 COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
1070
1071 COQLIBS_IEEEFLOAT_FILES = RoundingMode GenericFloat Float32 Float64
1072 COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES))
1073 endif
1074
1075 COQLIBS_FOR_DRIVERS_FILES = ComputerOfEuclideanDivision
1076 COQLIBS_FOR_DRIVERS = $(addprefix lib/coq/for_drivers/, $(COQLIBS_FOR_DRIVERS_FILES))
1077
1078 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)
1079
1080 %.vo: %.v
1081         $(SHOW) 'Coqc     $<'
1082         $(HIDE)$(COQC) $(COQFLAGS) -R lib/coq Why3 $<
1083
1084 %.vd: %.v
1085         $(SHOW) 'Coqdep   $<'
1086         $(HIDE)$(COQDEP) -R lib/coq Why3 $< $(TOTARGET)
1087
1088 COQV  = $(addsuffix .v,  $(COQLIBS_FILES))
1089 COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
1090 COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
1091
1092 coq: $(COQVO) drivers/coq-realizations.aux lib/coq/version
1093
1094 clean-coq::
1095         rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES)) lib/coq/version \
1096                 $(foreach f,$(COQLIBS_FILES),$(dir $f).$(notdir $f).aux)
1097
1098 drivers/coq-realizations.aux: Makefile
1099         $(SHOW) 'Generate $@'
1100         $(HIDE)(echo "(* generated automatically at compilation time *)"; \
1101         echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \
1102         echo 'theory HighOrd meta "realized_theory" "HighOrd", "" end'; \
1103         echo 'theory WellFounded meta "realized_theory" "WellFounded", "" end'; \
1104         for f in $(COQLIBS_INT_FILES); do \
1105         echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
1106         for f in $(COQLIBS_BOOL_FILES); do \
1107         echo 'theory bool.'"$$f"' meta "realized_theory" "bool.'"$$f"'", "" end'; done; \
1108         for f in $(COQLIBS_REAL_FILES); do \
1109         echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
1110         for f in $(COQLIBS_NUMBER_FILES); do \
1111         echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
1112         for f in $(COQLIBS_SET_FILES); do \
1113         echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
1114         for f in $(COQLIBS_MAP_FILES); do \
1115         echo 'theory map.'"$$f"' meta "realized_theory" "map.'"$$f"'", "" end'; done; \
1116         for f in $(COQLIBS_LIST_FILES); do \
1117         echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
1118         for f in $(COQLIBS_OPTION_FILES); do \
1119         echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
1120         for f in $(COQLIBS_BV_FILES); do \
1121         echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \
1122         for f in $(COQLIBS_IEEEFLOAT_FILES); do \
1123         echo 'theory ieee_float.'"$$f"' meta "realized_theory" "ieee_float.'"$$f"'", "" end'; done; \
1124         for f in $(COQLIBS_FP_FILES); do \
1125         echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
1126         for f in $(COQLIBS_FOR_DRIVERS_FILES); do \
1127         echo 'theory for_drivers.'"$$f"' meta "realized_theory" "for_drivers.'"$$f"'", "" end'; done; \
1128         ) > $@
1129
1130 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
1131
1132 LOCAL_STDLIB=-L stdlib --no-stdlib --no-load-default-plugins
1133
1134 update-coq-int: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/int.mlw
1135         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
1136
1137 update-coq-bool: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/bool.mlw
1138         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
1139
1140 update-coq-real: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/real.mlw
1141         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
1142
1143 update-coq-number: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/number.mlw
1144         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
1145
1146 update-coq-set: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/set.mlw
1147         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
1148
1149 update-coq-map: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/map.mlw
1150         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
1151
1152 update-coq-list: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/list.mlw
1153         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
1154
1155 update-coq-option: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/option.mlw
1156         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
1157
1158 update-coq-bv: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/bv.mlw
1159         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
1160
1161 update-coq-for-drivers: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/for_drivers.mlw
1162         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
1163
1164 update-coq-ieee_float: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/ieee_float.mlw
1165         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
1166
1167 update-coq-fp: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/floating_point.mlw
1168         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
1169
1170 ifeq (@enable_coq_libs@,yes)
1171
1172 uninstall-coq:
1173         rm -rf $(LIBDIR)/why3/coq
1174
1175 install-coq:
1176         $(MKDIR_P) $(LIBDIR)/why3/coq
1177         $(INSTALL_DATA) lib/coq/version $(LIBDIR)/why3/coq/
1178         $(INSTALL_DATA) lib/coq/BuiltIn.vo lib/coq/HighOrd.vo lib/coq/WellFounded.vo $(LIBDIR)/why3/coq/
1179         $(MKDIR_P) $(LIBDIR)/why3/coq/int
1180         $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/
1181         $(MKDIR_P) $(LIBDIR)/why3/coq/bool
1182         $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_BOOL)) $(LIBDIR)/why3/coq/bool/
1183         $(MKDIR_P) $(LIBDIR)/why3/coq/real
1184         $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
1185         $(MKDIR_P) $(LIBDIR)/why3/coq/number
1186         $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_NUMBER)) $(LIBDIR)/why3/coq/number/
1187         $(MKDIR_P) $(LIBDIR)/why3/coq/set
1188         $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_SET)) $(LIBDIR)/why3/coq/set/
1189         $(MKDIR_P) $(LIBDIR)/why3/coq/map
1190         $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_MAP)) $(LIBDIR)/why3/coq/map/
1191         $(MKDIR_P) $(LIBDIR)/why3/coq/list
1192         $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_LIST)) $(LIBDIR)/why3/coq/list/
1193         $(MKDIR_P) $(LIBDIR)/why3/coq/option
1194         $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_OPTION)) $(LIBDIR)/why3/coq/option/
1195         $(MKDIR_P) $(LIBDIR)/why3/coq/bv
1196         $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_BV)) $(LIBDIR)/why3/coq/bv/
1197 ifeq (@enable_coq_fp_libs@,yes)
1198         $(MKDIR_P) $(LIBDIR)/why3/coq/floating_point
1199         $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
1200         $(MKDIR_P) $(LIBDIR)/why3/coq/ieee_float
1201         $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_IEEEFLOAT)) $(LIBDIR)/why3/coq/ieee_float/
1202 endif
1203         $(MKDIR_P) $(LIBDIR)/why3/coq/for_drivers
1204         $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_FOR_DRIVERS)) $(LIBDIR)/why3/coq/for_drivers/
1205         $(MKDIR_P) $(DATADIR)/why3/drivers
1206         $(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
1207
1208 install:: install-coq
1209
1210 all: coq
1211
1212 ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq"
1213 MAKEINC += $(COQVD)
1214 endif
1215
1216 endif
1217
1218 install-data::
1219         $(MKDIR_P) $(DATADIR)/why3/drivers
1220         $(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
1221
1222 all: drivers/coq-realizations.aux
1223
1224 clean:: clean-coq
1225         rm -f drivers/coq-realizations.aux
1226
1227 ####################
1228 # PVS realizations
1229 ####################
1230
1231 PVSLIBS_INT_FILES = Int Abs MinMax ComputerDivision EuclideanDivision
1232 PVSLIBS_INT = $(addprefix lib/pvs/int/, $(PVSLIBS_INT_FILES))
1233
1234 PVSLIBS_REAL_FILES = Abs FromInt MinMax Real Square ExpLog Trigonometry \
1235                      PowerInt
1236  # RealInfix
1237 PVSLIBS_REAL = $(addprefix lib/pvs/real/, $(PVSLIBS_REAL_FILES))
1238
1239 PVSLIBS_LIST_FILES =
1240   # Nth
1241 PVSLIBS_LIST = $(addprefix lib/pvs/int/, $(PVSLIBS_LIST_FILES))
1242
1243 PVSLIBS_NUMBER_FILES = # Divisibility Gcd Parity Prime
1244 PVSLIBS_NUMBER = $(addprefix lib/pvs/number/, $(PVSLIBS_NUMBER_FILES))
1245
1246 PVSLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
1247 PVSLIBS_FP_ALL_FILES = $(PVSLIBS_FP_FILES)
1248 PVSLIBS_FP = $(addprefix lib/pvs/floating_point/, $(PVSLIBS_FP_ALL_FILES))
1249
1250 PVSLIBS_FILES = $(PVSLIBS_INT) $(PVSLIBS_REAL) $(PVSLIBS_LIST) \
1251                 $(PVSLIBS_NUMBER) $(PVSLIBS_FP)
1252
1253 update-pvs: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/pvs-realizations.aux
1254         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
1255         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
1256         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
1257         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
1258         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
1259
1260 drivers/pvs-realizations.aux: Makefile
1261         $(SHOW) 'Generate $@'
1262         $(HIDE)(echo "(* generated automatically at compilation time *)"; \
1263         for f in $(PVSLIBS_INT_FILES); do \
1264         echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
1265         for f in $(PVSLIBS_REAL_FILES); do \
1266         echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
1267         for f in $(PVSLIBS_LIST_FILES); do \
1268         echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
1269         for f in $(PVSLIBS_NUMBER_FILES); do \
1270         echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
1271         for f in $(PVSLIBS_FP_FILES); do \
1272         echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
1273         ) > $@
1274
1275 pvs: lib/pvs/version
1276
1277 clean-pvs:
1278         rm -f lib/pvs/version
1279
1280 ifeq (@enable_pvs_libs@,yes)
1281
1282 uninstall-pvs:
1283         rm -rf $(LIBDIR)/why3/pvs
1284
1285 install-pvs:
1286         $(MKDIR_P) $(LIBDIR)/why3/pvs
1287         $(INSTALL_DATA) lib/pvs/version $(LIBDIR)/why3/pvs/
1288         $(MKDIR_P) $(LIBDIR)/why3/pvs/int
1289         $(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_INT)) $(LIBDIR)/why3/pvs/int/
1290         $(INSTALL_DATA) $(addsuffix .prf, $(PVSLIBS_INT)) $(LIBDIR)/why3/pvs/int/
1291         $(MKDIR_P) $(LIBDIR)/why3/pvs/real
1292         $(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_REAL)) $(LIBDIR)/why3/pvs/real/
1293         $(INSTALL_DATA) $(addsuffix .prf, $(PVSLIBS_REAL)) $(LIBDIR)/why3/pvs/real/
1294         $(MKDIR_P) $(LIBDIR)/why3/pvs/floating_point/
1295         $(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_FP)) $(LIBDIR)/why3/pvs/floating_point/
1296         $(MKDIR_P) $(DATADIR)/why3/drivers/
1297         $(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
1298
1299 install:: install-pvs
1300
1301 all: pvs
1302
1303 endif
1304
1305 install-data::
1306         $(MKDIR_P) $(DATADIR)/why3/drivers/
1307         $(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
1308
1309 all: drivers/pvs-realizations.aux
1310
1311 clean:: clean-pvs
1312         rm -f drivers/pvs-realizations.aux
1313
1314 #######################
1315 # Isabelle realizations
1316 #######################
1317
1318
1319 ISABELLEVERSIONSPECIFIC=ROOT why3.ML Why3_BV.thy Why3_Map.thy
1320
1321 ISABELLEVERSIONSPECIFICTARGETS=$(addprefix lib/isabelle/, $(ISABELLEVERSIONSPECIFIC))
1322
1323 ISABELLEREALIZEDRV=isabelle-realize
1324 ISABELLEREALIZEDRVPATH=drivers/$(ISABELLEREALIZEDRV).drv
1325
1326 $(ISABELLEVERSIONSPECIFICTARGETS): %: %.@ISABELLEVERSION@
1327         $(CMP_CP)
1328
1329 clean-isabelle::
1330         rm -f $(ISABELLEVERSIONSPECIFICTARGETS)
1331
1332 ISABELLELIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
1333 ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/int/, $(ISABELLELIBS_INT_FILES)))
1334
1335 ISABELLELIBS_BOOL_FILES = Bool
1336 ISABELLELIBS_BOOL = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/bool/, $(ISABELLELIBS_BOOL_FILES)))
1337
1338 ISABELLELIBS_REAL_FILES = Real RealInfix Abs MinMax FromInt Truncate Square ExpLog Trigonometry PowerInt # not yet realized : PowerReal Hyperbolic Polar
1339 ISABELLELIBS_REAL = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/real/, $(ISABELLELIBS_REAL_FILES)))
1340
1341 ISABELLELIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
1342 ISABELLELIBS_NUMBER = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/number/, $(ISABELLELIBS_NUMBER_FILES)))
1343
1344 ISABELLELIBS_SET_FILES = Set Fset
1345 ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/set/, $(ISABELLELIBS_SET_FILES)))
1346
1347 ISABELLELIBS_MAP_FILES = Map Const Occ MapPermut MapInjection
1348 ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/map/, $(ISABELLELIBS_MAP_FILES)))
1349
1350 ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt RevAppend Combine Distinct NumOcc Permut
1351 ISABELLELIBS_LIST = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/list/, $(ISABELLELIBS_LIST_FILES)))
1352
1353 ISABELLELIBS_BV_FILES = Pow2int
1354 # BV8 BV16 BV32 BV64 BVConverter_32_64 BVConverter_16_64 BVConverter_8_64 BVConverter_16_32 BVConverter_8_32 BVConverter_8_16
1355 ISABELLELIBS_BV = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/bv/, $(ISABELLELIBS_BV_FILES)))
1356
1357 ISABELLELIBS = $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
1358
1359 drivers/isabelle-realizations.aux: Makefile
1360         $(SHOW) 'Generate $@'
1361         $(HIDE)(echo "(* generated automatically at compilation time *)"; \
1362         echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \
1363         for f in $(ISABELLELIBS_INT_FILES); do \
1364         echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
1365         for f in $(ISABELLELIBS_BOOL_FILES); do \
1366         echo 'theory bool.'"$$f"' meta "realized_theory" "bool.'"$$f"'", "" end'; done; \
1367         for f in $(ISABELLELIBS_REAL_FILES); do \
1368         echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
1369         for f in $(ISABELLELIBS_NUMBER_FILES); do \
1370         echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
1371         for f in $(ISABELLELIBS_SET_FILES); do \
1372         echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
1373         for f in $(ISABELLELIBS_MAP_FILES); do \
1374         echo 'theory map.'"$$f"' meta "realized_theory" "map.'"$$f"'", "" end'; done; \
1375         for f in $(ISABELLELIBS_LIST_FILES); do \
1376         echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
1377         for f in $(ISABELLELIBS_OPTION_FILES); do \
1378         echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
1379         for f in $(ISABELLELIBS_BV_FILES); do \
1380         echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \
1381         ) > $@
1382
1383 ifeq (@enable_local@,yes)
1384   ISABELLE_TARGET_DIR=`pwd`/lib/isabelle
1385 else
1386   ISABELLE_TARGET_DIR=$(LIBDIR)/why3/isabelle
1387 endif
1388
1389 $(GENERATED_PREFIX_ISABELLE)/realizations: $(ISABELLELIBS)
1390         $(HIDE)sha1sum $^ | sed -e "s,$(GENERATED_PREFIX_ISABELLE)/,," > $@
1391
1392 update-isabelle: $(GENERATED_PREFIX_ISABELLE)/realizations
1393
1394 $(ISABELLELIBS_INT): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1395   $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/int.mlw
1396         $(SHOW) "Generating Isabelle realization for int.$(notdir $(basename $@))"
1397         $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/int
1398         $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/int/
1399
1400 $(ISABELLELIBS_BOOL): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1401   $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/bool.mlw
1402         $(SHOW) "Generating Isabelle realization for bool.$(notdir $(basename $@))"
1403         $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/bool
1404         $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bool/
1405
1406 $(ISABELLELIBS_REAL): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1407   $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/real.mlw
1408         $(SHOW) "Generating Isabelle realization for real.$(notdir $(basename $@))"
1409         $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/real
1410         $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/real/
1411
1412 $(ISABELLELIBS_NUMBER): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1413   $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/number.mlw
1414         $(SHOW) "Generating Isabelle realization for number.$(notdir $(basename $@))"
1415         $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/number
1416         $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/number/
1417
1418 $(ISABELLELIBS_SET): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1419   $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/set.mlw
1420         $(SHOW) "Generating Isabelle realization for set.$(notdir $(basename $@))"
1421         $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/set
1422         $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/set/
1423
1424 $(ISABELLELIBS_MAP): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1425   $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/map.mlw
1426         $(SHOW) "Generating Isabelle realization for map.$(notdir $(basename $@))"
1427         $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/map
1428         $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/map/
1429
1430 $(ISABELLELIBS_LIST): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1431   $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/list.mlw
1432         $(SHOW) "Generating Isabelle realization for list.$(notdir $(basename $@))"
1433         $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/list
1434         $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/list/
1435
1436 $(ISABELLELIBS_OPTION): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1437   $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/option.mlw
1438         $(SHOW) "Generating Isabelle realization for option.$(notdir $(basename $@))"
1439         $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/option
1440         $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/option/
1441
1442 $(ISABELLELIBS_BV): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
1443   $(ISABELLEREALIZEDRVPATH) drivers/isabelle-common.gen stdlib/bv.mlw
1444         $(SHOW) "Generating Isabelle realization for bv.$(notdir $(basename $@))"
1445         $(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/bv
1446         $(HIDE)WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bv/
1447
1448 ifeq (@enable_isabelle_libs@,yes)
1449
1450 $(GENERATED_PREFIX_ISABELLE)/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(ISABELLELIBS)
1451 ifneq (@enable_local@,yes)
1452         cp -r $(GENERATED_PREFIX_ISABELLE) "$(LIBDIR)/why3"
1453 endif
1454         @(if isabelle components -l | grep -q "$(ISABELLE_TARGET_DIR)$$"; then \
1455             echo "Building the Why3 heap for Isabelle/HOL:"; \
1456             isabelle build -bc Why3; \
1457             touch $@; \
1458           else \
1459             echo "[Warning] Cannot pre-build the Isabelle heap because"; \
1460             echo "  the Isabelle component configuration does not contain"; \
1461             echo "  [$(ISABELLE_TARGET_DIR)]"; \
1462           fi)
1463
1464 install-isabelle: $(GENERATED_PREFIX_ISABELLE)/last_build
1465
1466 install_local:: install-isabelle
1467 install:: install-isabelle
1468
1469 endif
1470
1471 all: drivers/isabelle-realizations.aux
1472
1473 install-data::
1474         $(INSTALL_DATA) drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/
1475
1476 clean-isabelle::
1477         rm -f $(GENERATED_PREFIX_ISABELLE)/*/*.xml
1478
1479 clean:: clean-isabelle
1480         rm -f drivers/isabelle-realizations.aux
1481
1482 #######################
1483 # Isabelle client
1484 #######################
1485
1486 ISABELLEC_FILES := isabelle_client_main
1487
1488 ISABELLECMODULES := $(addprefix src/isabelle-client/, $(ISABELLEC_FILES))
1489 ISABELLECDEP = $(addsuffix .dep, $(ISABELLECMODULES))
1490 ISABELLECCMO = $(addsuffix .cmo, $(ISABELLECMODULES))
1491 ISABELLECCMX = $(addsuffix .cmx, $(ISABELLECMODULES))
1492
1493 $(ISABELLECDEP) $(ISABELLECCMO) $(ISABELLECCMX): INCLUDES += -I src/isabelle-client -I src/util
1494
1495 depend: $(ISABELLECDEP)
1496 CLEANDIRS += src/isabelle-client
1497
1498 # build targets
1499
1500 byte: bin/isabelle_client.byte
1501 opt:  bin/isabelle_client.opt
1502
1503 bin/isabelle_client.opt: lib/why3/why3.cmxa $(ISABELLECCMX)
1504
1505 bin/isabelle_client.byte: lib/why3/why3.cma $(ISABELLECCMO)
1506
1507 install-bin::
1508         cp -f bin/isabelle_client.@OCAMLBEST@ $(BINDIR)/isabelle_client$(EXE)
1509
1510 uninstall-bin::
1511         rm -f $(BINDIR)/isabelle_client$(EXE)
1512
1513 MAKEINC += $(ISABELLECDEP)
1514
1515 clean::
1516         rm -f bin/isabelle_client.byte bin/isabelle_client.opt bin/isabelle_client
1517
1518 ################
1519 # Jessie3 plugin
1520 ################
1521
1522 ifeq (@enable_frama_c@,yes)
1523
1524 nobyte: jessie.byte
1525 noopt: jessie.opt
1526
1527 jessie.byte: src/jessie/Makefile $(WHY3CMA)
1528         @$(MAKE) -C src/jessie Jessie3.cma
1529
1530 jessie.opt: src/jessie/Makefile $(WHY3CMXA)
1531         @$(MAKE) -C src/jessie Jessie3.cmxs
1532
1533 uninstall-framac:
1534         rm -f $(FRAMAC_LIBDIR)/plugins/Jessie3.*
1535
1536 uninstall:: uninstall-framac
1537
1538 install-framac:
1539         $(MKDIR_P) $(FRAMAC_LIBDIR)/plugins/
1540         $(INSTALL_DATA) $(wildcard $(addprefix src/jessie/Jessie3., $(INSTALLED_LIB_EXTS))) \
1541           $(FRAMAC_LIBDIR)/plugins/
1542
1543 install:: install-framac
1544
1545 clean::
1546         $(MAKE) -C src/jessie clean
1547
1548 endif
1549
1550 ###############
1551 # Why3 pp
1552 ###############
1553
1554 PRETTYPRINT_FILES = why3pp
1555
1556 PRETTYPRINTMODULES = $(addprefix src/tools/, $(PRETTYPRINT_FILES))
1557
1558 PRETTYPRINTDEP = $(addsuffix .dep, $(PRETTYPRINTMODULES))
1559 PRETTYPRINTCMO = $(addsuffix .cmo, $(PRETTYPRINTMODULES))
1560 PRETTYPRINTCMX = $(addsuffix .cmx, $(PRETTYPRINTMODULES))
1561
1562 $(PRETTYPRINTDEP) $(PRETTYPRINTCMO) $(PRETTYPRINTCMX): INCLUDES += -I src/tools
1563
1564 # build targets
1565
1566 byte: bin/why3pp.cma
1567 opt:  bin/why3pp.cmxs
1568
1569 bin/why3pp.cmxs: $(PRETTYPRINTCMX)
1570 bin/why3pp.cma:  $(PRETTYPRINTCMO)
1571
1572 # depend and clean targets
1573
1574 MAKEINC += $(PRETTYPRINTDEP)
1575
1576 uninstall-bin::
1577         rm -f $(TOOLDIR)/why3pp.$(SHAREDBEST)
1578
1579 install-bin::
1580         $(MKDIR_P) $(TOOLDIR)
1581         $(INSTALL_DATA) bin/why3pp.$(SHAREDBEST) $(TOOLDIR)
1582
1583 install_local:: bin/why3pp.$(SHAREDBEST)
1584
1585 #########
1586 # why3doc
1587 #########
1588
1589 WHY3DOCGENERATED = src/why3doc/doc_lexer.ml
1590
1591 WHY3DOC_FILES = doc_html doc_def doc_lexer doc_main
1592
1593 WHY3DOCMODULES = $(addprefix src/why3doc/, $(WHY3DOC_FILES))
1594
1595 WHY3DOCDEP = $(addsuffix .dep, $(WHY3DOCMODULES))
1596 WHY3DOCCMO = $(addsuffix .cmo, $(WHY3DOCMODULES))
1597 WHY3DOCCMX = $(addsuffix .cmx, $(WHY3DOCMODULES))
1598
1599 $(WHY3DOCDEP) $(WHY3DOCCMO) $(WHY3DOCCMX): INCLUDES += -I src/why3doc
1600
1601 $(WHY3DOCDEP): $(WHY3DOCGENERATED)
1602
1603 # build targets
1604
1605 byte: bin/why3doc.cma
1606 opt:  bin/why3doc.cmxs
1607
1608 bin/why3doc.cmxs: $(WHY3DOCCMX)
1609 bin/why3doc.cma:  $(WHY3DOCCMO)
1610
1611 # depend and clean targets
1612
1613 MAKEINC += $(WHY3DOCDEP)
1614
1615 CLEANDIRS += src/why3doc
1616 GENERATED += $(WHY3DOCGENERATED)
1617
1618 uninstall-bin::
1619         rm -f $(TOOLDIR)/why3doc.$(SHAREDBEST)
1620
1621 install-bin::
1622         $(MKDIR_P) $(TOOLDIR)
1623         $(INSTALL_DATA) bin/why3doc.$(SHAREDBEST) $(TOOLDIR)
1624
1625 install_local:: bin/why3doc.$(SHAREDBEST)
1626
1627 #########
1628 # trywhy3
1629 #########
1630
1631 ifeq ($(DEBUGJS),yes)
1632  JSOO_DEBUG=--pretty --debug-info --source-map
1633  JS_MAPS=trywhy3.map why3_worker.map
1634 else
1635  JSOO_DEBUG=
1636  JS_MAPS=
1637 endif
1638
1639 TRYWHY3_FILES = json_base json_parser json_lexer bindings shortener trywhy3 why3_worker worker_proto
1640
1641 TRYWHY3MODULES = $(addprefix src/trywhy3/, $(TRYWHY3_FILES))
1642
1643 TRYWHY3DEP = $(addsuffix .dep, $(TRYWHY3MODULES))
1644 TRYWHY3CMO = $(addsuffix .cmo, $(TRYWHY3MODULES))
1645 TRYWHY3CMI = $(addsuffix .cmi, $(TRYWHY3MODULES))
1646
1647 $(TRYWHY3DEP) $(TRYWHY3CMO) $(TRYWHY3CMI): INCLUDES += -I src/trywhy3
1648
1649 TRYWHY3_COMMON_PACK = \
1650         trywhy3.js trywhy3.html trywhy3.css trywhy3_custom.css \
1651         help_whyml.html help_python.html help_micro-C.html \
1652         why3_worker.js \
1653         examples/ \
1654          $(JS_MAPS)
1655
1656 TRYWHY3_SMALL_PACK = \
1657         $(TRYWHY3_COMMON_PACK) \
1658         mode-why3.js
1659
1660 TRYWHY3_FULL_PACK = \
1661         $(TRYWHY3_COMMON_PACK) \
1662         alt-ergo-worker.js \
1663         ace-builds/src-min-noconflict/ace.js \
1664         ace-builds/src-min-noconflict/mode-why3.js \
1665         ace-builds/src-min-noconflict/mode-python.js \
1666         ace-builds/src-min-noconflict/mode-c_cpp.js \
1667         ace-builds/src-min-noconflict/theme-chrome.js
1668
1669 trywhy3.tar.gz: $(addprefix src/trywhy3/, $(TRYWHY3_SMALL_PACK))
1670         tar czf $@ -C src $(addprefix trywhy3/, $(TRYWHY3_SMALL_PACK))
1671
1672 trywhy3-full.tar.gz: $(addprefix src/trywhy3/, $(TRYWHY3_FULL_PACK))
1673         tar czf $@ -C src $(addprefix trywhy3/, $(TRYWHY3_FULL_PACK))
1674
1675 trywhy3: src/trywhy3/trywhy3.js src/trywhy3/why3_worker.js
1676
1677 src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
1678         js_of_ocaml $(JSOO_DEBUG) --Werror $<
1679
1680 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)
1681         $(OCAMLFIND) ocamlc -o $@ -package js_of_ocaml -package menhirLib -linkpkg $^
1682
1683 src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte src/trywhy3/trywhy3.conf src/trywhy3/try_alt_ergo.drv
1684         js_of_ocaml $(JSOO_DEBUG) --Werror --extern-fs -I . -I src/trywhy3 \
1685                 --file=trywhy3.conf:/ \
1686                 --file=try_alt_ergo.drv:/ \
1687           `find stdlib -name "*.mlw" -exec printf " --file=%s:/%s" {} {} ";"` \
1688         +dynlink.js +toplevel.js $<
1689
1690 src/trywhy3/why3_worker.byte: $(WHY3CMA) $(PYTHONCMO) $(MICROCCMO) \
1691                 $(addprefix src/trywhy3/, bindings.cmo worker_proto.cmo why3_worker.cmo)
1692         $(OCAMLFIND) ocamlc $(filter-out -thread,$(BFLAGS)) -package js_of_ocaml -o $@ -linkpkg $^
1693
1694 src/trywhy3/%.cmo: src/trywhy3/%.ml
1695         $(OCAMLFIND) ocamlc $(BFLAGS) -c $<
1696
1697 src/trywhy3/%.cmi: src/trywhy3/%.mli
1698         $(OCAMLFIND) ocamlc $(BFLAGS) -c $<
1699
1700 $(addprefix src/trywhy3/, worker_proto.cmo why3_worker.cmo): BFLAGS += -package js_of_ocaml
1701
1702 $(addprefix src/trywhy3/, bindings.cmo trywhy3.cmo): BFLAGS += -package js_of_ocaml -package js_of_ocaml-ppx
1703
1704 TRYWHY3JSON_FILES = json_base json_parser json_lexer
1705 TRYWHY3JSON = $(TRYWHY3JSON_FILES:%=src/trywhy3/%.ml) $(TRYWHY3JSON_FILES:%=src/trywhy3/%.mli)
1706
1707 $(TRYWHY3JSON): src/trywhy3/%: src/util/%
1708         cp $< $@
1709
1710 GENERATED += $(TRYWHY3JSON)
1711
1712 $(TRYWHY3DEP): $(TRYWHY3JSON)
1713
1714 MAKEINC += $(TRYWHY3DEP)
1715
1716 clean-trywhy3:
1717         rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte \
1718           src/trywhy3/why3_worker.js src/trywhy3/why3_worker.byte \
1719           trywhy3.tar.gz
1720
1721 clean:: clean-trywhy3
1722
1723 CLEANDIRS += src/trywhy3
1724
1725
1726 #########
1727 # why3webserver and full web/js interface
1728 #########
1729
1730 ifeq (@enable_web_ide@,yes)
1731
1732 JSOCAMLCW=$(OCAMLFIND) ocamlc -package js_of_ocaml -package js_of_ocaml-ppx \
1733         -I src/ide
1734
1735 src/ide/why3_js.cmo: src/ide/why3_js.ml lib/why3/why3.cma
1736         $(JSOCAMLCW) $(BFLAGS) -c $<
1737
1738 src/ide/why3_js.byte: lib/why3/why3.cma src/ide/why3_js.cmo
1739         $(JSOCAMLCW) $(filter-out -thread,$(BFLAGS)) -o $@ -linkpkg $(BLINKFLAGS) $^
1740
1741 src/ide/why3_js.js: src/ide/why3_js.byte
1742         js_of_ocaml +dynlink.js +toplevel.js $<
1743
1744 web_ide: src/ide/why3_js.js
1745
1746 opt: bin/why3webserver.cmxs
1747 byte: bin/why3webserver.cma src/ide/why3_js.cmo
1748
1749 endif
1750
1751 ########
1752 # bench
1753 ########
1754
1755 .PHONY: bench test
1756
1757 bench:: bin/why3.@OCAMLBEST@ bin/why3config.$(SHAREDBEST) plugins $(TOOLS) \
1758   share/Makefile.config bin/why3extract.$(SHAREDBEST)
1759         bin/why3.@OCAMLBEST@ config list-provers | grep -q Alt-Ergo || \
1760                 bin/why3.@OCAMLBEST@ config detect
1761         @echo "=== Check API examples ==="
1762         $(MAKE) bench-api
1763         @echo "=== Check examples ==="
1764         bash bench/bench -suffix ".@OCAMLBEST@"
1765         @echo "=== Check parsing messages ==="
1766         bench/parsing-bench
1767
1768 APITESTS = \
1769         clone \
1770         counterexample \
1771         create_session \
1772         logic \
1773         mlw_expr \
1774         mlw_tree \
1775         transform
1776
1777 ifeq (@enable_infer@,yes)
1778         APITESTS += mlw_tree_infer_invs
1779 endif
1780
1781 ifeq (@enable_infer@,yes)
1782         APITESTS += mlw_tree_bddinfer_invs
1783 endif
1784
1785 ifeq (@enable_sexp@,yes)
1786         APITESTS += epsilon
1787 endif
1788
1789 bench-api: $(addprefix test-api-, $(APITESTS))
1790
1791 clean::
1792         rm -rf bench/infer/*.out
1793         rm -rf bench/bddinfer/*.out
1794         rm -rf bench/check-ce/*.out
1795
1796 ###############
1797 # test targets
1798 ###############
1799
1800 test-itp.opt: src/printer/itp.ml lib/why3/why3.cmxa
1801         $(if $(QUIET),@echo 'Ocamlopt $<' &&) \
1802         $(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(OLINKFLAGS) lib/why3/why3.cmxa $<
1803
1804 test-api-%.byte: examples/use_api/%.ml lib/why3/why3.cma
1805         $(SHOW) 'Ocaml    $<'
1806         $(HIDE)($(OCAMLC) -o $@ -I lib/why3 $(BFLAGS) $(BLINKFLAGS) lib/why3/why3.cma $<) \
1807                 || (printf "Compilation failed for API test $@. Please fix it.\n"; exit 2)
1808
1809 test-api-%.opt: examples/use_api/%.ml lib/why3/why3.cmxa
1810         $(SHOW) 'Ocamlopt $<'
1811         $(HIDE)($(OCAMLOPT) -o $@ -I lib/why3 $(OFLAGS) $(OLINKFLAGS) lib/why3/why3.cmxa $<) \
1812                 || (printf "Compilation failed for API test $@. Please fix it.\n"; exit 2)
1813
1814 test-api-%: test-api-%.@OCAMLBEST@
1815         $(HIDE)mkdir -p examples/use_api/results
1816         $(HIDE)(./$< | sed -e 's/^\(Versions of Alt-Ergo found: \).*$$/\1<hidden>/' \
1817                            -e 's/0\.0[0-9]/<hidden>/g;s/[0-9]\+ steps/<hidden> steps/' \
1818                             > examples/use_api/results/$@.stdout ) \
1819                 || (printf "Execution failed for API test $<. Please fix it.\n"; exit 2)
1820         $(HIDE)(diff -u examples/use_api/oracles/$@.stdout examples/use_api/results/$@.stdout) \
1821                 || (printf "Oracle updated for API test $<. Please review it.\n"; cp examples/use_api/results/$@.stdout examples/use_api/oracles/$@.stdout )
1822         $(HIDE)rm -f $< why3session.xml why3shapes why3shapes.gz
1823
1824
1825 #test-shape: lib/why3/why3.cma
1826 #       ocaml -I lib/why3 $(INCLUDES) $(BLINKFLAGS) $? examples/test_shape.ml
1827
1828
1829 ################
1830 # documentation
1831 ################
1832
1833 .PHONY: doc predoc update-doc-png clean-doc
1834
1835 doc/generated/drivers-all.dot: drivers/*.drv drivers/*.gen
1836         doc/drv_depgraph $^ > $@
1837
1838 doc/generated/drivers-%.dot: doc/generated/drivers-all.dot
1839         ccomps -X $(NODE) $< > $@
1840
1841 doc/generated/drivers-smt.dot: NODE = smt-libv2.gen
1842 doc/generated/drivers-tptp.dot: NODE = tptp.gen
1843 doc/generated/drivers-coq.dot: NODE = coq-common.gen
1844 doc/generated/drivers-isabelle.dot: NODE = isabelle-common.gen
1845 doc/generated/drivers-pvs.dot: NODE = pvs-common.gen
1846
1847 DRVDOT = $(patsubst %,doc/generated/drivers-%.dot, smt tptp coq isabelle pvs)
1848
1849 DOC = index zebibliography genindex \
1850   foreword starting whyml api install manpages syntaxref vcgen \
1851   input_formats exec itp technical changes
1852
1853 DOCRST = $(DOC:%=doc/%.rst) doc/manual.bib
1854
1855 LIBDOT = $(patsubst %,doc/generated/library-%.dot, int array)
1856
1857 doc/generated/library-%.dot: stdlib/%.mlw
1858         bin/why3 pp --output=dep $< | tred > $@
1859
1860 predoc: $(DRVDOT) $(LIBDOT)
1861
1862 update-doc-png:
1863         export UBUNTU_MENUPROXY=0; \
1864         export WHY3CONFIG=doc/why3ide-doc.conf; \
1865         export WHY3LOADPATH=stdlib; \
1866         export GTK_THEME=Adwaita; \
1867         export WAYLAND_DISPLAY=; \
1868         sed -n -e 's/^.. %EXECUTE \(.*\)/\1/p' $(DOCRST) | $(SHELL) -e
1869
1870 ifeq (@enable_doc@,yes)
1871
1872 doc: doc/html/index.html
1873
1874 TESTSAPIDOC = $(addsuffix .ml, $(addprefix examples/use_api/, $(APITESTS)))
1875
1876 doc/html/index.html: $(DOCRST) $(DRVDOT) $(LIBDOT) $(TESTSAPIDOC) doc/conf.py
1877         $(SPHINX) -b html -d doc/.doctrees doc doc/html
1878
1879 doc/latex/manual.tex: $(DOCRST) $(DRVDOT) $(LIBDOT) $(TESTSAPIDOC) doc/conf.py
1880         $(SPHINX) -b latex -d doc/.doctrees doc doc/latex
1881
1882 ifeq (@enable_pdf_doc@,yes)
1883
1884 doc: doc/latex/manual.pdf
1885
1886 doc/latex/manual.pdf: doc/latex/manual.tex
1887         @echo "running LaTeX compilation..."
1888         cd doc/latex; $(LATEXCOMP) manual.tex >/dev/null
1889 ifeq (@LATEX@,pdflatex)
1890         @cd doc/latex; if grep 'may have changed. Rerun to get' manual.log; then \
1891           makeindex manual; \
1892           echo "running LaTeX again to try to fix references..."; \
1893           pdflatex manual >/dev/null; \
1894         fi
1895         @cd doc/latex; if grep 'may have changed. Rerun to get' manual.log; then \
1896           echo "running LaTeX again to try to fix references..."; \
1897           pdflatex manual >/dev/null; \
1898         fi
1899 endif
1900
1901 endif
1902
1903 else
1904
1905 doc:
1906
1907 endif
1908
1909 clean-doc:
1910         rm -rf doc/html doc/latex
1911         rm -rf doc/generated/*.dot
1912
1913 clean:: clean-doc
1914
1915 ##########
1916 # API DOC
1917 ##########
1918
1919 .PHONY: apidoc apidot
1920
1921 MODULESTODOC = \
1922         util/util util/opt util/lists util/strings util/getopt \
1923         util/extmap util/extset util/exthtbl \
1924         util/weakhtbl util/wstdlib util/rc util/debug \
1925         util/loc util/pp util/bigInt util/number \
1926         util/mlmpfr_wrapper \
1927         core/ident core/ty core/term core/decl core/coercion core/theory \
1928         core/env core/task core/trans core/pretty core/printer \
1929         core/model_parser \
1930         parser/ptree.ml \
1931         parser/ptree_helpers parser/typing parser/mlw_printer \
1932         driver/whyconf driver/call_provers driver/driver \
1933         transform/args_wrapper \
1934         mlw/ity mlw/expr mlw/pdecl mlw/pmodule mlw/vc \
1935         mlw/pinterp_core mlw/rac mlw/pinterp mlw/check_ce \
1936         session/session_itp session/controller_itp \
1937         session/itp_communication session/itp_server \
1938         session/strategy
1939
1940 ifeq (@enable_bddinfer@,yes)
1941         MODULESTODOC += bddinfer/why3infer
1942 endif
1943
1944 FILESTODOC = $(subst .ml.mli,.ml,$(MODULESTODOC:%=src/%.mli))
1945
1946 DOCFLAGS = -sort $(INCLUDES) $(LIBINCLUDES)
1947
1948 ifeq (@enable_ocamlfind@,yes)
1949         DOCFLAGS += $(addprefix -package ,$(EXTPKGS))
1950 else
1951         DOCFLAGS += $(EXTINCLUDES)
1952 endif
1953
1954 doc/apidoc:
1955         mkdir -p doc/apidoc
1956
1957 apidoc: doc/apidoc $(FILESTODOC)
1958         $(OCAMLDOC) $(DOCFLAGS) -d doc/apidoc -charset utf-8 -html \
1959                 -t "Why3 API documentation" -keep-code $(FILESTODOC)
1960
1961 # could we include also the dependency graph ? -- someone
1962 # At least we can give a way to create it -- francois
1963
1964 apidot: doc/apidoc/dg.svg doc/apidoc/dg.png
1965
1966 #The sed remove configuration for dot that gives bad result
1967 doc/apidoc/dg.dot: doc/apidoc $(FILESTODOC)
1968         $(OCAMLDOC) $(DOCFLAGS) -o doc/apidoc/dg.dot.tmp -dot $(FILESTODOC)
1969         sed -e "s/  \(size\|ratio\|rotate\|fontsize\).*$$//" doc/apidoc/dg.dot.tmp \
1970           | tred > doc/apidoc/dg.dot
1971         rm -f doc/apidoc/dg.dot.tmp
1972
1973 doc/apidoc/dg.svg: doc/apidoc/dg.dot
1974         dot -T svg $< > $@
1975
1976 doc/apidoc/dg.png: doc/apidoc/dg.dot
1977         dot -T png $< > $@
1978
1979 doc/apidoc.tex: $(FILESTODOC)
1980         $(OCAMLDOC) $(DOCFLAGS) -o doc/apidoc.tex -latex -noheader -notrailer $(FILESTODOC)
1981
1982 clean::
1983         rm -f doc/apidoc/*
1984
1985 ##########
1986 # Install rules for bash completions
1987 ##########
1988
1989 uninstall-bash:
1990         if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then \
1991           rm -f /etc/bash_completion.d/why3; \
1992         fi
1993
1994 uninstall:: uninstall-bash
1995
1996 install-bash::
1997         if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then \
1998           $(INSTALL) share/bash/why3 /etc/bash_completion.d; \
1999         fi
2000
2001 install:: install-bash
2002
2003 ##########
2004 # Stdlib formatted with why3doc
2005 ##########
2006
2007 .PHONY: stdlibdoc
2008
2009 STDMACHLIBS = \
2010         array bv c float fxp int matrix onetime peano tagset
2011
2012 STDLIBS = \
2013         algebra array \
2014         bag bintree bool bv \
2015         cursor \
2016         exn \
2017         floating_point fmap function \
2018         graph hashtbl \
2019         ieee_float int io \
2020         list \
2021         map matrix \
2022         number \
2023         ocaml option \
2024         pigeon pqueue \
2025         queue \
2026         random real ref regexp relations \
2027         seq set stack string \
2028         tree \
2029         ufloat \
2030         witness \
2031         $(addprefix mach/, $(STDMACHLIBS))
2032
2033 # NO NEED DOC:
2034 # debug: too basic, needs large improvement
2035 # tptp: for TPTP provers ?
2036 # for_drivers: used only in drivers
2037
2038 STDLIBFILES = $(patsubst %,stdlib/%.mlw, $(STDLIBS))
2039
2040 # TODO: remove the hack about int.mlw once it has become builtin
2041 stdlibdoc: $(STDLIBFILES) bin/why3.@OCAMLBEST@ bin/why3doc.$(SHAREDBEST)
2042         mkdir -p doc/stdlibdoc
2043         sed -e "s/use Int/use int.Int/" stdlib/int.mlw > int.mlw
2044         rm -f doc/stdlibdoc/style.css
2045         WHY3CONFIG="" bin/why3.@OCAMLBEST@ doc $(LOCAL_STDLIB) \
2046           -o doc/stdlibdoc --title="Why3 Standard Library" \
2047           $(subst stdlib/int.mlw,int.mlw,$(STDLIBFILES))
2048         rm int.mlw
2049         cd doc/stdlibdoc; \
2050           for f in stdlib.*.html; \
2051             do mv "$$f" "$${f#stdlib.}"; done
2052         sed -i -e "s#stdlib.##g" doc/stdlibdoc/index.html
2053         sed -i -e "s#int\.\(<a href=\"\)int\.html#\1#g" doc/stdlibdoc/int.html
2054
2055 clean::
2056         rm -f doc/stdlibdoc/*
2057
2058 ################
2059 # generic rules
2060 ################
2061
2062 %.cmi: %.mli
2063         $(SHOW) 'Ocamlc   $<'
2064         $(HIDE)$(OCAMLC) -c $(BFLAGS) $<
2065
2066 # suppress "unused rec" warning for Menhir-produced files
2067 %.cmo: %.ml %.mly
2068         $(SHOW) 'Ocamlc   $<'
2069         $(HIDE)$(OCAMLC) -c $(BFLAGS) -w -39 $<
2070
2071 # suppress "unused rec" warning for Menhir-produced files
2072 %.cmx: %.ml %.mly
2073         $(SHOW) 'Ocamlopt $<'
2074         $(HIDE)$(OCAMLOPT) -c $(OFLAGS) -w -39 $(CMIHACK) $<
2075
2076 %.cmo: %.ml
2077         $(SHOW) 'Ocamlc   $<'
2078         $(HIDE)$(OCAMLC) -c $(BFLAGS) $<
2079
2080 %.cmx: %.ml %.mli
2081         $(SHOW) 'Ocamlopt $<'
2082         $(HIDE)$(OCAMLOPT) -c $(OFLAGS) $<
2083
2084 %.cmx: %.ml
2085         $(SHOW) 'Ocamlopt $<'
2086         $(HIDE)$(OCAMLOPT) -c $(OFLAGS) $(CMIHACK) $<
2087
2088 %.cma:
2089         $(SHOW) 'Linking  $@'
2090         $(HIDE)$(OCAMLC) -a $(BFLAGS) -o $@ $^
2091
2092 %.cmxa:
2093         $(SHOW) 'Linking  $@'
2094         $(HIDE)$(OCAMLOPT) -a $(OFLAGS) -o $@ $^
2095
2096 %.cmxs:
2097         $(SHOW) 'Linking  $@'
2098         $(HIDE)$(OCAMLOPT) -shared $(OFLAGS) -o $@ $^
2099
2100 %.ml: %.mll
2101         $(SHOW) 'Ocamllex $<'
2102         $(HIDE)$(OCAMLLEX) $<
2103
2104 # the % below are not a typo; they are a way to force Make to consider all the targets at once
2105 src/c%re/parser_tokens.ml src/c%re/parser_tokens.mli: src/parser/parser_common.mly
2106         $(SHOW) 'Menhir $^'
2107         $(HIDE)$(MENHIR) --base src/core/parser_tokens --only-tokens $^
2108
2109 src/p%rser/parser.ml src/p%rser/parser.mli: $(PARSERS)
2110         $(SHOW) 'Menhir $^'
2111         $(HIDE)$(MENHIR) --table --explain --strict --base src/parser/parser \
2112                 --external-tokens Parser_tokens $^
2113
2114 pl%gins/cfg/cfg_parser.ml pl%gins/cfg/cfg_parser.mli: src/parser/parser_common.mly plugins/cfg/cfg_parser.mly
2115         $(SHOW) 'Menhir $^'
2116         $(HIDE)$(MENHIR) --table --explain --strict --base plugins/cfg/cfg_parser $^
2117         $(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
2118
2119 pl%gins/coma/coma_parser.ml pl%gins/coma/coma_parser.mli: src/parser/parser_common.mly plugins/coma/coma_parser.mly
2120         $(SHOW) 'Menhir $^'
2121         $(HIDE)$(MENHIR) --table --explain --strict --base plugins/coma/coma_parser $^
2122         $(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
2123
2124 %.ml %.mli: %.mly
2125         $(SHOW) 'Menhir $<'
2126         $(HIDE)$(MENHIR) --table --explain --strict $<
2127
2128 %.dep: %.ml %.mli
2129         $(SHOW) 'Ocamldep $<'
2130         $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(INCLUDES) $< $<i $(TOTARGET)
2131
2132 %.dep: %.ml
2133         $(SHOW) 'Ocamldep $<'
2134         $(HIDE)($(OCAMLDEP) $(DEPFLAGS) $(INCLUDES) $<; \
2135                 echo '$*.cmx : $*.cmi'; \
2136                 echo '$*.cmi : $*.cmo') $(TOTARGET)
2137
2138 %.dep: %.mli
2139         $(SHOW) 'Ocamldep $<'
2140         $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(INCLUDES) $< $(TOTARGET)
2141
2142 bin/%.opt:
2143         $(SHOW) 'Linking  $@'
2144         $(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
2145
2146 bin/%.byte:
2147         $(SHOW) 'Linking  $@'
2148         $(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
2149
2150 # .ml4.ml:
2151 #       $(CAMLP4) pr_o.cmo -impl $< > $@
2152
2153 # jc/jc_ai.ml: jc/jc_annot_inference.ml jc/jc_annot_fail.ml Makefile
2154 #       if test "@enable_apron@" = "yes" ; then \
2155 #         echo "# 1 \"jc/jc_annot_inference.ml\"" > jc/jc_ai.ml; \
2156 #         cat jc/jc_annot_inference.ml >> jc/jc_ai.ml; \
2157 #       else \
2158 #         echo "# 1 \"jc/jc_annot_fail.ml\"" > jc/jc_ai.ml; \
2159 #         cat jc/jc_annot_fail.ml >> jc/jc_ai.ml; \
2160 #       fi
2161
2162 # %_why.v: %.mlw $(BINARY)
2163 #       $(BINARY) -coq $*.mlw
2164
2165 # %_why.pvs: %.mlw $(BINARY)
2166 #       $(BINARY) -pvs $*.mlw
2167
2168 # Emacs tags
2169 ############
2170
2171 tags:
2172         find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
2173         etags "--regex-ocaml=/let[ \t]+\([^ \t]+\)/\1/" \
2174               "--regex-ocaml=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
2175               "--regex-ocaml=/and[ \t]+\([^ \t]+\)/\1/" \
2176               "--regex-ocaml=/type[ \t]+\([^ \t]+\)/\1/" \
2177               "--regex-ocaml=/exception[ \t]+\([^ \t]+\)/\1/" \
2178               "--regex-ocaml=/val[ \t]+\([^ \t]+\)/\1/" \
2179               "--regex-ocaml=/module[ \t]+\([^ \t]+\)/\1/"
2180
2181 otags:
2182         find \( -name '*.ml' -or -name '*.mli' \) -print0 | xargs -0 otags
2183 #       otags src/*.mli src/*.ml c/*.mli c/*.ml intf/*.mli intf/*.ml
2184
2185 # the previous seems broken. This one is intented for vi(m) users, but could
2186 # be adapted for emacs (remove the -vi option ?)
2187 otags-vi:
2188         find \( -name '*.ml' -or -name '*.mli' \) -print0 | xargs -0 otags -vi
2189
2190 wc:
2191         ocamlwc -p src/*.ml* src/*/*.ml*
2192
2193 #dep: depend
2194 #       cat .depend* | ocamldot | dot -Tpdf > dep.pdf
2195 #       $(PDFVIEWER) dep.pdf
2196
2197 # distrib
2198 #########
2199
2200 NAME = why3-@VERSION@
2201 # see .gitattributes for the list of files that are not distributed
2202 MORE_DIST = configure
2203
2204 dist: $(MORE_DIST)
2205         rm -f distrib/$(NAME).tar.gz
2206         mkdir -p distrib/
2207         git archive --format=tar --prefix=$(NAME)/ -o distrib/$(NAME).tar HEAD
2208         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)
2209         gzip -n -f --best distrib/$(NAME).tar
2210
2211
2212 ###############
2213 # file headers
2214 ###############
2215
2216 headers:
2217         headache -c misc/headache_config.txt -h misc/header.txt \
2218                 Makefile.in configure.in \
2219                 src/*/*.ml src/*/*.ml[ily] \
2220                 plugins/*/*.ml plugins/*/*.ml[ily] \
2221                 lib/coq/*.v lib/coq/*/*.v \
2222                 src/server/*.[ch] \
2223                 examples/use_api/*.ml
2224
2225 #########
2226 # myself
2227 #########
2228
2229 AUTOCONF_FILES = \
2230         Makefile \
2231         src/jessie/Makefile \
2232         src/config.sh \
2233         .merlin \
2234         src/jessie/.merlin \
2235         lib/why3/META \
2236         lib/coq/version \
2237         lib/pvs/version
2238
2239 $(AUTOCONF_FILES): %: %.in config.status
2240         ./config.status chmod --file $@
2241
2242 src/util/config.ml share/Makefile.config: src/config.sh
2243         $(SHOW) 'Generate $@'
2244         $(HIDE)BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
2245
2246 clean::
2247         rm -f share/Makefile.config
2248
2249 config.status: configure
2250         ./config.status --recheck
2251
2252 configure: configure.in
2253         autoconf -f
2254
2255 ###################
2256 # clean and depend
2257 ###################
2258
2259 .PHONY: distclean
2260
2261 distclean: clean
2262         rm -f config.status config.cache config.log \
2263             src/util/config.ml $(AUTOCONF_FILES)
2264
2265 ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
2266 ifneq "$(MAKECMDGOALS)" "depend"
2267 -include $(MAKEINC)
2268 endif
2269 endif
2270
2271 depend: $(MAKEINC)
2272
2273 clean::
2274         rm -f $(GENERATED)
2275         $(foreach d,$(CLEANDIRS),rm -f $(addprefix $(d)/*.,$(COMPILED_LIB_EXTS));)
2276         $(foreach p,$(CLEANLIBS),rm -f $(addprefix $(p).,$(COMPILED_LIB_EXTS));)
2277
2278 detect-unused:
2279         @L1=$$(mktemp); \
2280         L2=$$(mktemp); \
2281         for d in `find examples/ -name 'why3session.xml' -printf '%h\n'`; do \
2282           sed -n -e 's/.*proof.*name="\([^"]*\)".*/\1/p' $$d/why3session.xml | sort > $$L1; \
2283           (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; \
2284           diff -u --label="$$d/why3session.xml" --label="$$d/" $$L1 $$L2 || echo; \
2285         done; \
2286         rm $$L1 $$L2
2287
2288 ##################################################################
2289 # Building the Why3 platform with ocamlbuild (OCaml 3.10 needed) #
2290 ##################################################################
2291
2292 # There used to be targets here but they are no longer useful.
2293
2294 # To build using Ocamlbuild:
2295 # 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
2296 # are generated.
2297 # 2) Run Ocamlbuild with any target to generate the sanitization script.
2298 # 3) Run ./sanitize to delete the generated files that shouldn't be generated
2299 # (i.e. all lexers and parsers).
2300 # 4) Run Ocamlbuild with the target you need, for example:
2301 # ocamlbuild jc/jc_main.native
2302
2303 # You can also use the Makefile ./build.makefile which has some handy targets.