########################################################################## # # # Copyright (C) 2010-2011 # # François Bobot # # Jean-Christophe Filliâtre # # Claude Marché # # Andrei Paskevich # # # # This software is free software; you can redistribute it and/or # # modify it under the terms of the GNU Library General Public # # License version 2.1, with the special exception on linking # # described in file LICENSE. # # # # This software is distributed in the hope that it will be useful, # # but WITHOUT ANY WARRANTY; without even the implied warranty of # # MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. # # # ########################################################################## include Version VERBOSEMAKE ?= @enable_verbose_make@ ifeq ($(VERBOSEMAKE),yes) QUIET = else QUIET = yes endif # install the binaries DESTDIR = prefix = @prefix@ exec_prefix = @exec_prefix@ datarootdir = @datarootdir@ BINDIR = $(DESTDIR)@bindir@ LIBDIR = $(DESTDIR)@libdir@ DATADIR = $(DESTDIR)@datarootdir@ MANDIR = $(DESTDIR)@mandir@ # OS specific stuff EXE = @EXE@ STRIP = @STRIP@ # other variables OCAMLC = @OCAMLC@ OCAMLOPT = @OCAMLOPT@ OCAMLDEP = @OCAMLDEP@ OCAMLLEX = @OCAMLLEX@ OCAMLYACC = @OCAMLYACC@ OCAMLDOC = @OCAMLDOC@ OCAMLLIB = @OCAMLLIB@ OCAMLBEST = @OCAMLBEST@ OCAMLVERSION = @OCAMLVERSION@ CAMLP5O = @CAMLP5O@ ifeq (@enable_menhirlib@,yes) MENHIR = @MENHIR@ --table MENHIRINC = -I @MENHIRLIB@ MENHIRLIB = menhirLib else MENHIR = @MENHIR@ MENHIRINC = MENHIRLIB = endif RUBBER = @RUBBER@ #PSVIEWER = @PSVIEWER@ #PDFVIEWER = @PDFVIEWER@ BFLAGS = -w Aer-29 -dtypes -g -I src $(INCLUDES) OFLAGS = -w Aer-29 -dtypes -I src $(INCLUDES) ifeq (@enable_profiling@,yes) OFLAGS += -g -p STRIP = true endif # external libraries common to all binaries EXTOBJS = EXTLIBS = str unix nums @META_DYNLINK@ EXTCMA = $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS)) EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS)) ############### # main target ############### all: @OCAMLBEST@ ifeq (@enable_local@,yes) all: install_local endif plugins: plugins.@OCAMLBEST@ .PHONY: byte opt clean depend all install install_local install_no_local .PHONY: plugins plugins.byte plugins.opt ############# # Why library ############# LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \ src/parser/parser.mli src/parser/parser.ml \ src/driver/driver_parser.mli src/driver/driver_parser.ml \ src/driver/driver_lexer.ml LIB_UTIL = stdlib exn_printer debug pp loc print_tree \ cmdline hashweak hashcons util sysutil rc plugin LIB_CORE = ident ty term pattern decl theory task pretty env printer trans LIB_PARSER = ptree denv typing parser lexer LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \ whyconf autodetection LIB_TRANSFORM = simplify_recursive_definition simplify_formula \ inlining split_goal \ eliminate_definition eliminate_algebraic \ eliminate_inductive eliminate_let eliminate_if \ libencoding discriminate protect_enumeration \ encoding encoding_select \ encoding_decorate encoding_bridge encoding_twin \ encoding_explicit encoding_guard encoding_sort \ encoding_instantiate simplify_array filter_trigger \ introduction abstraction close_epsilon lift_epsilon \ eval_match LIB_PRINTER = print_real alt_ergo why3printer smtv1 smtv2 \ coq tptp simplify gappa cvc3 LIBMODULES = src/config \ $(addprefix src/util/, $(LIB_UTIL)) \ $(addprefix src/core/, $(LIB_CORE)) \ $(addprefix src/parser/, $(LIB_PARSER)) \ $(addprefix src/driver/, $(LIB_DRIVER)) \ $(addprefix src/transform/, $(LIB_TRANSFORM)) \ $(addprefix src/printer/, $(LIB_PRINTER)) LIBDIRS = util core parser driver transform printer LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS)) ifeq (@enable_hypothesis_selection@,yes) LIB_TRANSFORM += hypothesis_selection INCLUDES += -I @OCAMLGRAPHLIB@ EXTLIBS += graph endif LIBML = $(addsuffix .ml, $(LIBMODULES)) LIBMLI = $(addsuffix .mli, $(LIBMODULES)) LIBCMO = $(addsuffix .cmo, $(LIBMODULES)) LIBCMX = $(addsuffix .cmx, $(LIBMODULES)) $(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES) $(LIBCMX): OFLAGS += -for-pack Why # build targets byte: src/why.cma opt: src/why.cmxa src/why.cma: src/why.cmo $(OCAMLC) -a $(BFLAGS) -o $@ $^ src/why.cmxa: src/why.cmx $(OCAMLOPT) -a $(OFLAGS) -o $@ $^ src/why.cmo: $(LIBCMO) $(OCAMLC) $(BFLAGS) -pack -o $@ $^ src/why.cmx: $(LIBCMX) $(OCAMLOPT) $(OFLAGS) -pack -o $@ $^ # depend target include .depend.lib .depend.lib: src/config.ml $(LIBGENERATED) $(OCAMLDEP) -slash -I src $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@ depend: .depend.lib # clean target LIBSDIRS = src $(addprefix src/, $(LIBDIRS)) LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \ $(addsuffix /*.annot, $(LIBSDIRS)) \ $(addsuffix /*.output, $(LIBSDIRS)) \ $(addsuffix /*.automaton, $(LIBSDIRS)) \ $(addsuffix /*.o, $(LIBSDIRS)) \ $(addsuffix /*~, $(LIBSDIRS)) clean:: rm -f $(LIBCLEAN) $(LIBGENERATED) rm -f src/why.cm[iox] src/why.[ao] src/why.cma src/why.cmxa rm -f .depend.lib ############### # installation ############### install_no_local:: mkdir -p $(BINDIR) mkdir -p $(LIBDIR)/why3 mkdir -p $(DATADIR)/why3/images mkdir -p $(DATADIR)/why3/emacs mkdir -p $(DATADIR)/why3/lang mkdir -p $(DATADIR)/why3/theories mkdir -p $(DATADIR)/why3/theories/transform mkdir -p $(DATADIR)/why3/modules mkdir -p $(DATADIR)/why3/drivers cp -f theories/*.why $(DATADIR)/why3/theories cp -f theories/transform/*.why $(DATADIR)/why3/theories/transform cp -f modules/*.mlw $(DATADIR)/why3/modules cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers cp -f share/provers-detection-data.conf $(DATADIR)/why3/ cp -f share/images/*.png $(DATADIR)/why3/images cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang install_no_local_lib:: mkdir -p $(OCAMLLIB)/why3 cp -f src/why.cm* $(OCAMLLIB)/why3 cp -f META $(OCAMLLIB)/why3 if test -f src/why.a; then cp -f src/why.a $(OCAMLLIB)/why3; fi ifeq (@enable_local@,yes) install install-lib: @echo "Why is configured in local installation mode." @echo "To install Why, run ./configure --disable-local ; make ; make install" else install: install_no_local install-lib: install_no_local_lib endif install-all: install install-lib ################## # Why binary ################## byte: bin/why3.byte opt: bin/why3.opt bin/why3.opt: src/why.cmxa src/main.cmx $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^ $(STRIP) $@ bin/why3.byte: src/why.cma src/main.cmo $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^ bin/why3: bin/why3.@OCAMLBEST@ ln -sf why3.@OCAMLBEST@ $@ src/main.cmo: src/why.cma src/main.cmx: src/why.cmxa clean:: rm -f src/main.cm[iox] src/main.annot src/main.o rm -f bin/why3.byte bin/why3.opt bin/why3 install_no_local:: cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3 install_local: bin/why3 ######## # Whyml ######## PGM_FILES = pgm_ttree pgm_types pgm_pretty \ pgm_module pgm_wp pgm_env pgm_typing pgm_main PGMMODULES = $(addprefix src/programs/, $(PGM_FILES)) PGMML = $(addsuffix .ml, $(PGMMODULES)) PGMMLI = $(addsuffix .mli, $(PGMMODULES)) PGMCMO = $(addsuffix .cmo, $(PGMMODULES)) PGMCMX = $(addsuffix .cmx, $(PGMMODULES)) $(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs # build targets byte: bin/why3ml.byte opt: bin/why3ml.opt bin/why3ml.opt: src/why.cmxa $(PGMCMX) src/main.cmx $(if $(QUIET), @echo 'Linking $@' &&) \ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^ $(STRIP) $@ bin/why3ml.byte: src/why.cma $(PGMCMO) src/main.cmo $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^ bin/why3ml: bin/why3ml.@OCAMLBEST@ ln -sf why3ml.@OCAMLBEST@ $@ # depend and clean targets include .depend.programs .depend.programs: $(OCAMLDEP) -slash -I src -I src/programs $(PGMML) $(PGMMLI) > $@ depend: .depend.programs clean:: rm -f src/programs/*.cm[iox] src/programs/*.o rm -f src/programs/*.annot src/programs/*~ rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml rm -f .depend.programs # test target %.gui: %.why bin/why3ide.opt bin/why3ide.opt $*.why %: %.mlw bin/why3ml.opt bin/why3ml.opt $*.mlw %: %.why bin/why3.opt bin/why3.opt $*.why %.gui: %.mlw bin/why3ide.opt bin/why3ide.opt $*.mlw %.type: %.mlw bin/why3ide.opt bin/why3ml.opt --type-only $*.mlw install_no_local:: cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml install_local: bin/why3ml ########## # gallery ########## GALLERYPGMS = binary_search bresenham sf same_fringe relabel quicksort \ power mergesort_list mac_carthy isqrt insertion_sort_list flag \ distance muller fib_memo fibonacci \ vstte10_aqueue vstte10_inverting vstte10_max_sum \ vstte10_queens vstte10_search_list \ vacid_0_sparse_array .PHONY: gallery gallery:: @if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi @for f in $(GALLERYPGMS); do \ echo "exporting $$f"; \ mkdir -p $(GALLERYDIR)/$$f; \ cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \ done ######## # Config ######## CONFIG_FILES = whyconfig CONFIGMODULES = $(addprefix src/config/, $(CONFIG_FILES)) CONFIGML = $(addsuffix .ml, $(CONFIGMODULES)) CONFIGMLI = $(addsuffix .mli, $(CONFIGMODULES)) CONFIGCMO = $(addsuffix .cmo, $(CONFIGMODULES)) CONFIGCMX = $(addsuffix .cmx, $(CONFIGMODULES)) $(CONFIGCMO) $(CONFIGCMX): INCLUDES += -I src/programs # build targets byte: bin/why3config.byte opt: bin/why3config.opt bin/why3config.opt: src/why.cmxa $(CONFIGCMX) $(if $(QUIET), @echo 'Linking $@' &&) \ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^ $(STRIP) $@ bin/why3config.byte: src/why.cma $(CONFIGCMO) $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^ bin/why3config: bin/why3config.@OCAMLBEST@ ln -sf why3config.@OCAMLBEST@ $@ # depend and clean targets include .depend.config .depend.config: $(CONFIGGENERATED) $(OCAMLDEP) -slash -I src -I src/config $(CONFIGML) $(CONFIGMLI) > $@ depend: .depend.config clean:: rm -f src/config/*.cm[iox] src/config/*.o rm -f src/config/*.annot src/config/*~ rm -f src/config/*.output src/config/*.automaton rm -f bin/why3config.byte bin/why3config.opt bin/why3config rm -f .why.conf rm -f .depend.config local_config: bin/why3config.@OCAMLBEST@ WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \ --detect --conf_file why.conf install_no_local:: cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config install_local: bin/why3config ############### # IDE ############### ifeq (@enable_ide@,yes) IDE_FILES = xml session gconfig newmain IDEMODULES = $(addprefix src/ide/, $(IDE_FILES)) IDEML = $(addsuffix .ml, $(IDEMODULES)) IDEMLI = $(addsuffix .mli, $(IDEMODULES)) IDECMO = $(addsuffix .cmo, $(IDEMODULES)) IDECMX = $(addsuffix .cmx, $(IDEMODULES)) $(IDECMO) $(IDECMX): INCLUDES += -I src/ide # build targets byte: bin/why3ide.byte opt: bin/why3ide.opt bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@ bin/why3ide.opt bin/why3ide.byte: EXTOBJS += bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2 bin/why3ide.opt: src/why.cmxa $(PGMCMX) $(IDECMX) $(if $(QUIET), @echo 'Linking $@' &&) \ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^ $(STRIP) $@ bin/why3ide.byte: src/why.cma $(PGMCMO) $(IDECMO) $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^ bin/why3ide: bin/why3ide.@OCAMLBEST@ ln -sf why3ide.@OCAMLBEST@ $@ # depend and clean targets include .depend.ide .depend.ide: src/ide/xml.ml $(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@ depend: .depend.ide clean:: rm -f src/ide/xml.ml rm -f src/ide/*.cm[iox] src/ide/*.o rm -f src/ide/*.annot src/ide/*~ rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide rm -f .depend.ide install_no_local:: cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide install_local: bin/why3ide endif ############### # Replayer ############### REPLAYER_FILES = xml session replay REPLAYERMODULES = $(addprefix src/ide/, $(REPLAYER_FILES)) REPLAYERML = $(addsuffix .ml, $(REPLAYERMODULES)) REPLAYERMLI = $(addsuffix .mli, $(REPLAYERMODULES)) REPLAYERCMO = $(addsuffix .cmo, $(REPLAYERMODULES)) REPLAYERCMX = $(addsuffix .cmx, $(REPLAYERMODULES)) $(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide # build targets byte: bin/why3replayer.byte opt: bin/why3replayer.opt bin/why3replayer.opt: src/why.cmxa $(PGMCMX) $(REPLAYERCMX) $(if $(QUIET), @echo 'Linking $@' &&) \ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^ $(STRIP) $@ bin/why3replayer.byte: src/why.cma $(PGMCMO) $(REPLAYERCMO) $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^ bin/why3replayer: bin/why3replayer.@OCAMLBEST@ ln -sf why3replayer.@OCAMLBEST@ $@ # depend and clean targets include .depend.replayer .depend.replayer: src/ide/xml.ml $(OCAMLDEP) -slash -I src -I src/ide $(REPLAYERML) $(REPLAYERMLI) > $@ depend: .depend.replayer clean:: rm -f src/ide/xml.ml rm -f src/ide/*.cm[iox] src/ide/*.o rm -f src/ide/*.annot src/ide/*~ rm -f bin/why3replayer.byte bin/why3replayer.opt bin/why3replayer rm -f .depend.replayer install_no_local:: cp -f bin/why3replayer.@OCAMLBEST@ $(BINDIR)/why3replayer install_local: bin/why3replayer ############### # Bench ############### ifeq (@enable_bench@,yes) BENCH_FILES = bench benchrc benchdb whybench BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES)) BENCHMODULES := src/ide/worker src/ide/db $(BENCHMODULES) BENCHML = $(addsuffix .ml, $(BENCHMODULES)) BENCHMLI = $(addsuffix .mli, $(BENCHMODULES)) BENCHCMO = $(addsuffix .cmo, $(BENCHMODULES)) BENCHCMX = $(addsuffix .cmx, $(BENCHMODULES)) $(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I @SQLITE3LIB@ # build targets byte: bin/why3bench.byte opt: bin/why3bench.opt bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I @SQLITE3LIB@ bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3 bin/why3bench.opt: src/why.cmxa $(PGMCMX) $(BENCHCMX) $(if $(QUIET), @echo 'Linking $@' &&) \ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^ $(STRIP) $@ bin/why3bench.byte: src/why.cma $(PGMCMO) $(BENCHCMO) $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^ bin/why3bench: bin/why3bench.@OCAMLBEST@ ln -sf why3bench.@OCAMLBEST@ $@ # depend and clean targets include .depend.bench .depend.bench: $(OCAMLDEP) -slash -I src -I src/bench -I src/ide $(BENCHML) $(BENCHMLI) > $@ depend: .depend.bench clean:: rm -f src/bench/*.cm[iox] src/bench/*.o rm -f src/bench/*.annot src/bench/*~ rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench rm -f .depend.bench install_no_local:: cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench install_local: bin/why3bench endif ############## # Coq plugin ############## ifeq (@enable_coq_support@,yes) COQGENERATED = src/coq-plugin/g_whytac.ml COQ_FILES = whytac g_whytac COQMODULES = $(addprefix src/coq-plugin/, $(COQ_FILES)) COQML = $(addsuffix .ml, $(COQMODULES)) COQCMO = $(addsuffix .cmo, $(COQMODULES)) COQCMX = $(addsuffix .cmx, $(COQMODULES)) COQTREES = kernel lib interp parsing proofs pretyping tactics library toplevel COQINCLUDES = -I src/coq-plugin $(addprefix -I @COQLIB@/, $(COQTREES)) $(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES) byte: src/coq-plugin/whytac.cma opt: src/coq-plugin/whytac.cmxs src/coq-plugin/whytac.cma: BFLAGS+=-rectypes -I +camlp5 src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5 src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX) $(OCAMLOPT) $(OFLAGS) -o $@ -shared $^ src/coq-plugin/whytac.cma: src/why.cma $(COQCMO) $(OCAMLC) -a $(BFLAGS) -o $@ $^ src/coq-plugin/g_whytac.ml: src/coq-plugin/g_whytac.ml4 $(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@ # depend and clean targets include .depend.coq .depend.coq: $(COQGENERATED) $(OCAMLDEP) -slash -I src -I src/coq-plugin $(COQML) > $@ depend: .depend.coq clean:: rm -f src/coq-plugin/*.cm[iox] src/coq-plugin/*.o rm -f src/coq-plugin/*.cma src/coq-plugin/*.cmxs rm -f src/coq-plugin/*.annot src/coq-plugin/*~ rm -f $(COQGENERATED) rm -f .depend.coq endif ######## # Tptp2why ######## ifeq (@enable_whytptp@,yes) TPTPGENERATED = src/tptp2why/tptpLexer.ml \ src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES)) TPTPML = $(addsuffix .ml, $(TPTPMODULES)) TPTPMLI = $(addsuffix .mli, $(TPTPMODULES)) TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES)) TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES)) $(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR) $(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why # build targets plugins.byte byte: plugins/whytptp.cmo plugins.opt opt : plugins/whytptp.cmxs plugins/whytptp.cmxs plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB) plugins/whytptp.cmxs plugins/whytptp.cmo: INCLUDES += $(MENHIRINC) plugins/whytptp.cmxs: $(TPTPCMX) $(if $(QUIET), @echo 'Linking $@' &&) \ $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^ plugins/whytptp.cmo: $(TPTPCMO) $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLC) $(BFLAGS) -pack -o $@ $^ install_no_local:: cp -f plugins/whytptp.cm* $(LIBDIR)/why3/ # depend and clean targets include .depend.tptp2why .depend.tptp2why: $(TPTPGENERATED) $(OCAMLDEP) -slash -I src -I src/tptp2why $(TPTPML) $(TPTPMLI) > $@ depend: .depend.tptp2why clean:: rm -f $(TPTPGENERATED) rm -f src/tptp2why/*.cm* src/tptp2why/*.o rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts rm -f src/tptp2why/*.output src/tptp2why/*.automaton rm -f plugins/whytptp.cm* plugins/whytptp.o rm -f .depend.tptp2why endif ####### # tools ####### TOOLS = bin/why3-cpulimit byte opt: $(TOOLS) bin/why3-cpulimit: src/tools/@CPULIMIT@.c $(CC) -Wall -o $@ $^ clean:: rm -f bin/why3-cpulimit src/tools/*~ install_no_local:: cp -f bin/why3-cpulimit $(BINDIR)/why3-cpulimit ######### # why3doc ######### # WHY3DOC_FILES = doc_html doc_main WHY3DOC_FILES = to_html WHY3DOCMODULES = $(addprefix src/why3doc/, $(WHY3DOC_FILES)) WHY3DOCML = $(addsuffix .ml, $(WHY3DOCMODULES)) WHY3DOCMLI = $(addsuffix .mli, $(WHY3DOCMODULES)) WHY3DOCCMO = $(addsuffix .cmo, $(WHY3DOCMODULES)) WHY3DOCCMX = $(addsuffix .cmx, $(WHY3DOCMODULES)) $(WHY3DOCCMO) $(WHY3DOCCMX): INCLUDES += -I src/why3doc # build targets byte: bin/why3doc.byte opt: bin/why3doc.opt bin/why3doc.opt: src/why.cmxa $(WHY3DOCCMX) $(if $(QUIET), @echo 'Linking $@' &&) \ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^ $(STRIP) $@ bin/why3doc.byte: src/why.cma $(WHY3DOCCMO) $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^ bin/why3doc: bin/why3doc.@OCAMLBEST@ ln -sf why3doc.@OCAMLBEST@ $@ install_no_local:: cp -f bin/why3doc.@OCAMLBEST@ $(BINDIR)/why3doc # depend and clean targets WHY3DOCGENERATED=src/why3doc/to_html.ml include .depend.why3doc .depend.why3doc: $(WHY3DOCGENERATED) $(OCAMLDEP) -slash -I src -I src/why3doc $(WHY3DOCML) $(WHY3DOCMLI) > $@ depend: .depend.why3doc clean:: rm -f $(WHY3DOCGENERATED) rm -f src/why3doc/*.cm[iox] src/why3doc/*.o rm -f src/why3doc/*.annot src/why3doc/*~ rm -f bin/why3doc.byte bin/why3doc.opt bin/why3doc rm -f .depend.why3doc install_local: bin/why3doc ######## # bench ######## .PHONY: bench test comp_bench_plugins bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) $(MAKE) test-api sh bench/bench \ "bin/why3.@OCAMLBEST@" \ "bin/why3ml.@OCAMLBEST@" BENCH_PLUGINS_CMO := helloworld.cmo BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO)) BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs) comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) # bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS) # bin/why3.byte -D bench/plugins/helloworld.drv \ # tests/test-jcf.why -T Test -G G # bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv \ # tests/test-jcf.why -T Test -G G ############### # test targets ############### test2: bin/why3.byte $(TOOLS) bin/why3.byte tests/test-jcf.why test: bin/why3.byte plugins.byte $(TOOLS) mkdir -p output_why3 bin/why3.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why # bin/why3.byte -D drivers/alt_ergo.drv tests/test-jcf.why -T Test -G G # bin/why3.byte -P alt-ergo --timelimit 3 tests/test-jcf.why -T Test -G G # bin/why3.byte -D drivers/coq.drv tests/test-jcf.why -T Test -G G echo bin/why3.byte -P alt-ergo --timelimit 1 --prove theories/real.why @printf "*** Checking Coq file generation ***\\n" @mkdir -p output_coq @for i in int.Abs int.EuclideanDivision int.ComputerDivision \ real.Abs real.FromIntTest real.SquareTest \ real.ExpLogTest real.PowerTest real.TrigonometryTest \ floating_point.Test map.TestBv32 \ ; do \ printf "Generating Coq file for $$i\\n" && \ bin/why3.byte -P coq -o output_coq -T $$i ; done @printf "*** Checking Coq compilation ***\\n" @for i in output_coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done testl: bin/why3ml.byte ocamlrun -bt bin/why3ml.byte tests/test-pgm-jcf.mlw ocamlrun -bt bin/why3ml.byte -P alt-ergo tests/test-pgm-jcf.mlw testl-debug: bin/why3ml.opt bin/why3ml.opt --debug program_typing tests/test-pgm-jcf.mlw testl-ide: bin/why3ide.opt bin/why3ide.opt tests/test-pgm-jcf.mlw testl-type: bin/why3ml.byte ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw test-api: src/why.cma ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why.cma examples/use_api.ml \ || (printf "Test of Why API calls failed. Please fix it"; exit 2) bts12244: src/why.cma ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why.cma examples/bts12244.ml ## Examples : Plugins ## ifeq (@enable_plugins@,yes) PLUGDIR = examples/plugins/ PLUG_FILES = genequlin PLUGMODULES = $(addprefix $(PLUGDIR), $(PLUG_FILES)) PLUGML = $(addsuffix .ml, $(PLUGMODULES)) PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES)) PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES)) PLUGCMXS = $(addsuffix .cmxs, $(PLUGMODULES)) # ifeq (@enable_plug_support@,yes) # byte: src/plug-plugin/whytac.cma # opt: src/plug-plugin/whytac.cmxs # endif # $(PLUGCMO): src/why.cma # $(PLUGCMXS): src/why.cmxa .PHONY: examples_plugins.byte examples_plugins.opt examples_plugins.byte : $(PLUGCMO) examples_plugins.opt : $(PLUGCMXS) # depend and clean targets include .depend.plug .depend.plug: $(PLUGGENERATED) $(OCAMLDEP) -slash -I src -I $(PLUGDIR) $(PLUGML) | sed "s/cmx/cmxs/" > $@ depend: .depend.plug clean:: rm -f $(PLUGDIR)/*.cm[iox] $(PLUGDIR)/*.o rm -f $(PLUGDIR)/*.cma $(PLUGDIR)/*.cmxs rm -f $(PLUGDIR)/*.annot $(PLUGDIR)/*~ rm -f $(PLUGGENERATED) rm -f .depend.plug endif ################ # documentation ################ .PHONY: doc ifeq (@enable_doc@,yes) doc: doc/manual.pdf # doc/manual.html BNF = qualid constant operator term type formula theory why_file \ typev expr module whyml_file BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF))) doc/%_bnf.tex: doc/%.bnf doc/bnf doc/bnf $< > $@ doc/bnf: doc/bnf.mll $(OCAMLLEX) $< $(OCAMLOPT) -o $@ doc/bnf.ml DOC = api glossary ide intro library macros manpages \ manual starting syntax syntaxref version whyml DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC))) doc/manual.pdf: $(BNFTEX) $(DOCTEX) doc/manual.bib cd doc; $(RUBBER) -d manual.tex # doc/manual.html: doc/manual.tex doc/version.tex # $(MAKE) -C doc manual.html clean:: cd doc; $(RUBBER) -d --clean manual.tex else doc: endif ########## # API DOC ########## .PHONY: apidoc MODULESTODOC = util/util util/hashweak \ core/ident core/ty core/term core/decl core/theory \ core/env core/task \ driver/whyconf driver/driver \ ide/session # transform/introduction \ # ide/db FILESTODOC = $(addsuffix .mli, $(addprefix src/, $(MODULESTODOC))) apidoc: $(FILESTODOC) mkdir -p doc/apidoc $(OCAMLDOC) -d doc/apidoc -html -keep-code $(INCLUDES) \ $(LIBINCLUDES) -I src $(FILESTODOC) # $(LIBML) install_apidoc: apidoc rsync -av doc/apidoc/ marche@scm.gforge.inria.fr:/home/groups/why3/htdocs/apidoc/ doc/apidoc.tex: $(FILESTODOC) $(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \ $(LIBINCLUDES) -I src $(FILESTODOC) # $(LIBML) clean:: rm -f doc/apidoc/* ################ # generic rules ################ %.cmi: %.mli $(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) $< %.cmo: %.ml $(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) $< %.cmx: %.ml $(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -c $(OFLAGS) $< %.cmxs: %.ml $(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $< %.ml: %.mll $(OCAMLLEX) $< %.ml %.mli: %.mly $(OCAMLYACC) -v $< # .ml4.ml: # $(CAMLP4) pr_o.cmo -impl $< > $@ # lib/coq/%.vo: lib/coq/%.v # $(COQC8) -I lib/coq $< # lib/coq-v7/%.vo: lib/coq-v7/%.v # $(COQC7) -I lib/coq-v7 $< # jc/jc_ai.ml: jc/jc_annot_inference.ml jc/jc_annot_fail.ml Makefile # if test "@enable_apron@" = "yes" ; then \ # echo "# 1 \"jc/jc_annot_inference.ml\"" > jc/jc_ai.ml; \ # cat jc/jc_annot_inference.ml >> jc/jc_ai.ml; \ # else \ # echo "# 1 \"jc/jc_annot_fail.ml\"" > jc/jc_ai.ml; \ # cat jc/jc_annot_fail.ml >> jc/jc_ai.ml; \ # fi # %_why.v: %.mlw $(BINARY) # $(BINARY) -coq $*.mlw # %_why.pvs: %.mlw $(BINARY) # $(BINARY) -pvs $*.mlw # Emacs tags ############ tags: find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \ etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ "--regex=/and[ \t]+\([^ \t]+\)/\1/" \ "--regex=/type[ \t]+\([^ \t]+\)/\1/" \ "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ "--regex=/module[ \t]+\([^ \t]+\)/\1/" otags: find \( -name '*.ml' -or -name '*.mli' \) -print0 | xargs -0 otags # otags src/*.mli src/*.ml c/*.mli c/*.ml intf/*.mli intf/*.ml # the previous seems broken. This one is intented for vi(m) users, but could # be adapted for emacs (remove the -vi option ?) otags-vi: find \( -name '*.ml' -or -name '*.mli' \) -print0 | xargs -0 otags -vi wc: ocamlwc -p src/*.ml* src/*/*.ml* dep: depend cat .depend* | ocamldot | dot -Tpdf > dep.pdf # $(PDFVIEWER) dep.pdf # distrib ######### NAME = why3-$(VERSION) DISTRIB_DIR = distrib/$(NAME) DISTRIB_TAR = $(DISTRIB_DIR).tar.gz # CHANGES (not up-to-date, moreover is in French) DISTRIB_FILES = Version Makefile.in configure.in META.in configure .depend.* \ README INSTALL OCAML-LICENSE LICENSE \ src/*.ml* src/*/*.ml* src/*/*.c \ src/config.sh.in \ doc/version.tex.in doc/manual.pdf \ drivers/*.drv \ examples/*.why examples/programs/*.mlw examples/tptp/*.why \ examples/my_cosine/*.v \ theories/*.why theories/*/*.why \ modules/*.mlw \ share/provers-detection-data.conf.in \ share/emacs/why.el share/images/*.png share/lang/*.lang # TODO? # share/zsh ? # symbolic links in share/ ? distrib:: $(DISTRIB_TAR) rmdistrib: rm -rf $(DISTRIB_DIR) redistrib: rmdistrib distrib $(DISTRIB_TAR): doc/manual.pdf @if test -d $(DISTRIB_DIR); then \ echo "Hum... there is already a directory $(NAME)"; \ echo "Please increase the version number"; exit 1; \ fi mkdir -p $(DISTRIB_DIR) mkdir -p $(DISTRIB_DIR)/bin mkdir -p $(DISTRIB_DIR)/share mkdir -p $(DISTRIB_DIR)/plugins ln -s ../drivers $(DISTRIB_DIR)/share/drivers ln -s ../modules $(DISTRIB_DIR)/share/modules ln -s ../theories $(DISTRIB_DIR)/share/theories cp --parents $(DISTRIB_FILES) $(DISTRIB_DIR) cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar # distrib export: source export-doc export-www export-examples export-examples-c linux # # export-www: # echo "<#def version>$(VERSION)" > /users/demons/filliatr/www/why/version.prehtml # echo "<#def cversion>$(CVERSION)" >> /users/demons/filliatr/www/why/version.prehtml # $(MAKE) -C /users/demons/filliatr/www/why install # # # tarball: # mkdir -p export # cd export; rm -rf $(NAME) $(NAME).tar.gz # $(MAKE) export/$(NAME).tar.gz # # EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw # # export-examples: # cp --parents $(EXFILES) $(WWW) # $(MAKE) -C $(WWW)/examples clean depend # echo "*** faire make all dans $(WWW)/examples ***" # # export-examples-c: # mkdir -p $(WWW)/caduceus/examples # cd examples-c; cp --parents */*.c */*.h $(WWW)/caduceus/examples # mkdir -p $(WWW)/caduceus/examples/bench # cp bench/c/good/*.c $(WWW)/caduceus/examples/bench # rm -f $(WWW)/caduceus/examples/bench/test.c # # export-doc: $(DOC) # cp doc/manual.ps doc/manual.html $(WWW)/manual # cp doc/logic_syntax.bnf $(WWW)/manual # (cd $(WWW)/manual; hacha manual.html) # cp doc/caduceus.ps doc/caduceus.html $(WWW)/caduceus/manual # (cd $(WWW)/caduceus/manual; hacha caduceus.html) # cp doc/krakatoa.pdf doc/krakatoa.html $(WWWKRAKATOA)/manual # (cd $(WWWKRAKATOA)/manual; hacha krakatoa.html) # # OSTYPE ?= linux # # BINARYNAME = $(NAME)-$(OSTYPE) # # linux: binary # # ALLBINARYFILES = $(FILES) $(BINARYFILES) # # binary: $(ALLBINARYFILES) # mkdir -p export/$(BINARYNAME) # cp --parents $(ALLBINARYFILES) export/$(BINARYNAME) # (cd export; tar czf $(BINARYNAME).tar.gz $(BINARYNAME)) # cp export/$(BINARYNAME).tar.gz $(FTP) ############### # file headers ############### headers: headache -c misc/headache_config.txt -h misc/header.txt \ Makefile.in configure.in src/*.ml* src/*/*.ml* \ src/tools/cpulimit.c headache -c misc/headache_config.txt -h misc/header_gm.txt \ src/transform/abstraction.ml* \ src/transform/simplify_formula.ml* \ src/printer/gappa.ml* headache -c misc/headache_config.txt -h misc/header_jk.txt \ src/transform/close_epsilon.ml* \ src/transform/lift_epsilon.ml* headache -c misc/headache_config.txt -h misc/header_sc.txt \ src/transform/hypothesis_selection.ml* \ src/tptp2why/*.ml* sed -i -f misc/fixnames.sed -- \ Makefile.in configure.in src/*.ml* src/*/*.ml* \ src/tools/cpulimit.c ######### # myself ######### Makefile: Makefile.in config.status ./config.status chmod --file $@ src/config.sh: src/config.sh.in config.status ./config.status chmod --file $@ src/config.ml: src/config.sh LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh doc/version.tex: doc/version.tex.in config.status ./config.status chmod --file $@ share/provers-detection-data.conf: share/provers-detection-data.conf.in config.status ./config.status chmod --file $@ # We want it to be always up-ot-date Makefile : share/provers-detection-data.conf config.status: configure Version ./config.status --recheck opt byte : META share/provers-detection-data.conf META: META.in config.status ./config.status chmod --file $@ configure: configure.in autoconf ################### # clean and depend ################### .PHONY: distclean distclean: clean rm -f config.status config.cache config.log \ Makefile src/config.ml doc/version.tex depend: rm -f $^ $(MAKE) $^ ################################################################# # Building the Why platform with ocamlbuild (OCaml 3.10 needed) # ################################################################# # There used to be targets here but they are no longer useful. # To build using Ocamlbuild: # 1) Run "make Makefile" to ensure that the generated files (config.ml, ...) # are generated. # 2) Run Ocamlbuild with any target to generate the sanitization script. # 3) Run ./sanitize to delete the generated files that shouldn't be generated # (i.e. all lexers and parsers). # 4) Run Ocamlbuild with the target you need, for example: # ocamlbuild jc/jc_main.native # You can also use the Makefile ./build.makefile which has some handy targets.