#################################################################### # # # The Why3 Verification Platform / The Why3 Development Team # # Copyright 2010-2017 -- INRIA - CNRS - Paris-Sud University # # # # This software is distributed under the terms of the GNU Lesser # # General Public License version 2.1, with the special exception # # on linking described in file LICENSE. # # # #################################################################### VERBOSEMAKE ?= @enable_verbose_make@ ifeq ($(VERBOSEMAKE),yes) SHOW = @true HIDE = else SHOW = @echo HIDE = @ 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@ TOOLDIR = $(LIBDIR)/why3/commands # OS specific stuff EXE = @EXE@ # other variables CC = @CC@ MKDIR_P = @MKDIR_P@ INSTALL = @INSTALL@ INSTALL_DATA = @INSTALL_DATA@ OCAMLC = @OCAMLC@ OCAMLOPT = @OCAMLOPT@ OCAMLDEP = @OCAMLDEP@ OCAMLLEX = @OCAMLLEX@ OCAMLYACC = @OCAMLYACC@ OCAMLDOC = @OCAMLDOC@ OCAMLLIB = @OCAMLLIB@ OCAMLINSTALLLIB = $(DESTDIR)@OCAMLINSTALLLIB@ OCAMLBEST = @OCAMLBEST@ OCAMLVERSION = @OCAMLVERSION@ COQC = @COQC@ COQDEP = @COQDEP@ COQCAMLP = @COQCAMLP@ COQCAMLPLIB = @COQCAMLPLIB@ FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@ ifeq (@enable_menhirLib@,yes) MENHIR = @MENHIR@ --table else MENHIR = @MENHIR@ endif DEPFLAGS = -slash -I lib/why3 ifeq (@OCAMLBEST@,opt) # the semantics of the -native flag changed in ocaml 4.03.0 #DEPFLAGS += -native endif RUBBER = @RUBBER@ HEVEA = @HEVEA@ HACHA = @HACHA@ EMACS = @EMACS@ #PSVIEWER = @PSVIEWER@ #PDFVIEWER = @PDFVIEWER@ INCLUDES = @ZIPINCLUDE@ @MENHIRINCLUDE@ # warnings are enabled and non fatal by default, except: # - disabled: # 4 Fragile pattern matching: matching that will remain complete even # if additional constructors are added to one of the variant types # matched. # 9 Missing fields in a record pattern. # 41 Ambiguous constructor or label name. # 44 Open statement shadows an already defined identifier. # 45 Open statement shadows an already defined label or constructor. # 50 Unexpected documentation comment. # 52 The argument of this constructor should not be matched against a # constant pattern; the actual value of the argument could change # in the future. # - fatal: # 5 Partially applied function: expression whose result has function # type and is ignored. # 48 Implicit elimination of optional arguments. WARNINGS = A-4-9-41-44-45-50-52@5@48 OFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g -I lib/why3 $(INCLUDES) BFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g -I lib/why3 $(INCLUDES) OLINKFLAGS = -linkall $(EXTCMXA) BLINKFLAGS = -linkall $(EXTCMA) ifeq (@enable_profiling@,yes) OFLAGS += -g -p endif # see http://caml.inria.fr/mantis/view.php?id=4991 CMIHACK = -intf-suffix .cmi # external libraries common to all binaries EXTOBJS = @MENHIRLIB@ EXTLIBS = str unix nums dynlink @ZIPLIB@ EXTCMA = $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS)) EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS)) INSTALLED_LIB_EXTS = a cma cmx cmi cmxa cmxs COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti annot dep conflicts TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV}) ############### # main target ############### all: @OCAMLBEST@ plugins: plugins.@OCAMLBEST@ opt: plugins.opt byte: plugins.byte ifeq (@enable_local@,yes) all: install_local endif .PHONY: byte opt clean depend all install install_local install_no_local .PHONY: plugins plugins.byte plugins.opt CLEANDIRS = CLEANLIBS = GENERATED = ############## # Why3 library ############## LIBGENERATED = src/util/config.ml \ src/util/rc.ml src/util/lexlib.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 \ src/driver/parse_smtv2_model_parser.mli src/driver/parse_smtv2_model_parser.ml \ src/driver/parse_smtv2_model_lexer.ml \ src/session/compress.ml src/session/xml.ml \ src/session/strategy_parser.ml \ lib/ocaml/why3__BigInt_compat.ml LIB_UTIL = config bigInt util opt lists strings \ extmap extset exthtbl weakhtbl \ hashcons stdlib exn_printer pp json debug loc lexlib print_tree \ cmdline warning sysutil rc plugin bigInt number pqueue LIB_CORE = ident ty term pattern decl theory \ task pretty dterm env trans printer model_parser LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer driver \ whyconf autodetection \ smt2_model_defs parse_smtv2_model_parser \ collect_data_model parse_smtv2_model_lexer parse_smtv2_model \ parse_smtv2_model LIB_MLW = ity expr dexpr pdecl pmodule LIB_PARSER = ptree glob parser typing lexer LIB_TRANSFORM = simplify_formula inlining split_goal induction \ detect_polymorphism reduction_engine compute \ eliminate_definition eliminate_algebraic \ eliminate_inductive eliminate_let eliminate_if \ libencoding discriminate encoding encoding_select \ encoding_guards_full encoding_tags_full \ encoding_guards encoding_tags encoding_twin \ encoding_sort simplify_array filter_trigger \ introduction abstraction close_epsilon lift_epsilon \ eliminate_epsilon intro_projections_counterexmp \ intro_vc_vars_counterexmp prepare_for_counterexmp \ eval_match instantiate_predicate smoke_detector \ induction_pr prop_curry eliminate_literal LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\ pvs isabelle \ simplify gappa cvc3 yices mathematica LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \ mlw_dexpr mlw_typing mlw_driver mlw_exec mlw_ocaml \ mlw_main mlw_interp LIB_SESSION = compress xml termcode session session_tools strategy \ strategy_parser session_scheduler LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \ $(addprefix src/core/, $(LIB_CORE)) \ $(addprefix src/driver/, $(LIB_DRIVER)) \ $(addprefix src/mlw/, $(LIB_MLW)) \ $(addprefix src/parser/, $(LIB_PARSER)) \ $(addprefix src/transform/, $(LIB_TRANSFORM)) \ $(addprefix src/printer/, $(LIB_PRINTER)) \ $(addprefix src/whyml/, $(LIB_WHYML)) \ $(addprefix src/session/, $(LIB_SESSION)) LIBDIRS = util core driver mlw parser transform printer whyml session LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS)) LIBDEP = $(addsuffix .dep, $(LIBMODULES)) LIBCMO = $(addsuffix .cmo, $(LIBMODULES)) LIBCMX = $(addsuffix .cmx, $(LIBMODULES)) $(LIBDEP): DEPFLAGS += $(LIBINCLUDES) $(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES) $(LIBCMX): OFLAGS += -for-pack Why3 $(LIBDEP): $(LIBGENERATED) # Zarith ifeq (@enable_zarith@,yes) lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_zarith.ml cp lib/ocaml/why3__BigInt_zarith.ml $@ else lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_num.ml cp lib/ocaml/why3__BigInt_num.ml $@ endif # Ocamlzip ifeq (@enable_zip@,yes) src/session/compress.ml: config.status src/session/compress_z.ml cp src/session/compress_z.ml $@ else src/session/compress.ml: config.status src/session/compress_none.ml cp src/session/compress_none.ml $@ endif # hide deprecated warnings for strings src/util/strings.cmo:: WARNINGS:=$(WARNINGS)-3 src/util/strings.cmx:: WARNINGS:=$(WARNINGS)-3 # hide warning 'no cmx file was found in path for module ..., and its interface was not compiled with -opaque' for the coq tactic src/coq-tactic/why3tac.cmx:: WARNINGS:=$(WARNINGS)-58 # build targets byte: lib/why3/why3.cma opt: lib/why3/why3.cmxa lib/why3/why3.cma: lib/why3/why3.cmo lib/why3/why3.cmxa: lib/why3/why3.cmx lib/why3/why3.cmo: $(LIBCMO) $(SHOW) 'Linking $@' $(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^ lib/why3/why3.cmx: $(LIBCMX) lib/why3/why3.cmo $(SHOW) 'Linking $@' $(HIDE)$(OCAMLOPT) $(OFLAGS) $(CMIHACK) -pack -o $@ $(filter %.cmx, $^) # clean and depend ifneq "$(MAKECMDGOALS:clean%=clean)" "clean" -include $(LIBDEP) endif depend: $(LIBDEP) CLEANDIRS += src $(addprefix src/, $(LIBDIRS)) CLEANLIBS += lib/why3/why3session lib/why3/why3 GENERATED += $(LIBGENERATED) ############### # installation ############### clean_old_install:: rm -rf $(LIBDIR)/why3 rm -rf $(DATADIR)/why3 rm -rf $(OCAMLINSTALLLIB)/why3 install_no_local:: clean_old_install $(MKDIR_P) $(BINDIR) $(MKDIR_P) $(LIBDIR)/why3 $(MKDIR_P) $(TOOLDIR) $(MKDIR_P) $(DATADIR)/why3 $(MKDIR_P) $(DATADIR)/why3/images $(MKDIR_P) $(DATADIR)/why3/vim $(MKDIR_P) $(DATADIR)/why3/vim/ftdetect $(MKDIR_P) $(DATADIR)/why3/vim/syntax $(MKDIR_P) $(DATADIR)/why3/lang $(MKDIR_P) $(DATADIR)/why3/theories $(MKDIR_P) $(DATADIR)/why3/modules/mach $(MKDIR_P) $(DATADIR)/why3/drivers $(INSTALL_DATA) theories/*.why $(DATADIR)/why3/theories $(INSTALL_DATA) modules/*.mlw $(DATADIR)/why3/modules $(INSTALL_DATA) modules/mach/*.mlw $(DATADIR)/why3/modules/mach $(INSTALL_DATA) drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers $(INSTALL_DATA) LICENSE $(DATADIR)/why3/ $(INSTALL_DATA) share/provers-detection-data.conf $(DATADIR)/why3/ for i in share/images/*.rc; do \ d=`basename $$i .rc`; \ $(INSTALL_DATA) $$i $(DATADIR)/why3/images; \ $(MKDIR_P) $(DATADIR)/why3/images/$$d; \ $(INSTALL_DATA) share/images/$$d/* $(DATADIR)/why3/images/$$d; \ done $(INSTALL_DATA) share/images/*.png $(DATADIR)/why3/images $(INSTALL_DATA) share/why3session.dtd $(DATADIR)/why3 $(INSTALL_DATA) share/Makefile.config $(DATADIR)/why3 $(INSTALL_DATA) share/vim/ftdetect/why3.vim $(DATADIR)/why3/vim/ftdetect/why3.vim $(INSTALL_DATA) share/vim/syntax/why3.vim $(DATADIR)/why3/vim/syntax/why3.vim $(INSTALL_DATA) share/lang/why3.lang $(DATADIR)/why3/lang/why3.lang install_no_local_lib:: $(MKDIR_P) $(OCAMLINSTALLLIB)/why3 $(INSTALL_DATA) $(wildcard $(addprefix lib/why3/why3., $(INSTALLED_LIB_EXTS))) \ lib/why3/META $(OCAMLINSTALLLIB)/why3 ifeq (@enable_local@,yes) install install-lib: @echo "Why3 is configured in local installation mode." @echo "To install Why3, run ./configure --disable-local ; make ; make install" else install: clean_old_install install_no_local install-lib: install_no_local_lib endif install-all: install install-lib ################## # Uninstallation ################## uninstall: clean_old_install ################## # Why3 emacs mode ################## %.elc: %.el $(EMACS) --batch --no-init-file -f batch-byte-compile $< clean_old_install:: rm -f $(DATADIR)/emacs/site-lisp/why3.el rm -f $(DATADIR)/emacs/site-lisp/why3.elc install_no_local:: $(MKDIR_P) $(DATADIR)/emacs/site-lisp/ $(INSTALL_DATA) share/emacs/why3.el $(DATADIR)/emacs/site-lisp/why3.el ifeq (@enable_emacs_compilation@,yes) $(INSTALL_DATA) share/emacs/why3.elc $(DATADIR)/emacs/site-lisp/why3.elc endif ifeq (@enable_emacs_compilation@,yes) all: share/emacs/why3.elc endif ################## # Why3 plugins ################## PLUGGENERATED = plugins/tptp/tptp_lexer.ml \ plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli \ plugins/python/py_lexer.ml \ plugins/python/py_parser.ml plugins/python/py_parser.mli \ plugins/parser/dimacs.ml \ PLUG_PARSER = genequlin dimacs PLUG_PRINTER = PLUG_TRANSFORM = PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer PLUG_PYTHON = py_ast py_parser py_lexer py_main PLUGINS = genequlin dimacs tptp python TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP)) PYTHONMODULES = $(addprefix plugins/python/, $(PLUG_PYTHON)) TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES)) TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES)) PYTHONCMO = $(addsuffix .cmo, $(PYTHONMODULES)) PYTHONCMX = $(addsuffix .cmx, $(PYTHONMODULES)) ifeq (@enable_hypothesis_selection@,yes) PLUG_TRANSFORM += hypothesis_selection PLUGINS += hypothesis_selection lib/plugins/hypothesis_selection.cmxs: INCLUDES += -I @OCAMLGRAPHLIB@ lib/plugins/hypothesis_selection.cmo: INCLUDES += -I @OCAMLGRAPHLIB@ lib/plugins/hypothesis_selection.cmxs: OFLAGS += graph.cmxa lib/plugins/hypothesis_selection.cmo: BFLAGS += graph.cmo endif PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \ $(addprefix plugins/printer/, $(PLUG_PRINTER)) \ $(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \ $(TPTPMODULES) $(PYTHONMODULES) PLUGDEP = $(addsuffix .dep, $(PLUGMODULES)) PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES)) PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES)) PLUGDIRS = parser printer transform tptp python PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS)) $(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES) $(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES) $(PLUGDEP): $(PLUGGENERATED) LIBPLUGCMO = $(addsuffix .cmo, $(addprefix lib/plugins/, $(PLUGINS))) LIBPLUGCMXS = $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS))) plugins.byte: $(LIBPLUGCMO) plugins.opt : $(LIBPLUGCMXS) lib/plugins/%.cmxs: plugins/parser/%.cmx $(SHOW) 'Linking $@' $(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $< lib/plugins/%.cmo: plugins/parser/%.cmo $(SHOW) 'Linking $@' $(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $< lib/plugins/%.cmxs: plugins/printer/%.cmx $(SHOW) 'Linking $@' $(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $< lib/plugins/%.cmo: plugins/printer/%.cmo $(SHOW) 'Linking $@' $(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $< lib/plugins/%.cmxs: plugins/transform/%.cmx $(SHOW) 'Linking $@' $(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $< lib/plugins/%.cmo: plugins/transform/%.cmo $(SHOW) 'Linking $@' $(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $< lib/plugins/tptp.cmxs: $(TPTPCMX) $(SHOW) 'Linking $@' $(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^ lib/plugins/tptp.cmo: $(TPTPCMO) $(SHOW) 'Linking $@' $(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^ lib/plugins/python.cmxs: $(PYTHONCMX) $(SHOW) 'Linking $@' $(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^ lib/plugins/python.cmo: $(PYTHONCMO) $(SHOW) 'Linking $@' $(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^ # depend and clean targets ifneq "$(MAKECMDGOALS:clean%=clean)" "clean" -include $(PLUGDEP) endif depend: $(PLUGDEP) CLEANDIRS += plugins $(addprefix plugins/, $(PLUGDIRS)) lib/plugins GENERATED += $(PLUGGENERATED) install_no_local:: $(MKDIR_P) $(LIBDIR)/why3/plugins $(INSTALL_DATA) $(wildcard $(LIBPLUGCMO) $(LIBPLUGCMXS)) $(LIBDIR)/why3/plugins ############### # Why3 commands ############### TOOLSGENERATED = src/tools/why3wc.ml TOOLS_BIN = why3config why3execute why3extract why3prove \ why3realize why3replay why3wc TOOLS_FILES = main $(TOOLS_BIN) TOOLSMODULES = $(addprefix src/tools/, $(TOOLS_FILES)) TOOLSDEP = $(addsuffix .dep, $(TOOLSMODULES)) TOOLSCMO = $(addsuffix .cmo, $(TOOLSMODULES)) TOOLSCMX = $(addsuffix .cmx, $(TOOLSMODULES)) $(TOOLSDEP): DEPFLAGS += -I src/tools $(TOOLSCMO) $(TOOLSCMX): INCLUDES += -I src/tools $(TOOLSDEP): $(TOOLSGENERATED) byte: bin/why3.byte $(TOOLS_BIN:%=bin/%.byte) opt: bin/why3.opt $(TOOLS_BIN:%=bin/%.opt) bin/why3.opt: lib/why3/why3.cmxa src/tools/main.cmx bin/why3.byte: lib/why3/why3.cma src/tools/main.cmo bin/why3config.opt: lib/why3/why3.cmxa src/tools/why3config.cmx bin/why3config.byte: lib/why3/why3.cma src/tools/why3config.cmo bin/why3execute.opt: lib/why3/why3.cmxa src/tools/why3execute.cmx bin/why3execute.byte: lib/why3/why3.cma src/tools/why3execute.cmo bin/why3extract.opt: lib/why3/why3.cmxa src/tools/why3extract.cmx bin/why3extract.byte: lib/why3/why3.cma src/tools/why3extract.cmo bin/why3prove.opt: lib/why3/why3.cmxa src/tools/why3prove.cmx bin/why3prove.byte: lib/why3/why3.cma src/tools/why3prove.cmo bin/why3realize.opt: lib/why3/why3.cmxa src/tools/why3realize.cmx bin/why3realize.byte: lib/why3/why3.cma src/tools/why3realize.cmo bin/why3replay.opt: lib/why3/why3.cmxa src/tools/why3replay.cmx bin/why3replay.byte: lib/why3/why3.cma src/tools/why3replay.cmo bin/why3wc.opt: src/tools/why3wc.cmx bin/why3wc.byte: src/tools/why3wc.cmo clean_old_install:: rm -f $(TOOLS_BIN:%=$(TOOLDIR)/%$(EXE)) $(BINDIR)/why3$(EXE) rm -f $(BINDIR)/why3bench$(EXE) $(BINDIR)/why3replayer$(EXE) install_no_local:: $(INSTALL) bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE) $(INSTALL) bin/why3config.@OCAMLBEST@ $(TOOLDIR)/why3config$(EXE) $(INSTALL) bin/why3execute.@OCAMLBEST@ $(TOOLDIR)/why3execute$(EXE) $(INSTALL) bin/why3extract.@OCAMLBEST@ $(TOOLDIR)/why3extract$(EXE) $(INSTALL) bin/why3prove.@OCAMLBEST@ $(TOOLDIR)/why3prove$(EXE) $(INSTALL) bin/why3realize.@OCAMLBEST@ $(TOOLDIR)/why3realize$(EXE) $(INSTALL) bin/why3replay.@OCAMLBEST@ $(TOOLDIR)/why3replay$(EXE) $(INSTALL) bin/why3wc.@OCAMLBEST@ $(TOOLDIR)/why3wc$(EXE) install_local:: bin/why3 $(addprefix bin/,$(TOOLS_BIN)) bin/%: bin/%.@OCAMLBEST@ ln -sf $(notdir $<) $@ install_local:: share/drivers share/modules share/theories share/drivers: ln -snf ../drivers share/drivers share/modules: ln -snf ../modules share/modules share/theories: ln -snf ../theories share/theories ifneq "$(MAKECMDGOALS:clean%=clean)" "clean" -include $(TOOLSDEP) endif depend: $(TOOLSDEP) CLEANDIRS += src/tools GENERATED += $(TOOLSGENERATED) clean:: rm -f bin/why3* ############## # test targets ############## %.gui: %.why bin/why3ide.opt bin/why3ide.opt $*.why %: %.mlw bin/why3.opt bin/why3.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/why3.opt --type-only $*.mlw ############## # Why3server # ############## SERVER_MODULES := logging arraylist options queue readbuf request \ writebuf server-unix server-win CPULIM_MODULES := cpulimit-unix cpulimit-win SERVER_O := $(addprefix src/server/, $(addsuffix .o, $(SERVER_MODULES))) CPULIM_O := $(addprefix src/server/, $(addsuffix .o, $(CPULIM_MODULES))) TOOLS = lib/why3server$(EXE) lib/why3cpulimit$(EXE) all: $(TOOLS) lib/why3server$(EXE): $(SERVER_O) $(CC) -Wall -o $@ $^ lib/why3cpulimit$(EXE): $(CPULIM_O) $(CC) -Wall -o $@ $^ %.o: %.c $(CC) -Wall -O -g -o $@ -c $< install_no_local:: $(MKDIR_P) $(LIBDIR)/why3 $(INSTALL) lib/why3server$(EXE) $(LIBDIR)/why3/why3server$(EXE) $(INSTALL) lib/why3cpulimit$(EXE) $(LIBDIR)/why3/why3cpulimit$(EXE) $(INSTALL) lib/why3-call-pvs $(LIBDIR)/why3/why3-call-pvs clean:: rm -f $(SERVER_O) $(CPULIM_O) $(TOOLS) ########## # gallery ########## # we export exactly the programs that have a why3session.xml file .PHONY: gallery gallery:: gallery-simple gallery-subs .PHONY: gallery-simple gallery-simple:: @if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi @for x in examples/*/why3session.xml ; do \ d=`dirname $$x`; \ f=`basename $$d`; \ echo "exporting $$f"; \ mkdir -p $(GALLERYDIR)/$$f; \ WHY3CONFIG="" bin/why3session.@OCAMLBEST@ html $$x -o $(GALLERYDIR)/$$f; \ cp examples/$$f.mlw $(GALLERYDIR)/$$f/; \ cd examples/; \ rm -f $(GALLERYDIR)/$$f/$$f.zip; \ zip -q -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \ cd ..; \ done .PHONY: gallery-subs GALLERYSUBS=WP_revisited verifythis_2016_matrix_multiplication avl double_wp gallery-subs:: @if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi @for d in $(GALLERYSUBS) ; do \ echo "exporting examples/$$d"; \ mkdir -p $(GALLERYDIR)/$$d; \ cd examples/$$d; \ WHY3CONFIG="" ../../bin/why3doc.@OCAMLBEST@ -L ../../theories -L ../../modules -L . --stdlib-url http://why3.lri.fr/stdlib/ *.mlw -o $(GALLERYDIR)/$$d; \ cd ..; \ rm -f $(GALLERYDIR)/$$d/$$d.zip; \ zip -q -r $(GALLERYDIR)/$$d/$$d.zip $$d; \ cd ..; \ done %-gallery:: @if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi x=$*/why3session.xml; \ d=`dirname $$x`; \ f=`basename $$d`; \ echo "exporting $$f"; \ rm -f $$d/*.bak; \ mkdir -p $(GALLERYDIR)/$$f; \ WHY3CONFIG="" bin/why3session.@OCAMLBEST@ html $$d -o $(GALLERYDIR)/$$f; \ if test -f examples/$$f.mlw; then cp examples/$$f.mlw $(GALLERYDIR)/$$f/; fi; \ if test -f examples/$$f.why; then cp examples/$$f.why $(GALLERYDIR)/$$f/; fi; \ cd examples/; \ rm -f $(GALLERYDIR)/$$f/$$f.zip; \ zip -q -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f ######## # XML DTD validation ######## .PHONY: xml-validate xml-validate: @for x in `find examples/ -name why3session.xml`; do \ xmllint --noout --valid $$x 2>&1 | head -1; \ done xml-validate-local: @for x in `find examples/ -name why3session.xml`; do \ xmllint --noout --dtdvalid share/why3session.dtd $$x 2>&1 | head -1; \ done ############### # IDE ############### ifeq (@enable_ide@,yes) IDE_FILES = gconfig gmain IDEMODULES = $(addprefix src/ide/, $(IDE_FILES)) IDEDEP = $(addsuffix .dep, $(IDEMODULES)) IDECMO = $(addsuffix .cmo, $(IDEMODULES)) IDECMX = $(addsuffix .cmx, $(IDEMODULES)) $(IDEDEP): DEPFLAGS += -I src/ide $(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: EXTLIBS += lablgtk lablgtksourceview2 bin/why3ide.opt: lib/why3/why3.cmxa src/ide/resetgc.o $(IDECMX) $(SHOW) 'Linking $@' $(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^ bin/why3ide.byte: lib/why3/why3.cma src/ide/resetgc.o $(IDECMO) $(SHOW) 'Linking $@' $(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^ src/ide/resetgc.o: src/ide/resetgc.c $(SHOW) 'Ocamlc $<' $(HIDE)$(OCAMLC) -c -ccopt "-Wall -o $@" $< # depend and clean targets ifneq "$(MAKECMDGOALS:clean%=clean)" "clean" -include $(IDEDEP) endif depend: $(IDEDEP) CLEANDIRS += src/ide clean_old_install:: rm -f $(BINDIR)/why3ide$(EXE) install_no_local:: $(INSTALL) bin/why3ide.@OCAMLBEST@ $(TOOLDIR)/why3ide$(EXE) install_local:: bin/why3ide endif ############### # Session ############### SESSION_FILES = why3session_lib why3session_copy why3session_info \ why3session_latex why3session_html why3session_rm \ why3session_output why3session_run why3session_csv \ why3session_main SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES)) SESSIONDEP = $(addsuffix .dep, $(SESSIONMODULES)) SESSIONCMO = $(addsuffix .cmo, $(SESSIONMODULES)) SESSIONCMX = $(addsuffix .cmx, $(SESSIONMODULES)) $(SESSIONDEP): DEPFLAGS += -I src/why3session $(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session # build targets byte: bin/why3session.byte opt: bin/why3session.opt bin/why3session.opt: lib/why3/why3.cmxa $(SESSIONCMX) $(SHOW) 'Linking $@' $(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^ bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO) $(SHOW) 'Linking $@' $(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^ # depend and clean targets ifneq "$(MAKECMDGOALS:clean%=clean)" "clean" -include $(SESSIONDEP) endif depend: $(SESSIONDEP) CLEANDIRS += src/why3session clean_old_install:: rm -f $(BINDIR)/why3session$(EXE) install_no_local:: $(INSTALL) bin/why3session.@OCAMLBEST@ $(TOOLDIR)/why3session$(EXE) install_local:: bin/why3session ############## # Coq plugin ############## ifeq (@enable_coq_tactic@,yes) COQPGENERATED = src/coq-tactic/why3tac.ml COQP_FILES = why3tac COQPMODULES = $(addprefix src/coq-tactic/, $(COQP_FILES)) COQPDEP = $(addsuffix .dep, $(COQPMODULES)) COQPCMO = $(addsuffix .cmo, $(COQPMODULES)) COQPCMX = $(addsuffix .cmx, $(COQPMODULES)) COQPTREES = engine interp intf kernel lib library ltac parsing pretyping printing proofs tactics toplevel vernac plugins/ltac COQPINCLUDES = -I src/coq-tactic -I $(COQCAMLPLIB) $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@ $(COQPDEP): DEPFLAGS += -I src/coq-tactic $(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES) $(COQPCMO) $(COQPCMX): BFLAGS += -rectypes $(COQPCMX): OFLAGS += -rectypes $(COQPDEP): $(COQPGENERATED) byte: lib/coq-tactic/why3tac.cma opt: lib/coq-tactic/why3tac.cmxs lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmxa, @ZIPLIB@) lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmx, @MENHIRLIB@) lib/coq-tactic/why3tac.cma: BFLAGS += $(addsuffix .cma, @ZIPLIB@) lib/coq-tactic/why3tac.cma: BFLAGS += $(addsuffix .cmo, @MENHIRLIB@) lib/coq-tactic/why3tac.cmxs: lib/why3/why3.cmxa $(COQPCMX) lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO) src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4 $(SHOW) 'Camlp $<' $(HIDE)$(COQCAMLP) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@ COQRTAC = -R lib/coq-tactic Why3 -R lib/coq Why3 -I lib/coq-tactic ifeq "$(OCAMLBEST)" "opt" COQTACEXT = cmxs else COQTACEXT = cma COQRTAC += -byte endif lib/coq-tactic/Why3.vo: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.$(COQTACEXT) $(SHOW) 'Coqc $<' $(HIDE)WHY3CONFIG="" $(COQC) $(COQRTAC) $< all: lib/coq-tactic/Why3.vo # depend and clean targets ifneq "$(MAKECMDGOALS:clean%=clean)" "clean" -include $(COQPDEP) endif depend: $(COQPDEP) CLEANDIRS += src/coq-tactic CLEANLIBS += lib/coq-tactic/why3tac GENERATED += $(COQPGENERATED) clean:: rm -f lib/coq-tactic/*.vo lib/coq-tactic/*.glob install_no_local:: $(MKDIR_P) $(LIBDIR)/why3/coq-tactic $(INSTALL_DATA) lib/coq-tactic/* $(LIBDIR)/why3/coq-tactic endif #################### # Coq realizations #################### ifeq (@enable_coq_support@,yes) ifeq (@enable_coq_libs@,yes) COQVERSIONSPECIFIC= COQVERSIONSPECIFICTARGETS=$(addprefix lib/coq/, $(COQVERSIONSPECIFIC)) COQVERSIONSPECIFICSOURCES=$(addsuffix .@coq_compat_version@, $(COQVERSIONSPECIFICTARGETS)) $(COQVERSIONSPECIFICTARGETS): $(COQVERSIONSPECIFICSOURCES) for i in $(COQVERSIONSPECIFIC); do \ cp lib/coq/$$i.@coq_compat_version@ lib/coq/$$i ; \ done clean:: rm -f $(COQVERSIONSPECIFICTARGETS) COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power NumOf COQLIBS_INT_ALL_FILES = Exponentiation $(COQLIBS_INT_FILES) COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES)) COQLIBS_BOOL_FILES = Bool COQLIBS_BOOL = $(addprefix lib/coq/bool/, $(COQLIBS_BOOL_FILES)) ifeq (@enable_coq_fp_libs@,yes) COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt PowerReal Real RealInfix Square Trigonometry Truncate else COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt PowerReal Real RealInfix Square Trigonometry endif COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES)) COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES)) COQLIBS_SET_FILES = Set COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES)) COQLIBS_MAP_FILES = Map Const Occ MapPermut MapInjection COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES)) COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt NthNoOpt RevAppend Combine Distinct NumOcc Permut COQLIBS_LIST = $(addprefix lib/coq/list/, $(COQLIBS_LIST_FILES)) COQLIBS_OPTION_FILES = Option COQLIBS_OPTION = $(addprefix lib/coq/option/, $(COQLIBS_OPTION_FILES)) COQLIBS_SEQ_FILES = Seq COQLIBS_SEQ = $(addprefix lib/coq/seq/, $(COQLIBS_SEQ_FILES)) ifeq (@coq_compat_version@,COQ84) COQLIBS_BV_FILES = Pow2int else COQLIBS_BV_FILES = Pow2int BV_Gen endif COQLIBS_BV = $(addprefix lib/coq/bv/, $(COQLIBS_BV_FILES)) ifeq (@enable_coq_fp_libs@,yes) COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES) COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES)) COQLIBS_IEEEFLOAT_FILES = RoundingMode GenericFloat Float32 Float64 COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES)) endif COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_SEQ) $(COQLIBS_FP) $(COQLIBS_BV) $(COQLIBS_IEEEFLOAT) drivers/coq-realizations.aux: Makefile $(SHOW) 'Generate $@' $(HIDE)(echo "(* generated automatically at compilation time *)"; \ echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \ echo 'theory HighOrd meta "realized_theory" "HighOrd", "" end'; \ for f in $(COQLIBS_INT_FILES); do \ echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \ for f in $(COQLIBS_BOOL_FILES); do \ echo 'theory bool.'"$$f"' meta "realized_theory" "bool.'"$$f"'", "" end'; done; \ for f in $(COQLIBS_REAL_FILES); do \ echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \ for f in $(COQLIBS_NUMBER_FILES); do \ echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \ for f in $(COQLIBS_SET_FILES); do \ echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \ for f in $(COQLIBS_MAP_FILES); do \ echo 'theory map.'"$$f"' meta "realized_theory" "map.'"$$f"'", "" end'; done; \ for f in $(COQLIBS_LIST_FILES); do \ echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \ for f in $(COQLIBS_OPTION_FILES); do \ echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \ for f in $(COQLIBS_SEQ_FILES); do \ echo 'theory seq.'"$$f"' meta "realized_theory" "seq.'"$$f"'", "" end'; done; \ for f in $(COQLIBS_BV_FILES); do \ echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \ for f in $(COQLIBS_IEEEFLOAT_FILES); do \ echo 'theory ieee_float.'"$$f"' meta "realized_theory" "ieee_float.'"$$f"'", "" end'; done; \ for f in $(COQLIBS_FP_FILES); do \ echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \ ) > $@ install_no_local:: $(MKDIR_P) $(LIBDIR)/why3/coq $(INSTALL_DATA) lib/coq/BuiltIn.vo lib/coq/HighOrd.vo $(LIBDIR)/why3/coq/ $(MKDIR_P) $(LIBDIR)/why3/coq/int $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/ $(MKDIR_P) $(LIBDIR)/why3/coq/bool $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_BOOL)) $(LIBDIR)/why3/coq/bool/ $(MKDIR_P) $(LIBDIR)/why3/coq/real $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/ $(MKDIR_P) $(LIBDIR)/why3/coq/number $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_NUMBER)) $(LIBDIR)/why3/coq/number/ $(MKDIR_P) $(LIBDIR)/why3/coq/set $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_SET)) $(LIBDIR)/why3/coq/set/ $(MKDIR_P) $(LIBDIR)/why3/coq/map $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_MAP)) $(LIBDIR)/why3/coq/map/ $(MKDIR_P) $(LIBDIR)/why3/coq/list $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_LIST)) $(LIBDIR)/why3/coq/list/ $(MKDIR_P) $(LIBDIR)/why3/coq/option $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_OPTION)) $(LIBDIR)/why3/coq/option/ $(MKDIR_P) $(LIBDIR)/why3/coq/seq $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_SEQ)) $(LIBDIR)/why3/coq/seq/ $(MKDIR_P) $(LIBDIR)/why3/coq/bv $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_BV)) $(LIBDIR)/why3/coq/bv/ ifeq (@enable_coq_fp_libs@,yes) $(MKDIR_P) $(LIBDIR)/why3/coq/floating_point $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/ $(MKDIR_P) $(LIBDIR)/why3/coq/ieee_float $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_IEEEFLOAT)) $(LIBDIR)/why3/coq/ieee_float/ endif 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-seq update-coq-bv update-coq-ieee_float update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done update-coq-bool: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bool.why for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bool.$$f -o lib/coq/bool/; done update-coq-real: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/real.why for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done update-coq-number: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/number.why for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T number.$$f -o lib/coq/number/; done update-coq-set: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/set.why for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T set.$$f -o lib/coq/set/; done update-coq-map: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/map.why for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T map.$$f -o lib/coq/map/; done update-coq-list: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/list.why for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T list.$$f -o lib/coq/list/; done update-coq-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/option.why for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T option.$$f -o lib/coq/option/; done update-coq-seq: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/seq.why for f in $(COQLIBS_SEQ_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T seq.$$f -o lib/coq/seq/; done update-coq-bv: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bv.why for f in $(COQLIBS_BV_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bv.$$f -o lib/coq/bv/; done update-coq-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/ieee_float.why for f in $(COQLIBS_IEEEFLOAT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T ieee_float.$$f -o lib/coq/ieee_float/; done update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/floating_point.why for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done else drivers/coq-realizations.aux: Makefile $(SHOW) 'Generate $@' $(HIDE)echo "(* generated automatically at compilation time *)" > $@ COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd endif COQV = $(addsuffix .v, $(COQLIBS_FILES)) COQVO = $(addsuffix .vo, $(COQLIBS_FILES)) COQVD = $(addsuffix .vd, $(COQLIBS_FILES)) %.vo: %.v $(SHOW) 'Coqc $<' $(HIDE)$(COQC) -R lib/coq Why3 $< %.vd: %.v $(SHOW) 'Coqdep $<' $(HIDE)$(COQDEP) -R lib/coq Why3 $< $(TOTARGET) all: $(COQVO) ifneq "$(MAKECMDGOALS:clean%=clean)" "clean" ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq" -include $(COQVD) endif endif depend: $(COQVD) clean-coq: rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES)) clean:: clean-coq else drivers/coq-realizations.aux: Makefile $(SHOW) 'Generate $@' $(HIDE)echo "(* generated automatically at compilation time *)" > $@ endif all: drivers/coq-realizations.aux install_no_local:: $(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/ clean:: rm -f drivers/coq-realizations.aux #################### # PVS realizations #################### ifeq (@enable_pvs_libs@,yes) PVSLIBS_INT_FILES = Int Abs MinMax ComputerDivision EuclideanDivision PVSLIBS_INT = $(addprefix lib/pvs/int/, $(PVSLIBS_INT_FILES)) PVSLIBS_REAL_FILES = Abs FromInt MinMax Real Square ExpLog Trigonometry \ PowerInt # RealInfix PVSLIBS_REAL = $(addprefix lib/pvs/real/, $(PVSLIBS_REAL_FILES)) PVSLIBS_LIST_FILES = # Nth PVSLIBS_LIST = $(addprefix lib/pvs/int/, $(PVSLIBS_LIST_FILES)) PVSLIBS_NUMBER_FILES = # Divisibility Gcd Parity Prime PVSLIBS_NUMBER = $(addprefix lib/pvs/number/, $(PVSLIBS_NUMBER_FILES)) PVSLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double PVSLIBS_FP_ALL_FILES = $(PVSLIBS_FP_FILES) PVSLIBS_FP = $(addprefix lib/pvs/floating_point/, $(PVSLIBS_FP_ALL_FILES)) PVSLIBS_FILES = $(PVSLIBS_INT) $(PVSLIBS_REAL) $(PVSLIBS_LIST) \ $(PVSLIBS_NUMBER) $(PVSLIBS_FP) drivers/pvs-realizations.aux: Makefile $(SHOW) 'Generate $@' $(HIDE)(echo "(* generated automatically at compilation time *)"; \ for f in $(PVSLIBS_INT_FILES); do \ echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \ for f in $(PVSLIBS_REAL_FILES); do \ echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \ for f in $(PVSLIBS_LIST_FILES); do \ echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \ for f in $(PVSLIBS_NUMBER_FILES); do \ echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \ for f in $(PVSLIBS_FP_FILES); do \ echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \ ) > $@ install_no_local:: $(MKDIR_P) $(LIBDIR)/why3/pvs/int $(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_INT)) $(LIBDIR)/why3/pvs/int/ $(INSTALL_DATA) $(addsuffix .prf, $(PVSLIBS_INT)) $(LIBDIR)/why3/pvs/int/ $(MKDIR_P) $(LIBDIR)/why3/pvs/real $(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_REAL)) $(LIBDIR)/why3/pvs/real/ $(INSTALL_DATA) $(addsuffix .prf, $(PVSLIBS_REAL)) $(LIBDIR)/why3/pvs/real/ $(MKDIR_P) $(LIBDIR)/why3/pvs/floating_point/ $(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_FP)) $(LIBDIR)/why3/pvs/floating_point/ $(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/ update-pvs: bin/why3realize.@OCAMLBEST@ drivers/pvs-realizations.aux for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done for f in $(PVSLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T list.$$f -o lib/pvs/list/; done for f in $(PVSLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T number.$$f -o lib/pvs/number/; done for f in $(PVSLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T floating_point.$$f -o lib/pvs/floating_point/; done else drivers/pvs-realizations.aux: Makefile $(SHOW) 'Generate $@' $(HIDE)echo "(* generated automatically at compilation time *)" > $@ install_no_local:: $(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/ endif all: drivers/pvs-realizations.aux clean:: rm -f drivers/pvs-realizations.aux ####################### # Isabelle realizations ####################### ifeq (@enable_isabelle_libs@,yes) ISABELLEVERSIONSPECIFIC=ROOT why3.ML Why3_BV.thy Why3_Number.thy Why3_Real.thy Why3_Set.thy ISABELLEVERSIONSPECIFICTARGETS=$(addprefix lib/isabelle/, $(ISABELLEVERSIONSPECIFIC)) ISABELLEVERSIONSPECIFICSOURCES=$(addsuffix .@ISABELLEVERSION@, $(ISABELLEVERSIONSPECIFICTARGETS)) ISABELLEREALIZEDRV=drivers/isabelle@ISABELLEVERSION@-realize.drv $(ISABELLEVERSIONSPECIFICTARGETS): $(ISABELLEVERSIONSPECIFICSOURCES) for i in $(ISABELLEVERSIONSPECIFIC); do \ cp lib/isabelle/$$i.@ISABELLEVERSION@ lib/isabelle/$$i ; \ done clean:: rm -f $(ISABELLEVERSIONSPECIFICTARGETS) ISABELLELIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix lib/isabelle/int/, $(ISABELLELIBS_INT_FILES))) ISABELLELIBS_BOOL_FILES = Bool ISABELLELIBS_BOOL = $(addsuffix .xml, $(addprefix lib/isabelle/bool/, $(ISABELLELIBS_BOOL_FILES))) ISABELLELIBS_REAL_FILES = Real RealInfix Abs MinMax FromInt Truncate Square ExpLog Trigonometry PowerInt # not yet realized : PowerReal Hyperbolic Polar ISABELLELIBS_REAL = $(addsuffix .xml, $(addprefix lib/isabelle/real/, $(ISABELLELIBS_REAL_FILES))) ISABELLELIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime ISABELLELIBS_NUMBER = $(addsuffix .xml, $(addprefix lib/isabelle/number/, $(ISABELLELIBS_NUMBER_FILES))) ISABELLELIBS_SET_FILES = Set Fset ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix lib/isabelle/set/, $(ISABELLELIBS_SET_FILES))) ISABELLELIBS_MAP_FILES = Map Const Occ MapPermut MapInjection ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix lib/isabelle/map/, $(ISABELLELIBS_MAP_FILES))) ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt RevAppend Combine Distinct NumOcc Permut ISABELLELIBS_LIST = $(addsuffix .xml, $(addprefix lib/isabelle/list/, $(ISABELLELIBS_LIST_FILES))) ISABELLELIBS_BV_FILES = Pow2int BV8 BV16 BV32 BV64 BVConverter_32_64 BVConverter_16_64 BVConverter_8_64 BVConverter_16_32 BVConverter_8_32 BVConverter_8_16 ISABELLELIBS_BV = $(addsuffix .xml, $(addprefix lib/isabelle/bv/, $(ISABELLELIBS_BV_FILES))) drivers/isabelle-realizations.aux: Makefile $(SHOW) 'Generate $@' $(HIDE)(echo "(* generated automatically at compilation time *)"; \ echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \ for f in $(ISABELLELIBS_INT_FILES); do \ echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \ for f in $(ISABELLELIBS_BOOL_FILES); do \ echo 'theory bool.'"$$f"' meta "realized_theory" "bool.'"$$f"'", "" end'; done; \ for f in $(ISABELLELIBS_REAL_FILES); do \ echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \ for f in $(ISABELLELIBS_NUMBER_FILES); do \ echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \ for f in $(ISABELLELIBS_SET_FILES); do \ echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \ for f in $(ISABELLELIBS_MAP_FILES); do \ echo 'theory map.'"$$f"' meta "realized_theory" "map.'"$$f"'", "" end'; done; \ for f in $(ISABELLELIBS_LIST_FILES); do \ echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \ for f in $(ISABELLELIBS_OPTION_FILES); do \ echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \ for f in $(ISABELLELIBS_BV_FILES); do \ echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \ ) > $@ ifeq (@enable_local@,yes) ISABELLE_TARGET_DIR=`pwd`/lib/isabelle else ISABELLE_TARGET_DIR=$(LIBDIR)/why3/isabelle endif lib/isabelle/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV) ifneq (@enable_local@,yes) cp -r lib/isabelle "$(LIBDIR)/why3" endif @(if isabelle components -l | grep -q "$(ISABELLE_TARGET_DIR)$$"; then \ echo "Building the Why3 heap for Isabelle/HOL:"; \ isabelle build -bc Why3; \ touch $@; \ else \ echo "[Warning] Cannot pre-build the Isabelle heap because"; \ echo " the Isabelle component configuration does not contain"; \ echo " [$(ISABELLE_TARGET_DIR)]"; \ fi) install_no_local:: $(INSTALL_DATA) drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/ install_no_local:: lib/isabelle/last_build install_local:: lib/isabelle/last_build update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV) $(ISABELLELIBS_INT): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \ $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/int.why $(SHOW) "Generating Isabelle realization for int.$(notdir $(basename $@))" $(HIDE)mkdir -p lib/isabelle/int $(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o lib/isabelle/int/ $(ISABELLELIBS_BOOL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \ $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/bool.why $(SHOW) "Generating Isabelle realization for bool.$(notdir $(basename $@))" $(HIDE)mkdir -p lib/isabelle/bool $(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o lib/isabelle/bool/ $(ISABELLELIBS_REAL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \ $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/real.why $(SHOW) "Generating Isabelle realization for real.$(notdir $(basename $@))" $(HIDE)mkdir -p lib/isabelle/real $(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o lib/isabelle/real/ $(ISABELLELIBS_NUMBER): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \ $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/number.why $(SHOW) "Generating Isabelle realization for number.$(notdir $(basename $@))" $(HIDE)mkdir -p lib/isabelle/number $(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o lib/isabelle/number/ $(ISABELLELIBS_SET): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \ $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/set.why $(SHOW) "Generating Isabelle realization for set.$(notdir $(basename $@))" $(HIDE)mkdir -p lib/isabelle/set $(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o lib/isabelle/set/ $(ISABELLELIBS_MAP): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \ $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/map.why $(SHOW) "Generating Isabelle realization for map.$(notdir $(basename $@))" $(HIDE)mkdir -p lib/isabelle/map $(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o lib/isabelle/map/ $(ISABELLELIBS_LIST): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \ $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/list.why $(SHOW) "Generating Isabelle realization for list.$(notdir $(basename $@))" $(HIDE)mkdir -p lib/isabelle/list $(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o lib/isabelle/list/ $(ISABELLELIBS_OPTION): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \ $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/option.why $(SHOW) "Generating Isabelle realization for option.$(notdir $(basename $@))" $(HIDE)mkdir -p lib/isabelle/option $(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o lib/isabelle/option/ $(ISABELLELIBS_BV): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \ $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/bv.why $(SHOW) "Generating Isabelle realization for bv.$(notdir $(basename $@))" $(HIDE)mkdir -p lib/isabelle/bv $(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o lib/isabelle/bv/ # do not update isabelle realizations systematically # all: update-isabelle clean:: rm -f lib/isabelle/*/*.xml else drivers/isabelle-realizations.aux: Makefile $(SHOW) 'Generate $@' $(HIDE)echo "(* generated automatically at compilation time *)" > $@ install_no_local:: $(INSTALL_DATA) drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/ endif all: drivers/isabelle-realizations.aux clean:: rm -f drivers/isabelle-realizations.aux ####################### # Ocaml realizations ####################### OCAMLLIBS_FILES = why3__BigInt_compat why3__BigInt why3__IntAux why3__Array \ why3__Matrix OCAMLLIBS_MODULES := $(addprefix lib/ocaml/, $(OCAMLLIBS_FILES)) OCAMLLIBS_DEP = $(addsuffix .dep, $(OCAMLLIBS_MODULES)) OCAMLLIBS_CMO = $(addsuffix .cmo, $(OCAMLLIBS_MODULES)) OCAMLLIBS_CMX = $(addsuffix .cmx, $(OCAMLLIBS_MODULES)) $(OCAMLLIBS_DEP): DEPFLAGS += -I src/util -I lib/ocaml @BIGINTINCLUDE@ $(OCAMLLIBS_CMO) $(OCAMLLIBS_CMX): INCLUDES += -I src/util -I lib/ocaml @BIGINTINCLUDE@ $(OCAMLLIBS_CMX): OFLAGS += -for-pack Why3extract byte: $(OCAMLLIBS_CMO) opt: $(OCAMLLIBS_CMX) byte: lib/why3/why3extract.cma opt: lib/why3/why3extract.cmxa lib/why3/why3extract.cma: lib/why3/why3extract.cmo lib/why3/why3extract.cmxa: lib/why3/why3extract.cmx lib/why3/why3extract.cmo: $(OCAMLLIBS_CMO) $(SHOW) 'Linking $@' $(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^ lib/why3/why3extract.cmx: $(OCAMLLIBS_CMX) lib/why3/why3extract.cmo $(SHOW) 'Linking $@' $(HIDE)$(OCAMLOPT) $(OFLAGS) $(CMIHACK) -pack -o $@ $(filter %.cmx, $^) install_no_local_lib:: $(MKDIR_P) $(OCAMLINSTALLLIB)/why3 $(INSTALL_DATA) $(wildcard $(addprefix lib/why3/why3extract., $(INSTALLED_LIB_EXTS))) \ $(OCAMLINSTALLLIB)/why3 ifneq "$(MAKECMDGOALS:clean%=clean)" "clean" -include $(OCAMLLIBS_DEP) endif $(OCAMLLIBS_DEP): lib/ocaml/why3__BigInt_compat.ml depend: $(OCAMLLIBS_DEP) CLEANDIRS += lib/ocaml CLEANLIBS += lib/why3/why3extract ################ # Jessie3 plugin ################ ifeq (@enable_frama_c@,yes) nobyte: jessie.byte noopt: jessie.opt jessie.byte: src/jessie/Makefile lib/why3/why3.cma @$(MAKE) -C src/jessie Jessie3.cma jessie.opt: src/jessie/Makefile lib/why3/why3.cmxa @$(MAKE) -C src/jessie Jessie3.cmxs install_no_local:: $(MKDIR_P) $(FRAMAC_LIBDIR)/plugins/ $(INSTALL_DATA) $(wildcard $(addprefix src/jessie/Jessie3., $(INSTALLED_LIB_EXTS))) \ $(FRAMAC_LIBDIR)/plugins/ clean:: $(MAKE) -C src/jessie clean endif ######### # why3doc ######### WHY3DOCGENERATED = src/why3doc/doc_lexer.ml WHY3DOC_FILES = doc_html doc_def doc_lexer doc_main WHY3DOCMODULES = $(addprefix src/why3doc/, $(WHY3DOC_FILES)) WHY3DOCDEP = $(addsuffix .dep, $(WHY3DOCMODULES)) WHY3DOCCMO = $(addsuffix .cmo, $(WHY3DOCMODULES)) WHY3DOCCMX = $(addsuffix .cmx, $(WHY3DOCMODULES)) $(WHY3DOCDEP): DEPFLAGS += -I src/why3doc $(WHY3DOCCMO) $(WHY3DOCCMX): INCLUDES += -I src/why3doc $(WHY3DOCDEP): $(WHY3DOCGENERATED) # build targets byte: bin/why3doc.byte opt: bin/why3doc.opt bin/why3doc.opt: lib/why3/why3.cmxa $(WHY3DOCCMX) $(SHOW) 'Linking $@' $(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^ bin/why3doc.byte: lib/why3/why3.cma $(WHY3DOCCMO) $(SHOW) 'Linking $@' $(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^ # depend and clean targets ifneq "$(MAKECMDGOALS:clean%=clean)" "clean" -include $(WHY3DOCDEP) endif depend: $(WHY3DOCDEP) CLEANDIRS += src/why3doc GENERATED += $(WHY3DOCGENERATED) clean_old_install:: rm -f $(BINDIR)/why3doc$(EXE) install_no_local:: $(INSTALL) bin/why3doc.@OCAMLBEST@ $(TOOLDIR)/why3doc$(EXE) install_local:: bin/why3doc ######### # trywhy3 ######### ifeq ($(DEBUGJS),yes) JSOO_DEBUG=--pretty --debug-info --source-map JS_MAPS=alt_ergo_worker.map trywhy3.map why3_worker.map else JSOO_DEBUG= JS_MAPS= endif ALTERGODIR=src/trywhy3/alt-ergo JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -g -package js_of_ocaml.syntax \ -package ocplib-simplex -syntax camlp4o -I src/trywhy3 \ -I $(ALTERGODIR)/src/util \ -I $(ALTERGODIR)/src/structures \ -I $(ALTERGODIR)/src/parsing \ -I $(ALTERGODIR)/src/preprocess \ -I $(ALTERGODIR)/src/theories \ -I $(ALTERGODIR)/src/instances \ -I $(ALTERGODIR)/src/sat \ -I $(ALTERGODIR)/src/main ALTERGOMODS=util/config util/version util/emap util/myUnix util/myDynlink \ util/myZip util/util util/lists util/numsNumbers util/numbers \ util/timers util/options util/gc_debug util/loc util/hashcons \ util/hstring \ structures/exception structures/symbols structures/ty \ structures/parsed structures/typed structures/term structures/literal \ structures/formula structures/explanation structures/errors \ util/profiling_default util/profiling \ parsing/why_parser parsing/why_lexer \ preprocess/existantial preprocess/triggers preprocess/why_typing \ preprocess/cnf \ instances/matching instances/instances \ theories/polynome theories/ac theories/uf theories/use \ theories/intervals theories/inequalities theories/intervalCalculus \ theories/arith theories/records theories/bitv theories/arrays \ theories/sum theories/combine theories/ccx theories/theory \ sat/sat_solvers \ main/frontend ALTERGOCMO=$(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS))) TRYWHY3CMO=lib/why3/why3.cma TRYWHY3FILES=trywhy3.js trywhy3.html trywhy3.css \ README examples/ \ trywhy3_custom.css gen_index.sh fontawesome/css/font-awesome.min.css \ fontawesome/fonts/FontAwesome.otf fontawesome/fonts/fontawesome-webfont.svg \ fontawesome/fonts/fontawesome-webfont.woff fontawesome/fonts/fontawesome-webfont.eot \ fontawesome/fonts/fontawesome-webfont.ttf fontawesome/fonts/fontawesome-webfont.woff2 \ ace-builds/src-min-noconflict/ace.js ace-builds/src-min-noconflict/mode-why3.js \ ace-builds/src-min-noconflict/theme-chrome.js $(JS_MAPS) trywhy3_package: trywhy3 tar czf trywhy3.tar.gz -C src $(addprefix trywhy3/, $(TRYWHY3FILES)) trywhy3: src/trywhy3/trywhy3.js src/trywhy3/why3_worker.js src/trywhy3/alt_ergo_worker.js src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte src/trywhy3/why3_worker.js src/trywhy3/alt_ergo_worker.js src/trywhy3/examples/*.mlw js_of_ocaml --extern-fs $(JSOO_DEBUG) -I src/trywhy3 \ --file=why3_worker.js:/ \ --file=alt_ergo_worker.js:/ \ --file=examples/index.txt:/examples/index.txt \ `find src/trywhy3/examples \( -name "*.mlw" -o -name "*.why" \) -printf " --file=examples/%P:/examples/%P"` \ +weak.js +nat.js $< src/trywhy3/trywhy3.byte: src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo $(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^ src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte js_of_ocaml $(JSOO_DEBUG) --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \ --file=try_alt_ergo.drv:/ \ `find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/%p"` \ +weak.js +nat.js $< src/trywhy3/why3_worker.byte: $(TRYWHY3CMO) src/trywhy3/worker_proto.cmo src/trywhy3/why3_worker.cmo $(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^ src/trywhy3/alt_ergo_worker.js: src/trywhy3/alt_ergo_worker.byte js_of_ocaml $(JSOO_DEBUG) +weak.js +nat.js +dynlink.js +toplevel.js $< src/trywhy3/alt_ergo_worker.byte: $(ALTERGOCMO) src/trywhy3/worker_proto.cmo src/trywhy3/alt_ergo_worker.cmo $(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^ src/trywhy3/alt_ergo_worker.cmo: src/trywhy3/worker_proto.cmo src/trywhy3/why3_worker.cmo: src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo: src/trywhy3/worker_proto.cmo src/trywhy3/%.cmo: src/trywhy3/%.ml $(JSOCAMLC) $(BFLAGS) -c $< src/trywhy3/%.cmi: src/trywhy3/%.mli $(JSOCAMLC) $(BFLAGS) -c $< clean:: rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte src/trywhy3/trywhy3.cm* \ src/trywhy3/why3_worker.js src/trywhy3/why3_worker.byte src/trywhy3/why3_worker.cm* \ src/trywhy3/alt_ergo_worker.js src/trywhy3/alt_ergo_worker.byte src/trywhy3/alt_ergo_worker.cm* \ src/trywhy3/worker_proto.cm* trywhy3.tar.gz CLEANDIRS += src/trywhy3 ######## # bench ######## .PHONY: bench test bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \ share/Makefile.config bin/why3extract $(MAKE) test-api-logic.@OCAMLBEST@ $(MAKE) test-api-mlw-tree.@OCAMLBEST@ $(MAKE) test-api-mlw.@OCAMLBEST@ $(MAKE) test-session.@OCAMLBEST@ $(MAKE) test-ocaml-extraction # desactivé car requiert findlib # if test -d examples/runstrat ; then \ # $(MAKE) test-runstrat.@OCAMLBEST@ ; fi bash bench/bench ".@OCAMLBEST@" @if test "@enable_coq_tactic@" = "yes"; then \ echo "=== checking the Coq tactic ==="; \ $(MAKE) test-coq-tactic; fi ############### # test targets ############### test-api-logic.byte: examples/use_api/logic.ml lib/why3/why3.cma $(SHOW) 'Ocaml $<' $(HIDE)ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null \ || (rm -f test-api-logic.byte; printf "Test of Why3 API calls failed. Please fix it"; exit 2) @rm -f test-api-logic.byte; test-api-logic.opt: examples/use_api/logic.ml lib/why3/why3.cmxa $(SHOW) 'Ocamlopt $<' $(HIDE)($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \ && ./test-api-logic.opt > /dev/null) \ || (rm -f test-api-logic.opt; printf "Test of Why3 API calls failed. Please fix it"; exit 2) @rm -f test-api-logic.opt test-api-mlw-tree.byte: examples/use_api/mlw_tree.ml lib/why3/why3.cma $(SHOW) 'Ocaml $<' $(HIDE)ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null\ || (rm -f test-api-mlw-tree.byte; printf "Test of Why3 API calls failed. Please fix it"; exit 2) @rm -f test-api-mlw-tree.byte; test-api-mlw-tree.opt: examples/use_api/mlw_tree.ml lib/why3/why3.cmxa $(SHOW) 'Ocamlopt $<' $(HIDE)($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \ && ./test-api-mlw-tree.opt > /dev/null) \ || (rm -f test-api-mlw-tree.opt; printf "Test of Why3 API calls failed. Please fix it"; exit 2) @rm -f test-api-mlw-tree.opt test-api-mlw.byte: examples/use_api/mlw.ml lib/why3/why3.cma $(SHOW) 'Ocaml $<' $(HIDE)ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< \ || (rm -f test-api-mlw.byte; printf "Test of Why3 API calls failed. Please fix it"; exit 2) @rm -f test-api-mlw.byte; test-api-mlw.opt: examples/use_api/mlw.ml lib/why3/why3.cmxa $(SHOW) 'Ocamlopt $<' $(HIDE)($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \ && ./test-api-mlw.opt > /dev/null) \ || (rm -f test-api-mlw.opt; printf "Test of Why3 API calls failed. Please fix it"; exit 2) @rm -f test-api-mlw.opt #test-shape: lib/why3/why3.cma # ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) $? examples/test_shape.ml test-session.byte: examples/use_api/create_session.ml lib/why3/why3.cma $(SHOW) 'Ocaml $<' $(HIDE)ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null\ || (rm -f why3session.xml why3shapes why3shapes.gz; \ printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2) @rm -f why3session.xml why3shapes why3shapes.gz test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa $(SHOW) 'Ocamlopt $<' $(HIDE)($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \ && ./test-session.opt > /dev/null) \ || (rm -f test-session.opt why3session.xml why3shapes why3shapes.gz; \ printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2) @rm -f test-session.opt why3session.xml why3shapes why3shapes.gz test-coq-tactic: lib/coq-tactic/Why3.vo $(COQC) $(COQRTAC) bench/coq-tactic/test.v #only test the compilation of runstrat test-runstrat.byte: lib/why3/why3.cma lib/why3/META OCAMLPATH=$(PWD)/lib $(MAKE) -C examples/use_api/runstrat clean OCAMLPATH=$(PWD)/lib $(MAKE) -C examples/use_api/runstrat byte test-runstrat.opt: lib/why3/why3.cmxa lib/why3/META OCAMLPATH=$(PWD)/lib $(MAKE) -C examples/use_api/runstrat clean OCAMLPATH=$(PWD)/lib $(MAKE) -C examples/use_api/runstrat opt test-runstrat: test-runstrat.@OCAMLBEST@ test-ocaml-extraction: bin/why3.opt bin/why3extract.opt lib/why3/why3extract.cmxa @echo "driver ocaml32" @mkdir -p tests/test-extraction @cd tests ; ../bin/why3extract.opt -D ocaml32 \ test_extraction.mlw -o test-extraction @cd tests/test-extraction/ ; \ $(OCAMLOPT) @BIGINTINCLUDE@ -I ../../lib/why3 \ @BIGINTLIB@.cmxa why3extract.cmxa \ ref__Refint.ml test_extraction__TestExtraction.ml main.ml @tests/test-extraction/a.out @echo "driver ocaml64" @cd tests ; ../bin/why3extract.opt -D ocaml64 \ test_extraction.mlw -o test-extraction @cd tests/test-extraction/ ; \ $(OCAMLOPT) @BIGINTINCLUDE@ -I ../../lib/why3 \ @BIGINTLIB@.cmxa why3extract.cmxa \ ref__Refint.ml test_extraction__TestExtraction.ml main.ml @tests/test-extraction/a.out ################ # documentation ################ .PHONY: doc ifeq (@enable_doc@,yes) doc: doc/manual.pdf doc/html/index.html BNF = qualid label constant operator term type formula theory theory2 \ why_file spec expr expr2 module whyml_file term_old_at BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF))) doc/%_bnf.tex: doc/%.bnf doc/bnf$(EXE) doc/bnf$(EXE) $< > $@ doc/bnf$(EXE): doc/bnf.mll $(OCAMLLEX) $< $(OCAMLC) -o $@ doc/bnf.ml DOC = api glossary ide intro exec macros manpages install \ manual starting syntax syntaxref technical version whyml \ itp pvs coq coq_tactic isabelle DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC))) doc/manual.pdf: $(BNFTEX) $(DOCTEX) doc/manual.bib share/provers-detection-data.conf cd doc; $(RUBBER) --warn all --pdf manual.tex CLEANDIRS += doc GENERATED += doc/bnf.ml ifeq (@enable_html_doc@,yes) # the dependency on the pdf ensures the bbl was built doc/html/manual.html: doc/manual.pdf doc/fix.hva cd doc; rm -rf html; mkdir -p html cp doc/*.png doc/manual.bbl doc/html/ cd doc; $(HEVEA) -o html/manual.html -fix -O fix.hva makeidx.hva manual.tex doc/html/index.html: doc/html/manual.html cd doc; $(HACHA) -tocbis -o html/index.html html/manual.html else doc/html/index.html: endif clean:: rm -rf doc/bnf$(EXE) $(BNFTEX) doc/html doc/manual.image.out; \ cd doc; $(RUBBER) --pdf --clean manual.tex else doc: endif ########## # API DOC ########## .PHONY: apidoc apidot MODULESTODOC = \ util/util util/opt util/lists util/strings \ util/extmap util/extset util/exthtbl \ util/weakhtbl util/stdlib util/rc util/debug \ core/ident core/ty core/term core/decl core/theory \ core/env core/task \ driver/whyconf driver/call_provers driver/driver \ session/session session/session_tools session/session_scheduler \ whyml/mlw_ty whyml/mlw_expr whyml/mlw_decl whyml/mlw_module \ whyml/mlw_wp FILESTODOC = $(addsuffix .mli, $(addprefix src/, $(MODULESTODOC))) doc/apidoc: mkdir -p doc/apidoc apidoc: doc/apidoc $(FILESTODOC) $(OCAMLDOC) -d doc/apidoc -html -t "Why3 API documentation" \ -keep-code $(INCLUDES) $(LIBINCLUDES) -I lib/why3 $(FILESTODOC) # could we include also the dependency graph ? -- someone # At least we can give a way to create it -- francois apidot: doc/apidoc/dg.svg doc/apidoc/dg.png #The sed remove configuration for dot that gives bad result doc/apidoc/dg.dot: doc/apidoc $(FILESTODOC) $(OCAMLDOC) -o doc/apidoc/dg.dot.tmp -dot $(INCLUDES) \ $(LIBINCLUDES) -I lib/why3 $(FILESTODOC) sed -e "s/ \(size\|ratio\|rotate\|fontsize\).*$$//" doc/apidoc/dg.dot.tmp > doc/apidoc/dg.dot rm -f doc/apidoc/dg.dot.tmp doc/apidoc/dg.svg: doc/apidoc/dg.dot dot -T svg $< > $@ doc/apidoc/dg.png: doc/apidoc/dg.dot dot -T png $< > $@ # what is this ? api doc is in why3.lri.fr/api instead... # 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 lib/why3 $(FILESTODOC) clean:: rm -f doc/apidoc/* ########## # Install rules that require root, and thus appear last in the file! ########## clean_old_install:: if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then rm -f /etc/bash_completion.d/why3; fi install_no_local:: if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then \ $(INSTALL_DATA) share/bash/why3 /etc/bash_completion.d; \ fi ########## # Stdlib formatted with why3doc ########## .PHONY: stdlibdoc STDLIBS = algebra \ bag \ bintree \ bool \ bv \ floating_point \ graph \ int \ ieee_float \ list \ map \ number \ option \ pigeon \ real \ relations \ seq \ set \ sum # function ? tptp ? STDMODS = array \ hashtbl \ impset \ matrix \ pqueue \ queue \ random \ ref \ stack \ string STDMACS = array int STDLIBFILES = $(addsuffix .why, $(addprefix theories/, $(STDLIBS))) STDMODFILES = $(addsuffix .mlw, $(addprefix modules/, $(STDMODS))) STDMACFILES = $(addsuffix .mlw, $(addprefix modules/mach/, $(STDMACS))) stdlibdoc: $(STDLIBFILES) $(STDMODFILES) bin/why3doc.@OCAMLBEST@ mkdir -p doc/stdlibdoc rm -f doc/stdlibdoc/style.css WHY3CONFIG="" bin/why3doc.@OCAMLBEST@ -L theories -L modules \ -o doc/stdlibdoc --title "Why3 Standard Library" \ $(STDLIBFILES) $(STDMODFILES) $(STDMACFILES) cd doc/stdlibdoc; \ for f in theories.*.html; \ do mv "$$f" "$${f#theories.}"; done; \ for f in modules.*.html; \ do mv "$$f" "$${f#modules.}"; done sed -i -e "s#theories.##g" -e "s#modules.##g" doc/stdlibdoc/index.html clean:: rm -f doc/stdlibdoc/* ################ # generic rules ################ %.cmi: %.mli $(SHOW) 'Ocamlc $<' $(HIDE)$(OCAMLC) -c $(BFLAGS) $< # suppress "unused rec" warning for Menhir-produced files %.cmo: %.ml %.mly $(SHOW) 'Ocamlc $<' $(HIDE)$(OCAMLC) -c $(BFLAGS) -w -39 $< # suppress "unused rec" warning for Menhir-produced files %.cmx: %.ml %.mly $(SHOW) 'Ocamlopt $<' $(HIDE)$(OCAMLOPT) -c $(OFLAGS) -w -39 $(CMIHACK) $< %.cmo: %.ml $(SHOW) 'Ocamlc $<' $(HIDE)$(OCAMLC) -c $(BFLAGS) $< %.cmx: %.ml %.mli $(SHOW) 'Ocamlopt $<' $(HIDE)$(OCAMLOPT) -c $(OFLAGS) $< # the generic rule cannot be applied since ocaml would confuse # lib/why3/why3extract.cmi for the interface (!!!) # same for ocaml/lablgtk2/gMain.cmi on case-insensitive filesystems src/tools/why3extract.cmx src/ide/gmain.cmx: %.cmx: %.ml $(SHOW) 'Ocamlopt $<' $(HIDE)$(OCAMLOPT) -c $(OFLAGS) $< %.cmx: %.ml $(SHOW) 'Ocamlopt $<' $(HIDE)$(OCAMLOPT) -c $(OFLAGS) $(CMIHACK) $< %.cma: $(SHOW) 'Linking $@' $(HIDE)$(OCAMLC) -a $(BFLAGS) -o $@ $^ %.cmxa: $(SHOW) 'Linking $@' $(HIDE)$(OCAMLOPT) -a $(OFLAGS) -o $@ $^ %.cmxs: $(SHOW) 'Linking $@' $(HIDE)$(OCAMLOPT) -shared $(OFLAGS) -o $@ $^ %.ml: %.mll $(SHOW) 'Ocamllex $<' $(HIDE)$(OCAMLLEX) $< %.ml %.mli: %.mly $(SHOW) 'Menhir $<' $(HIDE)$(MENHIR) --explain --strict $< %.dep: %.ml %.mli $(SHOW) 'Ocamldep $<' $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< $ $@ # 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-ocaml=/let[ \t]+\([^ \t]+\)/\1/" \ "--regex-ocaml=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ "--regex-ocaml=/and[ \t]+\([^ \t]+\)/\1/" \ "--regex-ocaml=/type[ \t]+\([^ \t]+\)/\1/" \ "--regex-ocaml=/exception[ \t]+\([^ \t]+\)/\1/" \ "--regex-ocaml=/val[ \t]+\([^ \t]+\)/\1/" \ "--regex-ocaml=/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@ # see .gitattributes for the list of files that are not distributed MORE_DIST = configure install-sh doc/manual.pdf dist: $(MORE_DIST) rm -rf distrib/$(NAME)/ distrib/$(NAME).tar.gz mkdir -p distrib/ git archive --format tar --prefix $(NAME)/ HEAD | tar x -C distrib/ for f in $(MORE_DIST); do cp $$f distrib/$(NAME)/$$f; done cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar ############### # file headers ############### headers: headache -c misc/headache_config.txt -h misc/header.txt \ Makefile.in configure.in \ src/*/*.ml src/*/*.ml[iyl4] \ plugins/*/*.ml plugins/*/*.ml[ily] \ lib/coq-tactic/*.v lib/coq/*.v lib/coq/*/*.v \ src/server/*.c src/server/*.h \ src/ide/resetgc.c \ examples/use_api/*.ml ######### # myself ######### Makefile: Makefile.in config.status ./config.status chmod --file $@ src/jessie/Makefile: src/jessie/Makefile.in config.status ./config.status chmod --file $@ src/config.sh: src/config.sh.in config.status ./config.status chmod --file $@ .merlin: .merlin.in config.status ./config.status chmod --file $@ src/util/config.ml share/Makefile.config: src/config.sh $(SHOW) 'Generate $@' $(HIDE)BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh clean:: rm -f share/Makefile.config doc/version.tex: doc/version.tex.in config.status ./config.status chmod --file $@ config.status: configure ./config.status --recheck all: lib/why3/META .merlin lib/why3/META: lib/why3/META.in config.status ./config.status chmod --file $@ configure: configure.in Version autoconf -f ################### # clean and depend ################### .PHONY: distclean distclean: clean rm -f config.status config.cache config.log .merlin \ Makefile src/util/config.ml doc/version.tex \ src/jessie/Makefile src/config.sh lib/why3/META depend: rm -f $^ $(MAKE) $^ clean:: rm -f $(GENERATED) $(foreach d,$(CLEANDIRS),rm -f $(addprefix $(d)/*.,$(COMPILED_LIB_EXTS));) $(foreach p,$(CLEANLIBS),rm -f $(addprefix $(p).,$(COMPILED_LIB_EXTS));) detect-unused: @L1=$$(mktemp); \ L2=$$(mktemp); \ for d in `find examples/ -name 'why3session.xml' -printf '%h\n'`; do \ sed -n -e 's/.*edited="\([^"]*\)".*/\1/p' $$d/why3session.xml | sort > $$L1; \ (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; \ diff -u --label="$$d/why3session.xml" --label="$$d/" $$L1 $$L2 || echo; \ done; \ rm $$L1 $$L2 ################################################################## # Building the Why3 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.