Makefile.in

   1 ##########################################################################
   2 #                                                                        #
   3 #  Copyright (C) 2010-2012                                               #
   4 #    François Bobot                                                      #
   5 #    Jean-Christophe Filliâtre                                           #
   6 #    Claude Marché                                                       #
   7 #    Guillaume Melquiond                                                 #
   8 #    Andrei Paskevich                                                    #
   9 #                                                                        #
  10 #  This software is free software; you can redistribute it and/or        #
  11 #  modify it under the terms of the GNU Library General Public           #
  12 #  License version 2.1, with the special exception on linking            #
  13 #  described in file LICENSE.                                            #
  14 #                                                                        #
  15 #  This software is distributed in the hope that it will be useful,      #
  16 #  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
  17 #  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  #
  18 #                                                                        #
  19 ##########################################################################
  20
  21 include Version
  22
  23 VERBOSEMAKE ?= @enable_verbose_make@
  24
  25 ifeq ($(VERBOSEMAKE),yes)
  26   QUIET =
  27 else
  28   QUIET = yes
  29 endif
  30
  31 # install the binaries
  32 DESTDIR =
  33
  34 prefix      = @prefix@
  35 exec_prefix = @exec_prefix@
  36 datarootdir = @datarootdir@
  37
  38 BINDIR  = $(DESTDIR)@bindir@
  39 LIBDIR  = $(DESTDIR)@libdir@
  40 DATADIR = $(DESTDIR)@datarootdir@
  41 MANDIR  = $(DESTDIR)@mandir@
  42
  43 # OS specific stuff
  44 EXE   = @EXE@
  45
  46 # other variables
  47 CC        = @CC@
  48 OCAMLC    = @OCAMLC@
  49 OCAMLOPT  = @OCAMLOPT@
  50 OCAMLDEP  = @OCAMLDEP@
  51 OCAMLLEX  = @OCAMLLEX@
  52 OCAMLYACC = @OCAMLYACC@
  53 OCAMLDOC  = @OCAMLDOC@
  54 OCAMLLIB  = @OCAMLLIB@
  55 OCAMLBEST = @OCAMLBEST@
  56 OCAMLVERSION = @OCAMLVERSION@
  57 COQC      = @COQC@
  58 COQDEP    = @COQDEP@
  59 CAMLP5O   = @CAMLP5O@
  60
  61 DEPFLAGS  = -slash -I src
  62 ifeq (@OCAMLBEST@,opt)
  63 DEPFLAGS += -native
  64 endif
  65
  66 RUBBER = @RUBBER@
  67
  68 #PSVIEWER  = @PSVIEWER@
  69 #PDFVIEWER = @PDFVIEWER@
  70
  71 OFLAGS = -w Aer-29 -dtypes    -I src $(INCLUDES)
  72 BFLAGS = -w Aer-29 -dtypes -g -I src $(INCLUDES)
  73
  74 OLINKFLAGS = -linkall $(EXTCMXA)
  75 BLINKFLAGS = -linkall $(EXTCMA)
  76
  77 ifeq (@enable_debug@,yes)
  78 OFLAGS += -g
  79 endif
  80
  81 ifeq (@enable_profiling@,yes)
  82 OFLAGS += -g -p
  83 endif
  84
  85 # external libraries common to all binaries
  86
  87 EXTOBJS =
  88 EXTLIBS = str unix nums dynlink
  89
  90 EXTCMA  = $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
  91 EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
  92
  93 ###############
  94 # main target
  95 ###############
  96
  97 all: @OCAMLBEST@
  98 plugins: plugins.@OCAMLBEST@
  99 opt: plugins.opt
 100 byte: plugins.byte
 101
 102 ifeq (@enable_local@,yes)
 103 all: install_local
 104 endif
 105
 106 .PHONY: byte opt clean depend all install install_local install_no_local
 107 .PHONY: plugins plugins.byte plugins.opt
 108
 109 #############
 110 # Why library
 111 #############
 112
 113 LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
 114                src/parser/parser.mli src/parser/parser.ml \
 115                src/driver/driver_parser.mli src/driver/driver_parser.ml \
 116                src/driver/driver_lexer.ml src/session/xml.ml
 117
 118 LIB_UTIL = stdlib exn_printer pp debug loc print_tree \
 119            cmdline hashweak hashcons util sysutil rc plugin
 120
 121 LIB_CORE = ident ty term pattern decl theory task pretty env trans printer
 122
 123 LIB_PARSER = ptree denv glob typing parser lexer
 124
 125 LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
 126              whyconf autodetection
 127
 128 LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
 129                 inlining split_goal induction \
 130                 eliminate_definition eliminate_algebraic \
 131                 eliminate_inductive eliminate_let eliminate_if \
 132                 libencoding discriminate protect_finite \
 133                 encoding encoding_select \
 134                 encoding_decorate encoding_decoexp encoding_twin \
 135                 encoding_explicit encoding_guard encoding_sort \
 136                 encoding_instantiate simplify_array filter_trigger \
 137                 introduction abstraction close_epsilon lift_epsilon \
 138                 eval_match instantiate_predicate smoke_detector
 139
 140 LIB_PRINTER = print_number alt_ergo why3printer smtv1 smtv2 coq pvs \
 141                 simplify gappa cvc3 yices
 142
 143 LIB_SESSION = xml termcode session session_tools session_scheduler
 144
 145 LIBMODULES = src/config \
 146               $(addprefix src/util/, $(LIB_UTIL)) \
 147               $(addprefix src/core/, $(LIB_CORE)) \
 148               $(addprefix src/parser/, $(LIB_PARSER)) \
 149               $(addprefix src/driver/, $(LIB_DRIVER)) \
 150               $(addprefix src/transform/, $(LIB_TRANSFORM)) \
 151               $(addprefix src/printer/, $(LIB_PRINTER)) \
 152               $(addprefix src/session/, $(LIB_SESSION))
 153
 154 LIBDIRS = util core parser driver transform printer session
 155 LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
 156
 157 LIBDEP = $(addsuffix .dep, $(LIBMODULES))
 158 LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
 159 LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
 160
 161 $(LIBDEP): DEPFLAGS += $(LIBINCLUDES)
 162 $(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
 163 $(LIBCMX): OFLAGS += -for-pack Why3
 164
 165 $(LIBDEP): $(LIBGENERATED)
 166
 167 # build targets
 168
 169 byte: src/why3.cma
 170 opt:  src/why3.cmxa
 171
 172 src/why3.cma: src/why3.cmo
 173         $(if $(QUIET),@echo 'Linking  $@' &&) \
 174             $(OCAMLC) -a $(BFLAGS) -o $@ $^
 175
 176 src/why3.cmxa: src/why3.cmx
 177         $(if $(QUIET),@echo 'Linking  $@' &&) \
 178             $(OCAMLOPT) -a $(OFLAGS) -o $@ $^
 179
 180 src/why3.cmo: $(LIBCMO)
 181         $(if $(QUIET),@echo 'Linking  $@' &&) \
 182             $(OCAMLC) $(BFLAGS) -pack -o $@ $^
 183
 184 src/why3.cmx: $(LIBCMX)
 185         $(if $(QUIET),@echo 'Linking  $@' &&) \
 186             $(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
 187
 188 # clean and depend
 189
 190 ifneq "$(MAKECMDGOALS)" "clean"
 191 include $(LIBDEP)
 192 endif
 193
 194 depend: $(LIBDEP)
 195
 196 LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
 197 LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
 198            $(addsuffix /*.annot, $(LIBSDIRS)) \
 199            $(addsuffix /*.output, $(LIBSDIRS)) \
 200            $(addsuffix /*.automaton, $(LIBSDIRS)) \
 201            $(addsuffix /*.dep, $(LIBSDIRS)) \
 202            $(addsuffix /*.o, $(LIBSDIRS)) \
 203            $(addsuffix /*~, $(LIBSDIRS))
 204
 205 clean::
 206         rm -f $(LIBCLEAN) $(LIBGENERATED)
 207         rm -f src/why3.cm[aiox] src/why3.[ao] src/why3.cmxa
 208
 209 ###############
 210 # installation
 211 ###############
 212
 213 install_no_local::
 214         mkdir -p $(BINDIR)
 215         mkdir -p $(DATADIR)/why3/images
 216         mkdir -p $(DATADIR)/why3/images/boomy
 217         mkdir -p $(DATADIR)/why3/images/fatcow
 218         mkdir -p $(DATADIR)/why3/emacs
 219         mkdir -p $(DATADIR)/why3/lang
 220         mkdir -p $(DATADIR)/why3/theories
 221         mkdir -p $(DATADIR)/why3/modules
 222         mkdir -p $(DATADIR)/why3/drivers
 223         cp -f theories/*.why $(DATADIR)/why3/theories
 224         cp -f modules/*.mlw $(DATADIR)/why3/modules
 225         cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
 226         cp -f share/provers-detection-data.conf $(DATADIR)/why3/
 227         cp -f share/images/icons.rc $(DATADIR)/why3/images
 228         cp -f share/images/*.png $(DATADIR)/why3/images
 229         cp -f share/images/boomy/*.png $(DATADIR)/why3/images/boomy
 230         cp -f share/images/fatcow/*.png $(DATADIR)/why3/images/fatcow
 231         cp -f share/why3session.dtd $(DATADIR)/why3
 232         cp -rf share/javascript $(DATADIR)/why3/javascript
 233         cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el
 234         cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang
 235 #       if test -d /etc/bash_completion.d; then cp -f share/bash/why3 /etc/bash_completion.d; fi
 236
 237 install_no_local_lib::
 238         mkdir -p $(OCAMLLIB)/why3
 239         cp -f src/why3.cm* $(OCAMLLIB)/why3
 240         cp -f META $(OCAMLLIB)/why3
 241         if test -f src/why3.a; then cp -f src/why3.a $(OCAMLLIB)/why3; fi
 242         if test -f src/why3.o; then cp -f src/why3.o $(OCAMLLIB)/why3; fi
 243
 244 ifeq (@enable_local@,yes)
 245 install install-lib:
 246         @echo "Why is configured in local installation mode."
 247         @echo "To install Why, run ./configure --disable-local ; make ; make install"
 248 else
 249 install: install_no_local
 250 install-lib: install_no_local_lib
 251 endif
 252
 253 install-all: install install-lib
 254
 255 ##################
 256 # Why plugins
 257 ##################
 258
 259 PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
 260                 plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli
 261
 262 PLUG_PARSER = genequlin
 263 PLUG_PRINTER =
 264 PLUG_TRANSFORM =
 265 PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
 266
 267 PLUGINS = genequlin tptp
 268
 269 TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
 270
 271 TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
 272 TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
 273
 274 ifeq (@enable_hypothesis_selection@,yes)
 275 PLUG_TRANSFORM += hypothesis_selection
 276 PLUGINS += hypothesis_selection
 277
 278 lib/plugins/hypothesis_selection.cmxs: INCLUDES += -I @OCAMLGRAPHLIB@
 279 lib/plugins/hypothesis_selection.cmo:  INCLUDES += -I @OCAMLGRAPHLIB@
 280 lib/plugins/hypothesis_selection.cmxs: OFLAGS += graph.cmxa
 281 lib/plugins/hypothesis_selection.cmo:  BFLAGS += graph.cmo
 282 endif
 283
 284 PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
 285               $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
 286               $(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
 287               $(TPTPMODULES)
 288
 289 PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
 290 PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
 291 PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
 292
 293 PLUGDIRS = parser printer transform tptp
 294 PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))
 295
 296 $(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES)
 297 $(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES)
 298
 299 $(PLUGDEP): $(PLUGGENERATED)
 300
 301 plugins.byte: $(addsuffix .cmo, $(addprefix lib/plugins/, $(PLUGINS)))
 302 plugins.opt : $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))
 303
 304 lib/plugins/%.cmxs: plugins/parser/%.cmx
 305         $(if $(QUIET),@echo 'Linking  $@' &&) \
 306             $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
 307
 308 lib/plugins/%.cmo: plugins/parser/%.cmo
 309         $(if $(QUIET),@echo 'Linking  $@' &&) \
 310             $(OCAMLC) $(BFLAGS) -pack -o $@ $<
 311
 312 lib/plugins/%.cmxs: plugins/printer/%.cmx
 313         $(if $(QUIET),@echo 'Linking  $@' &&) \
 314             $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
 315
 316 lib/plugins/%.cmo: plugins/printer/%.cmo
 317         $(if $(QUIET),@echo 'Linking  $@' &&) \
 318             $(OCAMLC) $(BFLAGS) -pack -o $@ $<
 319
 320 lib/plugins/%.cmxs: plugins/transform/%.cmx
 321         $(if $(QUIET),@echo 'Linking  $@' &&) \
 322             $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
 323
 324 lib/plugins/%.cmo: plugins/transform/%.cmo
 325         $(if $(QUIET),@echo 'Linking  $@' &&) \
 326             $(OCAMLC) $(BFLAGS) -pack -o $@ $<
 327
 328 lib/plugins/tptp.cmxs: $(TPTPCMX)
 329         $(if $(QUIET),@echo 'Linking  $@' &&) \
 330             $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
 331
 332 lib/plugins/tptp.cmo: $(TPTPCMO)
 333         $(if $(QUIET),@echo 'Linking  $@' &&) \
 334             $(OCAMLC) $(BFLAGS) -pack -o $@ $^
 335
 336 PLUGSDIRS = plugins $(addprefix plugins/, $(PLUGDIRS))
 337 PLUGCLEAN = $(addsuffix /*.cm[iox], $(PLUGSDIRS)) \
 338             $(addsuffix /*.annot, $(PLUGSDIRS)) \
 339             $(addsuffix /*.output, $(PLUGSDIRS)) \
 340             $(addsuffix /*.automaton, $(PLUGSDIRS)) \
 341             $(addsuffix /*.dep, $(PLUGSDIRS)) \
 342             $(addsuffix /*.o, $(PLUGSDIRS)) \
 343             $(addsuffix /*~, $(PLUGSDIRS))
 344
 345 # depend and clean targets
 346
 347 ifneq "$(MAKECMDGOALS)" "clean"
 348 include $(PLUGDEP)
 349 endif
 350
 351 depend: $(PLUGDEP)
 352
 353 clean::
 354         rm -f $(PLUGCLEAN) $(PLUGGENERATED)
 355         rm -f lib/plugins/*
 356
 357 install_no_local::
 358         mkdir -p $(LIBDIR)/why3/plugins
 359         cp -f lib/plugins/* $(LIBDIR)/why3/plugins
 360
 361
 362 ##################
 363 # Why binary
 364 ##################
 365
 366 byte: bin/why3.byte
 367 opt:  bin/why3.opt
 368
 369 bin/why3.opt: src/why3.cmxa src/main.cmx
 370         $(if $(QUIET),@echo 'Linking  $@' &&) \
 371             $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
 372
 373 bin/why3.byte: src/why3.cma src/main.cmo
 374         $(if $(QUIET),@echo 'Linking  $@' &&) \
 375             $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
 376
 377 bin/why3: bin/why3.@OCAMLBEST@
 378         ln -sf why3.@OCAMLBEST@ $@
 379
 380 src/main.cmo: src/why3.cma
 381 src/main.cmx: src/why3.cmxa
 382
 383 clean::
 384         rm -f src/main.cm[iox] src/main.annot src/main.o
 385         rm -f bin/why3.byte bin/why3.opt bin/why3
 386
 387 install_no_local::
 388         cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
 389
 390 install_local: bin/why3
 391
 392 ########
 393 # Whyml (new API)
 394 ########
 395
 396 MLW_FILES = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
 397             mlw_dtree mlw_dty mlw_typing mlw_main
 398
 399 MLWMODULES = $(addprefix src/whyml/, $(MLW_FILES))
 400
 401 MLWDEP = $(addsuffix .dep, $(MLWMODULES))
 402 MLWCMO = $(addsuffix .cmo, $(MLWMODULES))
 403 MLWCMX = $(addsuffix .cmx, $(MLWMODULES))
 404
 405 $(MLWDEP): DEPFLAGS += -I src/whyml
 406 $(MLWCMO) $(MLWCMX): INCLUDES += -I src/whyml
 407
 408 # build targets
 409
 410 byte: $(MLWCMO)
 411 opt:  $(MLWCMX)
 412
 413 # depend and clean targets
 414
 415 ifneq "$(MAKECMDGOALS)" "clean"
 416 include $(MLWDEP)
 417 endif
 418
 419 depend: $(MLWDEP)
 420
 421 clean::
 422         rm -f src/whyml/*.cm[iox] src/whyml/*.o
 423         rm -f src/whyml/*.annot src/whyml/*.dep src/whyml/*~
 424 #       rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
 425
 426 ########
 427 # Whyml
 428 ########
 429
 430 PGM_FILES = pgm_ttree pgm_types pgm_pretty \
 431             pgm_module pgm_wp pgm_typing pgm_ocaml pgm_main
 432
 433 PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
 434
 435 PGMDEP = $(addsuffix .dep, $(PGMMODULES))
 436 PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
 437 PGMCMX = $(addsuffix .cmx, $(PGMMODULES))
 438
 439 $(PGMDEP): DEPFLAGS += -I src/programs
 440 $(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
 441
 442 # build targets
 443
 444 byte: bin/why3ml.byte
 445 opt:  bin/why3ml.opt
 446
 447 bin/why3ml.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) src/main.cmx
 448         $(if $(QUIET),@echo 'Linking  $@' &&) \
 449             $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
 450
 451 bin/why3ml.byte: src/why3.cma $(PGMCMO) $(MLWCMO) src/main.cmo
 452         $(if $(QUIET),@echo 'Linking  $@' &&) \
 453             $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
 454
 455 bin/why3ml: bin/why3ml.@OCAMLBEST@
 456         ln -sf why3ml.@OCAMLBEST@ $@
 457
 458 # depend and clean targets
 459
 460 ifneq "$(MAKECMDGOALS)" "clean"
 461 include $(PGMDEP)
 462 endif
 463
 464 depend: $(PGMDEP)
 465
 466 clean::
 467         rm -f src/programs/*.cm[iox] src/programs/*.o
 468         rm -f src/programs/*.annot src/programs/*.dep src/programs/*~
 469         rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
 470
 471 # test target
 472
 473 %.gui: %.why bin/why3ide.opt
 474         bin/why3ide.opt $*.why
 475
 476 %: %.mlw bin/why3ml.opt
 477         bin/why3ml.opt $*.mlw
 478
 479 %: %.why bin/why3.opt
 480         bin/why3.opt $*.why
 481
 482 %.gui: %.mlw bin/why3ide.opt
 483         bin/why3ide.opt $*.mlw
 484
 485 %.type: %.mlw bin/why3ide.opt
 486         bin/why3ml.opt --type-only $*.mlw
 487
 488 install_no_local::
 489         cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml$(EXE)
 490
 491 install_local: bin/why3ml
 492
 493 ##########
 494 # gallery
 495 ##########
 496
 497 # we export exactly the programs that have a why3session.xml file
 498
 499 .PHONY: gallery
 500
 501 gallery::
 502         @if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
 503         @for x in `find examples/programs/ -name why3session.xml`; do \
 504           d=`dirname $$x`; \
 505           f=`basename $$d`; \
 506           echo "exporting $$f"; \
 507           mkdir -p $(GALLERYDIR)/$$f; \
 508           cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \
 509           rm -f $(GALLERYDIR)/$$f/$$f.zip; \
 510           cd examples/programs/; \
 511           zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
 512           cd ../..; \
 513         done
 514
 515 ########
 516 # XML DTD validation
 517 ########
 518
 519 .PHONY: xml-validate
 520
 521 xml-validate:
 522         @for x in `find examples/ -name why3session.xml`; do \
 523           xmllint --noout --valid $$x 2>&1 | head -1; \
 524         done
 525
 526 ########
 527 # Config
 528 ########
 529
 530 CONFIG_FILES = whyconfig
 531
 532 CONFIGMODULES = $(addprefix src/config/, $(CONFIG_FILES))
 533
 534 CONFIGDEP = $(addsuffix .dep, $(CONFIGMODULES))
 535 CONFIGCMO = $(addsuffix .cmo, $(CONFIGMODULES))
 536 CONFIGCMX = $(addsuffix .cmx, $(CONFIGMODULES))
 537
 538 $(CONFIGDEP): DEPFLAGS += -I src/programs
 539 $(CONFIGCMO) $(CONFIGCMX): INCLUDES += -I src/programs
 540
 541 # build targets
 542
 543 byte: bin/why3config.byte
 544 opt:  bin/why3config.opt
 545
 546 bin/why3config.opt: src/why3.cmxa $(CONFIGCMX)
 547         $(if $(QUIET),@echo 'Linking  $@' &&) \
 548             $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
 549
 550 bin/why3config.byte: src/why3.cma $(CONFIGCMO)
 551         $(if $(QUIET),@echo 'Linking  $@' &&) \
 552             $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
 553
 554 bin/why3config: bin/why3config.@OCAMLBEST@
 555         ln -sf why3config.@OCAMLBEST@ $@
 556
 557 # depend and clean targets
 558
 559 ifneq "$(MAKECMDGOALS)" "clean"
 560 include $(CONFIGDEP)
 561 endif
 562
 563 depend: $(CONFIGDEP)
 564
 565 clean::
 566         rm -f src/config/*.cm[iox] src/config/*.o
 567         rm -f src/config/*.annot src/config/*.dep src/config/*~
 568         rm -f src/config/*.output src/config/*.automaton
 569         rm -f bin/why3config.byte bin/why3config.opt bin/why3config
 570
 571 local_config: bin/why3config.@OCAMLBEST@
 572         WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
 573                 --detect --conf_file why.conf
 574
 575 install_no_local::
 576         cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config$(EXE)
 577
 578 install_local: bin/why3config
 579
 580 ###############
 581 # IDE
 582 ###############
 583
 584 ifeq (@enable_ide@,yes)
 585
 586 IDE_FILES = gconfig gmain
 587
 588 IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
 589
 590 IDEDEP = $(addsuffix .dep, $(IDEMODULES))
 591 IDECMO = $(addsuffix .cmo, $(IDEMODULES))
 592 IDECMX = $(addsuffix .cmx, $(IDEMODULES))
 593
 594 $(IDEDEP): DEPFLAGS += -I src/ide
 595 $(IDECMO) $(IDECMX): INCLUDES += -I src/ide
 596
 597 # build targets
 598
 599 byte: bin/why3ide.byte
 600 opt:  bin/why3ide.opt
 601
 602 bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
 603 bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
 604
 605 bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) $(IDECMX)
 606         $(if $(QUIET),@echo 'Linking  $@' &&) \
 607             $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
 608
 609 bin/why3ide.byte: src/why3.cma $(PGMCMO) $(MLWCMO) $(IDECMO)
 610         $(if $(QUIET),@echo 'Linking  $@' &&) \
 611             $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
 612
 613 bin/why3ide: bin/why3ide.@OCAMLBEST@
 614         ln -sf why3ide.@OCAMLBEST@ $@
 615
 616 # depend and clean targets
 617
 618 ifneq "$(MAKECMDGOALS)" "clean"
 619 include $(IDEDEP)
 620 endif
 621
 622 depend: $(IDEDEP)
 623
 624 clean::
 625         rm -f src/ide/xml.ml
 626         rm -f src/ide/*.cm[iox] src/ide/*.o
 627         rm -f src/ide/*.annot src/ide/*.dep src/ide/*~
 628         rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
 629
 630 install_no_local::
 631         cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide$(EXE)
 632
 633 install_local: bin/why3ide
 634
 635 endif
 636
 637
 638 ###############
 639 # Replayer
 640 ###############
 641
 642 REPLAYER_FILES = replay
 643
 644 REPLAYERMODULES = $(addprefix src/ide/, $(REPLAYER_FILES))
 645
 646 REPLAYERDEP = $(addsuffix .dep, $(REPLAYERMODULES))
 647 REPLAYERCMO = $(addsuffix .cmo, $(REPLAYERMODULES))
 648 REPLAYERCMX = $(addsuffix .cmx, $(REPLAYERMODULES))
 649
 650 $(REPLAYERDEP): DEPFLAGS += -I src/ide
 651 $(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
 652
 653 # build targets
 654
 655 byte: bin/why3replayer.byte
 656 opt:  bin/why3replayer.opt
 657
 658 bin/why3replayer.opt: src/why3.cmxa $(PGMCMX) $(REPLAYERCMX)
 659         $(if $(QUIET),@echo 'Linking  $@' &&) \
 660             $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
 661
 662 bin/why3replayer.byte: src/why3.cma $(PGMCMO) $(REPLAYERCMO)
 663         $(if $(QUIET),@echo 'Linking  $@' &&) \
 664             $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
 665
 666 bin/why3replayer: bin/why3replayer.@OCAMLBEST@
 667         ln -sf why3replayer.@OCAMLBEST@ $@
 668
 669 # depend and clean targets
 670
 671 ifneq "$(MAKECMDGOALS)" "clean"
 672 include $(REPLAYERDEP)
 673 endif
 674
 675 depend: $(REPLAYERDEP)
 676
 677 clean::
 678         rm -f bin/why3replayer.byte bin/why3replayer.opt bin/why3replayer
 679
 680 install_no_local::
 681         cp -f bin/why3replayer.@OCAMLBEST@ $(BINDIR)/why3replayer$(EXE)
 682
 683 install_local: bin/why3replayer
 684
 685
 686 ###############
 687 # Session
 688 ###############
 689
 690 SESSION_FILES = why3session_lib why3session_copy why3session_info \
 691                 why3session_latex why3session_html why3session_rm \
 692                 why3session
 693
 694 SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
 695
 696 SESSIONDEP = $(addsuffix .dep, $(SESSIONMODULES))
 697 SESSIONCMO = $(addsuffix .cmo, $(SESSIONMODULES))
 698 SESSIONCMX = $(addsuffix .cmx, $(SESSIONMODULES))
 699
 700 $(SESSIONDEP): DEPFLAGS += -I src/why3session
 701 $(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session
 702
 703 # build targets
 704
 705 byte: bin/why3session.byte
 706 opt:  bin/why3session.opt
 707
 708 bin/why3session.opt: src/why3.cmxa $(PGMCMX) $(SESSIONCMX)
 709         $(if $(QUIET),@echo 'Linking  $@' &&) \
 710             $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
 711
 712 bin/why3session.byte: src/why3.cma $(PGMCMO) $(SESSIONCMO)
 713         $(if $(QUIET),@echo 'Linking  $@' &&) \
 714             $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
 715
 716 bin/why3session: bin/why3session.@OCAMLBEST@
 717         ln -sf why3session.@OCAMLBEST@ $@
 718
 719 # depend and clean targets
 720
 721 ifneq "$(MAKECMDGOALS)" "clean"
 722 include $(SESSIONDEP)
 723 endif
 724
 725 depend: $(SESSIONDEP)
 726
 727 clean::
 728         rm -f src/why3session/*.cm[iox] src/why3session/*.o
 729         rm -f src/why3session/*.annot src/why3session/*.dep src/why3session/*~
 730         rm -f bin/why3session.byte bin/why3session.opt bin/why3session
 731
 732 install_no_local::
 733         cp -f bin/why3session.@OCAMLBEST@ $(BINDIR)/why3session$(EXE)
 734
 735 install_local: bin/why3session
 736
 737
 738 ###############
 739 # Bench
 740 ###############
 741
 742 ifeq (@enable_bench@,yes)
 743
 744 BENCH_FILES = worker db bench benchrc benchdb whybench
 745
 746 BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES))
 747
 748 BENCHDEP = $(addsuffix .dep, $(BENCHMODULES))
 749 BENCHCMO = $(addsuffix .cmo, $(BENCHMODULES))
 750 BENCHCMX = $(addsuffix .cmx, $(BENCHMODULES))
 751
 752 $(BENCHDEP): DEPFLAGS += -I src/bench
 753 $(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/bench -I @SQLITE3LIB@
 754
 755 # build targets
 756
 757 byte: bin/why3bench.byte
 758 opt:  bin/why3bench.opt
 759
 760 bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I @SQLITE3LIB@
 761 bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3
 762
 763 bin/why3bench.opt: src/why3.cmxa $(PGMCMX) $(BENCHCMX)
 764         $(if $(QUIET),@echo 'Linking  $@' &&) \
 765             $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
 766
 767 bin/why3bench.byte: src/why3.cma  $(PGMCMO) $(BENCHCMO)
 768         $(if $(QUIET),@echo 'Linking  $@' &&) \
 769             $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
 770
 771 bin/why3bench: bin/why3bench.@OCAMLBEST@
 772         ln -sf why3bench.@OCAMLBEST@ $@
 773
 774 # depend and clean targets
 775
 776 ifneq "$(MAKECMDGOALS)" "clean"
 777 include $(BENCHDEP)
 778 endif
 779
 780 depend: $(BENCHDEP)
 781
 782 clean::
 783         rm -f src/bench/*.cm[iox] src/bench/*.o
 784         rm -f src/bench/*.annot src/bench/*.dep src/bench/*~
 785         rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
 786
 787 install_no_local::
 788         cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench$(EXE)
 789
 790 install_local: bin/why3bench
 791
 792 endif
 793
 794 ##############
 795 # Coq plugin
 796 ##############
 797
 798 ifeq (@enable_coq_plugin@,yes)
 799
 800 COQPGENERATED = src/coq-tactic/g_why3tac.ml
 801
 802 COQP_FILES = why3tac g_why3tac
 803
 804 COQPMODULES = $(addprefix src/coq-tactic/, $(COQP_FILES))
 805
 806 COQPDEP = $(addsuffix .dep, $(COQPMODULES))
 807 COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
 808 COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
 809
 810 COQPTREES = kernel lib interp parsing proofs pretyping tactics library toplevel
 811 COQPINCLUDES = -I src/coq-tactic $(addprefix -I @COQLIB@/, $(COQPTREES))
 812
 813 $(COQPDEP): DEPFLAGS += -I src/coq-tactic
 814 $(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
 815
 816 $(COQPDEP): $(COQPGENERATED)
 817
 818 byte: src/coq-tactic/.why3-vo-byte
 819 opt:  src/coq-tactic/.why3-vo-opt
 820
 821 lib/coq-tactic/why3tac.cma:  BFLAGS+=-rectypes -I +camlp5
 822 lib/coq-tactic/why3tac.cmxs: OFLAGS+=-rectypes -I +camlp5
 823
 824 lib/coq-tactic/why3tac.cmxs: src/why3.cmxa $(COQPCMX)
 825         $(if $(QUIET),@echo 'Linking  $@' &&) \
 826             $(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
 827
 828 lib/coq-tactic/why3tac.cma: src/why3.cma $(COQPCMO)
 829         $(if $(QUIET),@echo 'Linking  $@' &&) \
 830             $(OCAMLC) -a $(BFLAGS) -o $@ $^
 831
 832 src/coq-tactic/g_why3tac.ml: src/coq-tactic/g_why3tac.ml4
 833         $(if $(QUIET),@echo 'Camlp5   $<' &&) \
 834             $(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@
 835
 836 src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cma
 837         $(if $(QUIET),@echo 'Coqc     $<' &&) \
 838             WHY3NOCONFIG=42 $(COQC) -byte -I lib/coq-tactic/ $< && \
 839             touch src/coq-tactic/.why3-vo-byte
 840
 841 src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cmxs
 842         $(if $(QUIET),@echo 'Coqc     $<' &&) \
 843             WHY3NOCONFIG=42 $(COQC) -opt -I lib/coq-tactic/ $< && \
 844             touch src/coq-tactic/.why3-vo-opt
 845
 846 test-coq-tactic.byte: src/coq-tactic/.why3-vo-byte
 847         $(COQC) -byte -I lib/coq-tactic/ src/coq-tactic/test.v
 848
 849 test-coq-tactic.opt: src/coq-tactic/.why3-vo-opt
 850         $(COQC) -opt -I lib/coq-tactic/ src/coq-tactic/test.v
 851
 852 # depend and clean targets
 853
 854 ifneq "$(MAKECMDGOALS)" "clean"
 855 include $(COQPDEP)
 856 endif
 857
 858 depend: $(COQPDEP)
 859
 860 clean::
 861         rm -f src/coq-tactic/*.cm[iox] src/coq-tactic/*.o
 862         rm -f lib/coq-tactic/*.cma lib/coq-tactic/*.cmxs
 863         rm -f lib/coq-tactic/*.vo lib/coq-tactic/*.glob
 864         rm -f src/coq-tactic/*.annot src/coq-tactic/*.dep src/coq-tactic/*~
 865         rm -f src/coq-tactic/.why3-vo-*
 866         rm -f $(COQPGENERATED)
 867
 868 install_no_local::
 869         mkdir -p $(LIBDIR)/why3/coq-tactic
 870         cp -f lib/coq-tactic/* $(LIBDIR)/why3/coq-tactic
 871
 872 endif
 873
 874 ####################
 875 # Coq realizations
 876 ####################
 877
 878 ifeq (@enable_coq_libs@,yes)
 879
 880 COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax
 881 COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES))
 882
 883 COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax Real Square RealInfix
 884 COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
 885
 886 COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime
 887 COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
 888
 889 ifeq (@enable_coq_fp_libs@,yes)
 890 COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
 891 COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
 892 COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
 893 endif
 894
 895 COQLIBS_FILES = $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_FP)
 896
 897 COQV  = $(addsuffix .v,  $(COQLIBS_FILES))
 898 COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
 899 COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
 900
 901 %.vo: %.v
 902         $(if $(QUIET),@echo 'Coqc     $<' &&) \
 903             $(COQC) -R lib/coq Why3 $<
 904
 905 %.vd: %.v
 906         $(if $(QUIET),@echo 'Coqdep   $<' &&) \
 907             $(COQDEP) -slash -R lib/coq Why3 $< > $@
 908
 909 drivers/coq-realizations.aux: Makefile
 910         $(if $(QUIET),@echo 'Generate $@' &&) \
 911         (echo "(* generated automatically at compilation time *)"; \
 912         for f in $(COQLIBS_INT_FILES); do \
 913         echo 'theory int.'"$$f"' meta "realized" "int.'"$$f"'", "" end'; done; \
 914         for f in $(COQLIBS_REAL_FILES); do \
 915         echo 'theory real.'"$$f"' meta "realized" "real.'"$$f"'", "" end'; done; \
 916         for f in $(COQLIBS_NUMBER_FILES); do \
 917         echo 'theory number.'"$$f"' meta "realized" "number.'"$$f"'", "" end'; done; \
 918         for f in $(COQLIBS_FP_FILES); do \
 919         echo 'theory floating_point.'"$$f"' meta "realized" "floating_point.'"$$f"'", "" end'; done; \
 920         ) > $@
 921
 922 opt byte: $(COQVO)
 923
 924 install_no_local::
 925         mkdir -p $(LIBDIR)/why3/coq
 926         mkdir -p $(LIBDIR)/why3/coq/int
 927         cp $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/
 928         mkdir -p $(LIBDIR)/why3/coq/real
 929         cp $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
 930         mkdir -p $(LIBDIR)/why3/coq/number
 931         cp $(addsuffix .vo, $(COQLIBS_NUMBER)) $(LIBDIR)/why3/coq/number/
 932 ifeq (@enable_coq_fp_libs@,yes)
 933         mkdir -p $(LIBDIR)/why3/coq/floating_point
 934         cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
 935 endif
 936         cp drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
 937
 938 install_local: $(COQVO) drivers/coq-realizations.aux
 939
 940 ifneq "$(MAKECMDGOALS)" "clean"
 941 include $(COQVD)
 942 endif
 943
 944 depend: $(COQVD)
 945
 946 clean::
 947         rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
 948
 949 update-coq: bin/why3 drivers/coq-realizations.aux
 950         for f in $(COQLIBS_INT_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
 951         for f in $(COQLIBS_REAL_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
 952         for f in $(COQLIBS_NUMBER_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T number.$$f -o lib/coq/number/; done
 953         for f in $(COQLIBS_FP_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
 954
 955 else
 956
 957 drivers/coq-realizations.aux:
 958         echo "(* generated automatically at compilation time *)" > $@
 959
 960 endif
 961
 962 opt byte: drivers/coq-realizations.aux
 963
 964 clean::
 965         rm -f drivers/coq-realizations.aux
 966
 967 ####################
 968 # PVS realizations
 969 ####################
 970
 971 ifeq (@enable_pvs_libs@,yes)
 972
 973 PVSLIBS_INT_FILES = Int Abs MinMax ComputerDivision EuclideanDivision
 974 PVSLIBS_INT = $(addprefix lib/pvs/int/, $(PVSLIBS_INT_FILES))
 975
 976 PVSLIBS_REAL_FILES = Abs FromInt MinMax Real # ExpLog Square RealInfix
 977 PVSLIBS_REAL = $(addprefix lib/pvs/real/, $(PVSLIBS_REAL_FILES))
 978
 979 PVSLIBS_NUMBER_FILES = # Divisibility Gcd Parity Prime
 980 PVSLIBS_NUMBER = $(addprefix lib/pvs/number/, $(PVSLIBS_NUMBER_FILES))
 981
 982 ifeq (@enable_pvs_fp_libs@,yes)
 983 PVSLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
 984 PVSLIBS_FP_ALL_FILES = GenFloat $(PVSLIBS_FP_FILES)
 985 PVSLIBS_FP = $(addprefix lib/pvs/floating_point/, $(PVSLIBS_FP_ALL_FILES))
 986 endif
 987
 988 PVSLIBS_FILES = $(PVSLIBS_INT) $(PVSLIBS_REAL) $(PVSLIBS_NUMBER) $(PVSLIBS_FP)
 989
 990 drivers/pvs-realizations.aux: Makefile
 991         $(if $(QUIET),@echo 'Generate $@' &&) \
 992         (echo "(* generated automatically at compilation time *)"; \
 993         for f in $(PVSLIBS_INT_FILES); do \
 994         echo 'theory int.'"$$f"' meta "realized" "int.'"$$f"'", "" end'; done; \
 995         for f in $(PVSLIBS_REAL_FILES); do \
 996         echo 'theory real.'"$$f"' meta "realized" "real.'"$$f"'", "" end'; done; \
 997         for f in $(PVSLIBS_NUMBER_FILES); do \
 998         echo 'theory number.'"$$f"' meta "realized" "number.'"$$f"'", "" end'; done; \
 999         for f in $(PVSLIBS_FP_FILES); do \
1000         echo 'theory floating_point.'"$$f"' meta "realized" "floating_point.'"$$f"'", "" end'; done; \
1001         ) > $@
1002
1003 install_no_local::
1004         mkdir -p $(LIBDIR)/why3/pvs/int
1005         cp $(PVSLIBS_INT) $(LIBDIR)/why3/pvs/int/
1006         mkdir -p $(LIBDIR)/why3/pvs/real
1007         cp $(PVSLIBS_REAL) $(LIBDIR)/why3/pvs/real/
1008         mkdir -p $(LIBDIR)/why3/pvs/number
1009         cp $(PVSLIBS_NUMBER) $(LIBDIR)/why3/pvs/number/
1010 ifeq (@enable_pvs_fp_libs@,yes)
1011         mkdir -p $(LIBDIR)/why3/pvs/floating_point/
1012         cp $(PVSLIBS_FP) $(LIBDIR)/why3/pvs/
1013 endif
1014         cp drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
1015
1016 install_local: drivers/pvs-realizations.aux
1017
1018 update-pvs: bin/why3 drivers/pvs-realizations.aux
1019         for f in $(PVSLIBS_INT_FILES); do bin/why3 --realize -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done
1020         for f in $(PVSLIBS_REAL_FILES); do bin/why3 --realize -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
1021         for f in $(PVSLIBS_NUMBER_FILES); do bin/why3 --realize -D drivers/pvs-realize.drv -T number.$$f -o lib/pvs/number/; done
1022         for f in $(PVSLIBS_FP_FILES); do bin/why3 --realize -D drivers/pvs-realize.drv -T floating_point.$$f -o lib/pvs/floating_point/; done
1023
1024 else
1025
1026 drivers/pvs-realizations.aux:
1027         echo "(* generated automatically at compilation time *)" > $@
1028
1029 endif
1030
1031 opt byte: drivers/pvs-realizations.aux
1032
1033 clean::
1034         rm -f drivers/pvs-realizations.aux
1035
1036 #######
1037 # tools
1038 #######
1039
1040 TOOLS = bin/why3-cpulimit$(EXE)
1041
1042 byte opt: $(TOOLS)
1043
1044 bin/why3-cpulimit$(EXE): src/tools/@CPULIMIT@.c
1045         $(CC) -Wall -o $@ $^
1046
1047 clean::
1048         rm -f bin/why3-cpulimit$(EXE) src/tools/*~
1049
1050 install_no_local::
1051         cp -f bin/why3-cpulimit$(EXE) $(BINDIR)/why3-cpulimit$(EXE)
1052
1053 #########
1054 # why3doc
1055 #########
1056
1057 WHY3DOCGENERATED = src/why3doc/doc_lexer.ml
1058
1059 WHY3DOC_FILES = doc_html doc_def doc_lexer doc_main
1060
1061 WHY3DOCMODULES = $(addprefix src/why3doc/, $(WHY3DOC_FILES))
1062
1063 WHY3DOCDEP = $(addsuffix .dep, $(WHY3DOCMODULES))
1064 WHY3DOCCMO = $(addsuffix .cmo, $(WHY3DOCMODULES))
1065 WHY3DOCCMX = $(addsuffix .cmx, $(WHY3DOCMODULES))
1066
1067 $(WHY3DOCDEP): DEPFLAGS += -I src/why3doc
1068 $(WHY3DOCCMO) $(WHY3DOCCMX): INCLUDES += -I src/why3doc
1069
1070 $(WHY3DOCDEP): $(WHY3DOCGENERATED)
1071
1072 # build targets
1073
1074 byte: bin/why3doc.byte
1075 opt:  bin/why3doc.opt
1076
1077 bin/why3doc.opt: src/why3.cmxa $(PGMCMX) $(WHY3DOCCMX)
1078         $(if $(QUIET),@echo 'Linking  $@' &&) \
1079             $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
1080
1081 bin/why3doc.byte: src/why3.cma $(PGMCMO) $(WHY3DOCCMO)
1082         $(if $(QUIET),@echo 'Linking  $@' &&) \
1083             $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
1084
1085 bin/why3doc: bin/why3doc.@OCAMLBEST@
1086         ln -sf why3doc.@OCAMLBEST@ $@
1087
1088 # depend and clean targets
1089
1090 ifneq "$(MAKECMDGOALS)" "clean"
1091 include $(WHY3DOCDEP)
1092 endif
1093
1094 depend: $(WHY3DOCDEP)
1095
1096 clean::
1097         rm -f $(WHY3DOCGENERATED)
1098         rm -f src/why3doc/*.cm[iox] src/why3doc/*.o
1099         rm -f src/why3doc/*.annot src/why3doc/*.dep src/why3doc/*~
1100         rm -f bin/why3doc.byte bin/why3doc.opt bin/why3doc
1101
1102 install_no_local::
1103         cp -f bin/why3doc.@OCAMLBEST@ $(BINDIR)/why3doc$(EXE)
1104
1105 install_local: bin/why3doc
1106
1107 ########
1108 # bench
1109 ########
1110
1111 .PHONY: bench test
1112
1113 bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
1114         $(MAKE) test-api.@OCAMLBEST@
1115         sh bench/bench "bin/why3.@OCAMLBEST@" "bin/why3ml.@OCAMLBEST@"
1116         @if test "@enable_coq_plugin@" = "yes"; then \
1117            echo "=== checking the Coq tactic ==="; \
1118            $(MAKE) test-coq-tactic.@OCAMLBEST@; fi
1119
1120 ###############
1121 # test targets
1122 ###############
1123
1124 test2: bin/why3.byte $(TOOLS)
1125         bin/why3.byte tests/test-jcf.why
1126
1127 test: bin/why3.byte plugins.byte $(TOOLS)
1128         mkdir -p output_why3
1129         bin/why3.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
1130         # bin/why3.byte -D drivers/alt_ergo.drv tests/test-jcf.why -T Test -G G
1131         # bin/why3.byte -P alt-ergo --timelimit 3 tests/test-jcf.why -T Test -G G
1132         # bin/why3.byte -D drivers/coq.drv tests/test-jcf.why -T Test -G G
1133         echo bin/why3.byte -P alt-ergo --timelimit 1 --prove theories/real.why
1134         @printf "*** Checking Coq file generation ***\\n"
1135         @mkdir -p output_coq
1136         @for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
1137                 real.Abs real.FromIntTest real.SquareTest \
1138                 real.ExpLogTest real.PowerTest real.TrigonometryTest \
1139                 floating_point.Test map.TestBv32 \
1140                 ; do \
1141           printf "Generating Coq file for $$i\\n" && \
1142                 bin/why3.byte -P coq -o output_coq -T $$i ; done
1143         @printf "*** Checking Coq compilation ***\\n"
1144         @for i in output_coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done
1145
1146 testl: bin/why3ml.byte
1147         ocamlrun -bt bin/why3ml.byte tests/test-pgm-jcf.mlw
1148         ocamlrun -bt bin/why3ml.byte -P alt-ergo tests/test-pgm-jcf.mlw
1149
1150 testl-debug: bin/why3ml.opt
1151         bin/why3ml.opt --debug program_typing tests/test-pgm-jcf.mlw
1152
1153 testl-ide: bin/why3ide.opt
1154         bin/why3ide.opt tests/test-pgm-jcf.mlw
1155
1156 testl-type: bin/why3ml.byte
1157         ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
1158
1159 test-api.byte: examples/use_api.ml src/why3.cma
1160         $(if $(QUIET),@echo 'Ocaml    $<' &&) \
1161         ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma $< \
1162         || (printf "Test of Why API calls failed. Please fix it"; exit 2)
1163
1164 test-api.opt: examples/use_api.ml src/why3.cmxa
1165         $(if $(QUIET),@echo 'Ocamlopt $<' &&) \
1166         ($(OCAMLOPT) -o $@ -I src/ $(INCLUDES) $(EXTCMXA) src/why3.cmxa $< \
1167         && ./test-api.opt) \
1168         || (printf "Test of Why API calls failed. Please fix it"; exit 2)
1169         @rm -f test-api.opt
1170
1171 test-shape: src/why3.cma
1172         ocaml -I src/ $(INCLUDES) $(EXTCMA) $? examples/test_shape.ml
1173
1174
1175 ################
1176 # documentation
1177 ################
1178
1179 .PHONY: doc
1180
1181 ifeq (@enable_doc@,yes)
1182
1183 doc: doc/manual.pdf
1184 # doc/manual.html
1185
1186 BNF = qualid label constant operator term type formula theory theory2 \
1187         why_file typev expr expr2 module whyml_file
1188 BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
1189
1190 doc/%_bnf.tex: doc/%.bnf doc/bnf
1191         doc/bnf $< > $@
1192
1193 doc/bnf: doc/bnf.mll
1194         $(OCAMLLEX) $<
1195         $(OCAMLOPT) -o $@ doc/bnf.ml
1196
1197 DOC = api glossary ide intro library macros manpages coq_tactic \
1198       realizations manual starting syntax syntaxref technical version whyml
1199
1200 DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
1201
1202 doc/manual.pdf: $(BNFTEX) $(DOCTEX) doc/manual.bib
1203         cd doc; $(RUBBER) --warn all --pdf manual.tex
1204
1205 # doc/manual.html: doc/manual.tex doc/version.tex
1206 #       $(MAKE) -C doc manual.html
1207
1208 clean::
1209         cd doc; $(RUBBER) --pdf --clean manual.tex
1210
1211 else
1212
1213 doc:
1214
1215 endif
1216
1217 ##########
1218 # API DOC
1219 ##########
1220
1221 .PHONY: apidoc
1222
1223 MODULESTODOC = util/util util/hashweak \
1224         core/ident core/ty core/term core/decl core/theory \
1225         core/env core/task \
1226         driver/whyconf driver/driver \
1227         util/rc \
1228         session/session session/session_tools session/session_scheduler
1229 #       transform/introduction \
1230 #       ide/db
1231
1232 FILESTODOC = $(addsuffix .mli, $(addprefix src/, $(MODULESTODOC)))
1233
1234 apidoc: $(FILESTODOC)
1235         mkdir -p doc/apidoc
1236         $(OCAMLDOC) -d doc/apidoc -html -t "Why3 API documentation" \
1237                 -keep-code $(INCLUDES) \
1238                 $(LIBINCLUDES) -I src $(FILESTODOC)
1239
1240 # could we include also the dependency graph ?
1241 # $(OCAMLDOC) -o doc/apidoc/dg.dot -dot $(INCLUDES) \
1242 #       $(LIBINCLUDES) -I src $(FILESTODOC)
1243
1244 # what is this ? api doc is in why3.lri.fr/api instead...
1245 # install_apidoc: apidoc
1246 #       rsync -av doc/apidoc/ marche@scm.gforge.inria.fr:/home/groups/why3/htdocs/apidoc/
1247
1248 doc/apidoc.tex: $(FILESTODOC)
1249         $(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
1250                 $(LIBINCLUDES) -I src $(FILESTODOC)
1251
1252 clean::
1253         rm -f doc/apidoc/*
1254
1255 ##########
1256 # Stdlib formatted with why3doc
1257 ##########
1258
1259 .PHONY: stdlibdoc
1260
1261 STDLIBS = algebra \
1262         bag \
1263         bool \
1264         comparison \
1265         floating_point \
1266         graph \
1267         int \
1268         list \
1269         map \
1270         number \
1271         option \
1272         real \
1273         relations \
1274         set
1275 # function ? sum ? tptp ?
1276
1277 STDMODS = arith array hashtbl impset pqueue queue random ref stack string
1278
1279 STDLIBFILES = $(addsuffix .why, $(addprefix theories/, $(STDLIBS)))
1280 STDMODFILES = $(addsuffix .mlw, $(addprefix modules/, $(STDMODS)))
1281
1282 stdlibdoc: $(STDLIBFILES) $(STDMODFILES) bin/why3doc.@OCAMLBEST@
1283         mkdir -p doc/stdlibdoc
1284         rm -f doc/stdlibdoc/style.css
1285         WHY3LOADPATH=theories bin/why3doc.@OCAMLBEST@ -L modules \
1286           -o doc/stdlibdoc --title "Why3 Standard Library" \
1287           $(STDLIBFILES) $(STDMODFILES)
1288
1289 clean::
1290         rm -f doc/stdlibdoc/*
1291
1292 ################
1293 # generic rules
1294 ################
1295
1296 %.cmi: %.mli
1297         $(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) $<
1298
1299 %.cmo: %.ml
1300         $(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) $<
1301
1302 %.cmx: %.ml
1303         $(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -c $(OFLAGS) $<
1304
1305 %.cmxs: %.ml
1306         $(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
1307
1308 %.ml: %.mll
1309         $(if $(QUIET),@echo 'Ocamllex $<' &&) $(OCAMLLEX) $<
1310
1311 %.ml %.mli: %.mly
1312         $(if $(QUIET),@echo 'Ocamlyacc $<' &&) $(OCAMLYACC) -v $<
1313
1314 %.dep: %.ml
1315         $(if $(QUIET),@echo 'Ocamldep $<' &&) $(OCAMLDEP) $(DEPFLAGS) $< $<i > $@
1316
1317 # .ml4.ml:
1318 #       $(CAMLP4) pr_o.cmo -impl $< > $@
1319
1320 # jc/jc_ai.ml: jc/jc_annot_inference.ml jc/jc_annot_fail.ml Makefile
1321 #       if test "@enable_apron@" = "yes" ; then \
1322 #         echo "# 1 \"jc/jc_annot_inference.ml\"" > jc/jc_ai.ml; \
1323 #         cat jc/jc_annot_inference.ml >> jc/jc_ai.ml; \
1324 #       else \
1325 #         echo "# 1 \"jc/jc_annot_fail.ml\"" > jc/jc_ai.ml; \
1326 #         cat jc/jc_annot_fail.ml >> jc/jc_ai.ml; \
1327 #       fi
1328
1329 # %_why.v: %.mlw $(BINARY)
1330 #       $(BINARY) -coq $*.mlw
1331
1332 # %_why.pvs: %.mlw $(BINARY)
1333 #       $(BINARY) -pvs $*.mlw
1334
1335 # Emacs tags
1336 ############
1337
1338 tags:
1339         find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
1340         etags "--regex-ocaml=/let[ \t]+\([^ \t]+\)/\1/" \
1341               "--regex-ocaml=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
1342               "--regex-ocaml=/and[ \t]+\([^ \t]+\)/\1/" \
1343               "--regex-ocaml=/type[ \t]+\([^ \t]+\)/\1/" \
1344               "--regex-ocaml=/exception[ \t]+\([^ \t]+\)/\1/" \
1345               "--regex-ocaml=/val[ \t]+\([^ \t]+\)/\1/" \
1346               "--regex-ocaml=/module[ \t]+\([^ \t]+\)/\1/"
1347
1348 otags:
1349         find \( -name '*.ml' -or -name '*.mli' \) -print0 | xargs -0 otags
1350 #       otags src/*.mli src/*.ml c/*.mli c/*.ml intf/*.mli intf/*.ml
1351
1352 # the previous seems broken. This one is intented for vi(m) users, but could
1353 # be adapted for emacs (remove the -vi option ?)
1354 otags-vi:
1355         find \( -name '*.ml' -or -name '*.mli' \) -print0 | xargs -0 otags -vi
1356
1357 wc:
1358         ocamlwc -p src/*.ml* src/*/*.ml*
1359
1360 #dep: depend
1361 #       cat .depend* | ocamldot | dot -Tpdf > dep.pdf
1362 #       $(PDFVIEWER) dep.pdf
1363
1364 # distrib
1365 #########
1366
1367 NAME = why3-$(VERSION)
1368 DISTRIB_DIR = distrib/$(NAME)
1369 DISTRIB_TAR = $(DISTRIB_DIR).tar.gz
1370
1371 DISTRIB_FILES = Version Makefile.in configure.in META.in configure \
1372       README CHANGES INSTALL OCAML-LICENSE LICENSE src/config.sh.in \
1373       src/*.ml* src/*.dep src/*/*.ml* src/*/*.dep src/*/*.c \
1374       plugins/printer/.keepme plugins/*/*.ml* plugins/*/*.dep \
1375       doc/version.tex.in doc/manual.pdf \
1376       drivers/*.drv drivers/*.gen \
1377       examples/*.why examples/programs/*.mlw examples/tptp/*.why \
1378       examples/tests-provers/*.why examples/check-builtin/*.why \
1379       examples/bts/*.why \
1380       examples/programs/vacid_0_binary_heaps/*.why \
1381       examples/programs/vacid_0_binary_heaps/*.mlw \
1382       examples/bitvectors/*.why \
1383       examples/foveoos2011/*.mlw \
1384       examples/*/*.xml examples/*/*/*.xml examples/*/*/*/*.xml \
1385       examples/*/*.v   examples/*/*/*.v examples/*/*/*/*.v\
1386       examples/use_api.ml \
1387       theories/*.why \
1388       modules/*.mlw \
1389       lib/coq/*/*.v lib/coq-tactic/*.v \
1390       share/provers-detection-data.conf.in \
1391       share/why3session.dtd \
1392       share/javascript/*.js share/javascript/*.css \
1393       share/javascript/themes/default/*.gif \
1394       share/javascript/themes/default/*.png \
1395       share/javascript/themes/default/*.css \
1396       share/emacs/why.el share/lang/*.lang \
1397       share/images/icons.rc share/images/*.png share/images/*/*.png \
1398       share/bash/why3 share/zsh/_why3 share/vim/why3.vim
1399
1400 # TODO?
1401 # share/zsh ?
1402 # symbolic links in share/ ?
1403
1404 distrib:: $(DISTRIB_TAR)
1405
1406 rmdistrib:
1407         rm -rf $(DISTRIB_DIR)
1408
1409 redistrib: rmdistrib distrib
1410
1411 $(DISTRIB_TAR): doc/manual.pdf
1412         @if test -d $(DISTRIB_DIR); then \
1413           echo "Hum... there is already a directory $(NAME)"; \
1414           echo "Please increase the version number"; exit 1; \
1415         fi
1416         mkdir -p $(DISTRIB_DIR)
1417         mkdir -p $(DISTRIB_DIR)/bin
1418         mkdir -p $(DISTRIB_DIR)/share
1419         mkdir -p $(DISTRIB_DIR)/lib
1420         mkdir -p $(DISTRIB_DIR)/lib/plugins
1421         mkdir -p $(DISTRIB_DIR)/lib/coq
1422         mkdir -p $(DISTRIB_DIR)/lib/coq-tactic
1423         ln -s ../drivers $(DISTRIB_DIR)/share/drivers
1424         ln -s ../modules $(DISTRIB_DIR)/share/modules
1425         ln -s ../theories $(DISTRIB_DIR)/share/theories
1426         cp --parents $(DISTRIB_FILES) $(DISTRIB_DIR)
1427         rm -f $(DISTRIB_DIR)/src/config.ml
1428         cd $(DISTRIB_DIR); rm -f $(LIBGENERATED) \
1429           $(COQGENERATED) $(WHY3DOCGENERATED) $(PLUGGENERATED)
1430         cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar
1431
1432 # distrib export: source export-doc export-www export-examples export-examples-c linux
1433 #
1434 # export-www:
1435 #       echo "<#def version>$(VERSION)</#def>" > /users/demons/filliatr/www/why/version.prehtml
1436 #       echo "<#def cversion>$(CVERSION)</#def>" >> /users/demons/filliatr/www/why/version.prehtml
1437 #       $(MAKE) -C /users/demons/filliatr/www/why install
1438 #
1439 #
1440 # tarball:
1441 #       mkdir -p export
1442 #       cd export; rm -rf $(NAME) $(NAME).tar.gz
1443 #       $(MAKE) export/$(NAME).tar.gz
1444 #
1445 # EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
1446 #
1447 # export-examples:
1448 #       cp --parents $(EXFILES) $(WWW)
1449 #       $(MAKE) -C $(WWW)/examples clean depend
1450 #       echo "*** faire make all dans $(WWW)/examples ***"
1451 #
1452 # export-examples-c:
1453 #       mkdir -p $(WWW)/caduceus/examples
1454 #       cd examples-c; cp --parents */*.c */*.h $(WWW)/caduceus/examples
1455 #       mkdir -p $(WWW)/caduceus/examples/bench
1456 #       cp bench/c/good/*.c $(WWW)/caduceus/examples/bench
1457 #       rm -f $(WWW)/caduceus/examples/bench/test.c
1458 #
1459 # export-doc: $(DOC)
1460 #       cp doc/manual.ps doc/manual.html $(WWW)/manual
1461 #       cp doc/logic_syntax.bnf $(WWW)/manual
1462 #       (cd $(WWW)/manual; hacha manual.html)
1463 #       cp doc/caduceus.ps doc/caduceus.html $(WWW)/caduceus/manual
1464 #       (cd $(WWW)/caduceus/manual; hacha caduceus.html)
1465 #       cp doc/krakatoa.pdf doc/krakatoa.html $(WWWKRAKATOA)/manual
1466 #       (cd $(WWWKRAKATOA)/manual; hacha krakatoa.html)
1467 #
1468 # OSTYPE  ?= linux
1469 #
1470 # BINARYNAME = $(NAME)-$(OSTYPE)
1471 #
1472 # linux: binary
1473 #
1474 # ALLBINARYFILES = $(FILES) $(BINARYFILES)
1475 #
1476 # binary: $(ALLBINARYFILES)
1477 #       mkdir -p export/$(BINARYNAME)
1478 #       cp --parents $(ALLBINARYFILES) export/$(BINARYNAME)
1479 #       (cd export; tar czf $(BINARYNAME).tar.gz $(BINARYNAME))
1480 #       cp export/$(BINARYNAME).tar.gz $(FTP)
1481
1482 ###############
1483 # file headers
1484 ###############
1485
1486 headers:
1487         headache -c misc/headache_config.txt -h misc/header.txt \
1488             Makefile.in configure.in src/*.ml* src/*/*.ml* \
1489             plugins/*/*.ml* src/tools/cpulimit.c
1490         headache -c misc/headache_config.txt -h misc/header_gm.txt \
1491             src/transform/abstraction.ml* \
1492             src/transform/instantiate_predicate.ml* \
1493             src/transform/simplify_formula.ml* \
1494             src/printer/print_number.ml* \
1495             src/printer/gappa.ml*
1496         headache -c misc/headache_config.txt -h misc/header_jk.txt \
1497             src/transform/close_epsilon.ml* \
1498             src/transform/lift_epsilon.ml*
1499         headache -c misc/headache_config.txt -h misc/header_sc.txt \
1500             plugins/transform/hypothesis_selection.ml*
1501         sed -i -f misc/fixnames.sed -- \
1502             Makefile.in configure.in src/*.ml* src/*/*.ml* \
1503             plugins/*/*.ml* src/tools/cpulimit.c
1504
1505 #########
1506 # myself
1507 #########
1508
1509 Makefile: Makefile.in config.status
1510         ./config.status chmod --file $@
1511
1512 src/config.sh: src/config.sh.in config.status
1513         ./config.status chmod --file $@
1514
1515 src/config.ml: src/config.sh
1516         $(if $(QUIET),@echo 'Generate $@' &&) \
1517             LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
1518
1519 clean::
1520         rm -f src/config.ml
1521
1522 doc/version.tex: doc/version.tex.in config.status
1523         ./config.status chmod --file $@
1524
1525 share/provers-detection-data.conf: share/provers-detection-data.conf.in config.status
1526         ./config.status chmod --file $@
1527
1528 # We want it to be always up-ot-date
1529 Makefile : share/provers-detection-data.conf
1530
1531 config.status: configure Version
1532         ./config.status --recheck
1533
1534 opt byte : META share/provers-detection-data.conf
1535
1536 META: META.in config.status
1537         ./config.status chmod --file $@
1538
1539 configure: configure.in
1540         autoconf
1541
1542 ###################
1543 # clean and depend
1544 ###################
1545
1546 .PHONY: distclean
1547
1548 distclean: clean
1549         rm -f config.status config.cache config.log \
1550             Makefile src/config.ml doc/version.tex
1551
1552 depend:
1553         rm -f $^
1554         $(MAKE) $^
1555
1556 #################################################################
1557 # Building the Why platform with ocamlbuild (OCaml 3.10 needed) #
1558 #################################################################
1559
1560 # There used to be targets here but they are no longer useful.
1561
1562 # To build using Ocamlbuild:
1563 # 1) Run "make Makefile" to ensure that the generated files (config.ml, ...)
1564 # are generated.
1565 # 2) Run Ocamlbuild with any target to generate the sanitization script.
1566 # 3) Run ./sanitize to delete the generated files that shouldn't be generated
1567 # (i.e. all lexers and parsers).
1568 # 4) Run Ocamlbuild with the target you need, for example:
1569 # ocamlbuild jc/jc_main.native
1570
1571 # You can also use the Makefile ./build.makefile which has some handy targets.