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