########################################################################## # # # Copyright (C) 2010- # # Francois Bobot # # Jean-Christophe Filliatre # # Johannes Kanig # # 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)@datadir@ 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@ #CAMLP4 = @CAMLP4O@ OCAMLVERSION = @OCAMLVERSION@ #PSVIEWER = @PSVIEWER@ #PDFVIEWER = @PDFVIEWER@ BFLAGS = -w Aelz -dtypes -g -I src $(INCLUDES) OFLAGS = -w Aelz -dtypes -I src $(INCLUDES) # external libraries common to all binaries ifeq (@enable_plugins@,yes) DYNLINK = dynlink else DYNLINK = endif EXTLIBS = str unix nums $(DYNLINK) EXTCMA = $(addsuffix .cma,$(EXTLIBS)) EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) ############### # main target ############### all: @OCAMLBEST@ .PHONY: byte opt clean depend all ############# # Why library ############# LIBGENERATED = src/userconf/rc.ml \ src/parser/parser.mli src/parser/parser.ml \ src/parser/parser.output src/parser/lexer.ml \ src/driver/driver_parser.mli src/driver/driver_parser.ml \ src/driver/driver_parser.output src/driver/driver_lexer.ml LIB_UTIL = pp loc prtree util hashcons sysutil hashweak LIB_CORE = ident ty term pattern decl theory task pretty trans env register LIB_PARSER = ptree parser lexer denv typing LIB_DRIVER = driver_ast call_provers driver_parser driver_lexer driver LIB_TRANSFORM = simplify_recursive_definition inlining \ split_conjunction encoding_decorate \ remove_logic_definition eliminate_inductive \ compile_match eliminate_algebraic \ eliminate_let eliminate_definition LIB_PRINTER = print_real alt_ergo why3 smt coq LIB_USERCONF = rc whyconf 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)) \ $(addprefix src/userconf/, $(LIB_USERCONF)) LIBDIRS = util core parser driver transform printer userconf LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS)) 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 $@ $^ src/why.cmi: src/why.cmo src/why.cmx @echo -n # depend target include .depend.lib .depend.lib: src/config.ml $(LIBGENERATED) $(OCAMLDEP) -slash $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@ depend: .depend.lib # clean target LIBSDIRS = src $(addprefix src/, $(LIBDIRS)) LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \ $(addsuffix /*.annot, $(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 ################## # Why binary ################## byte: bin/why.byte opt: bin/why.opt bin/why.opt: src/why.cmxa src/main.cmx $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^ $(STRIP) $@ bin/why.byte: src/why.cma src/main.cmo $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^ src/main.cmo src/main.cmx: src/why.cmi clean:: rm -f src/main.cm[iox] src/main.annot src/main.o rm -f bin/why.byte bin/why.opt ######## # Whyml ######## PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \ src/programs/pgm_parser.output src/programs/pgm_lexer.ml PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer 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 $(PGMCMO) $(PGMCMX): src/why.cmi # build targets byte: bin/whyml.byte opt: bin/whyml.opt bin/whyml.opt: src/why.cmxa $(PGMCMX) $(if $(QUIET), @echo 'Linking $@' &&) \ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^ $(STRIP) $@ bin/whyml.byte: src/why.cma $(PGMCMO) $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^ # depend and clean targets include .depend.programs .depend.programs: $(PGMGENERATED) $(OCAMLDEP) -slash -I src/programs $(PGMML) $(PGMMLI) > $@ depend: .depend.programs clean:: rm -f $(PGMGENERATED) rm -f src/programs/*.cm[iox] src/programs/*.o rm -f src/programs/*.annot src/programs/*~ rm -f bin/whyml.byte bin/whyml.opt ############### # proof manager ############### MNG_FILES = db test MNGMODULES = $(addprefix src/manager/, $(MNG_FILES)) MNGML = $(addsuffix .ml, $(MNGMODULES)) MNGMLI = $(addsuffix .mli, $(MNGMODULES)) MNGCMO = $(addsuffix .cmo, $(MNGMODULES)) MNGCMX = $(addsuffix .cmx, $(MNGMODULES)) $(MNGCMO) $(MNGCMX): INCLUDES = -I src/manager -I +sqlite3 $(MNGCMO) $(MNGCMX): src/why.cmi #byte: bin/manager.byte #opt: bin/manager.opt bin/manager.opt: src/why.cmxa $(MNGCMX) $(if $(QUIET), @echo 'Linking $@' &&) \ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) sqlite3.cma $^ $(STRIP) $@ bin/manager.byte: src/why.cma $(MNGCMO) $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) sqlite3.cma $^ # depend and clean targets include .depend.manager .depend.manager: $(OCAMLDEP) -slash -I src/manager/ $(MNGML) $(MNGMLI) > $@ depend: .depend.manager clean:: rm -f src/manager/*.cm[iox] src/manager/*.o rm -f src/manager/*.annot src/manager/*~ rm -f bin/manager.byte bin/manager.opt ##################### # graphical interface ##################### IDE_FILES = ide_main 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 -I +lablgtk2 -I +threads $(IDECMO) $(IDECMX): src/why.cmi # build targets ifeq (@enable_ide@,yes) byte: bin/whyide.byte opt: bin/whyide.opt endif bin/whyide.opt: src/why.cmxa $(IDE_CMX) $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \ lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^ $(STRIP) $@ bin/whyide.byte: src/why.cma $(IDE_CMO) $(if $(QUIET),@echo 'Linking $@' &&) \ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \ lablgtk.cma lablgtksourceview2.cma gtkThread.cmo $^ # depend and clean targets include .depend.ide .depend.ide: $(OCAMLDEP) -slash -I src/ide $(IDEML) $(IDEMLI) > $@ depend: .depend.ide clean:: rm -f src/ide/*.cm[iox] src/ide/*.o rm -f src/ide/*.annot src/ide/*~ rm -f bin/whyide.byte bin/whyide.opt ############## # Coq plugin ############## ifeq (@enable_coq_support@,yes) #byte: src/coq-plugin/whytac.cmo opt: src/coq-plugin/whytac.cmxs endif COQTREES = kernel lib interp parsing proofs pretyping tactics library #src/coq-plugin/whytac.cmo: INCLUDES = $(addprefix -I @COQLIB@/, $(COQTREES)) src/coq-plugin/whytac.cmxs: INCLUDES = $(addprefix -I @COQLIB@/, $(COQTREES)) #src/coq-plugin/whytac.cmo: BFLAGS+=-rectypes src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes src/coq-plugin/whytac.cmxs: src/why.cmxa src/coq-plugin/whytac.ml $(OCAMLOPT) $(OFLAGS) -o $@ -shared $^ ####### # tools ####### TOOLS = bin/why-cpulimit byte opt: $(TOOLS) bin/why-cpulimit: src/tools/@CPULIMIT@.c $(CC) -o $@ $^ clean:: rm -f bin/why-cpulimit src/tools/*~ ######## # bench ######## .PHONY: bench test bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ sh bench/bench \ "bin/why.@OCAMLBEST@ -I theories" \ "bin/whyml.@OCAMLBEST@ -I theories" BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO)) BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs) bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS) bin/why.byte -D bench/plugins/helloworld.drv -I theories/ \ src/test.why -t Test -g G bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv -I theories/ \ src/test.why -t Test -g G bin/why.$(OCAMLBEST) -D bench/plugins/simplify_array.drv -I theories/ \ src/test.why -t Test_simplify_array -g G ############### # test targets ############### test: bin/why.byte $(TOOLS) mkdir -p output_why3 ocamlrun -bt bin/why.byte -I theories/ -D drivers/why3.drv \ -o output_why3 src/test.why bin/why.byte -D drivers/alt_ergo.drv -I theories/ \ src/test.why -t Test -g G bin/why.byte -D drivers/alt_ergo.drv -I theories/ \ --timeout 3 --prove src/test.why -t Test -g G bin/why.byte -D drivers/coq.drv -I theories/ \ src/test.why -t Test -g G echo bin/why.byte -D drivers/alt_ergo.drv -I theories/ \ --timeout 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 array.TestBv32 \ ; do \ printf "Generating Coq file for $$i\\n" && bin/why.byte \ -D drivers/coq.drv -I theories/ \ -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/whyml.byte ocamlrun -bt bin/whyml.byte -I theories/ src/programs/test.mlw examples/programs/%: bin/whyml.byte bin/whyml.byte -I theories examples/programs/$*.mlw ############### # installation ############### ## install: install-binary install-lib install-man ## ## BINARYFILES = $(BINARY) bin/why-ide.$(OCAMLBEST) ## ## # install-binary should not depend on $(BINARYFILES); otherwise it ## # enforces the compilation of why-ide, even when lablgtk2 is not installed ## install-binary: ## mkdir -p $(BINDIR) ## cp -f $(BINARY) $(BINDIR)/why$(EXE) ## if test -f bin/why-ide.$(OCAMLBEST); then \ ## cp -f bin/why-ide.$(OCAMLBEST) $(BINDIR)/why-ide-bin$(EXE); \ ## fi ## ## install-lib: ## mkdir -p $(LIBDIR)/why/why ## ## install-man: ## mkdir -p $(MANDIR)/man1 ## cp -f doc/*.1 $(MANDIR)/man1 ## ## install-coq-no: ## install-coq-yes: install-coq-@COQVER@ ## install-coq-v7: ## mkdir -p $(LIBDIR)/why/coq7 ## cp -f $(V7FILES) $(LIBDIR)/why/coq7 ## cp -f $(VO7) $(LIBDIR)/why/coq7 ## install-coq-v8 install-coq-v8.1: ## if test -w $(COQLIB) ; then \ ## mkdir -p $(COQLIB)/user-contrib ; \ ## cp -f $(V8FILES) $(COQLIB)/user-contrib ; \ ## cp -f $(VO8) $(COQLIB)/user-contrib ; \ ## else \ ## echo "Cannot copy to Coq standard library. Add $(LIBDIR)/why/coq to Coq include path." ;\ ## mkdir -p $(LIBDIR)/why/coq ;\ ## cp -f $(VO8) $(V8FILES) $(LIBDIR)/why/coq ;\ ## fi ## ## install-pvs-no: ## install-pvs-yes: $(PVSFILES) ## mkdir -p $(PVSLIB)/why ## cp $(PVSFILES) $(PVSFILES:.pvs=.prf) $(PVSLIB)/why ## cp lib/pvs/top.pvs lib/pvs/pvscontext.el $(PVSLIB)/why ## @echo "====== Compiling PVS theories, this may take some time ======" ## (cd $(PVSLIB)/why ; @PVSC@ -batch -l pvscontext.el -q -v 2 > top.out) ## @echo "====== Done compiling PVS theories ======" ## ## install-mizar-no: ## install-mizar-yes: ## mkdir -p @MIZARLIB@/mml/dict ## cp lib/mizar/why.miz @MIZARLIB@/mml ## cp lib/mizar/dict/why.voc @MIZARLIB@/mml/dict ## ## local-install: $(BINARY) $(WHYCONFIG) $(JESSIE) bin/why-ide.$(OCAMLBEST) byte bin/why-ide.byte ## cp $(BINARY) $$HOME/bin/why ## cp $(WHYCONFIG) $$HOME/bin/why ## cp $(JESSIE) $$HOME/bin/jessie ## if test -f bin/why-ide.$(OCAMLBEST); then \ ## cp -f bin/why-ide.$(OCAMLBEST) $$HOME/bin/why-ide; \ ## fi ## ## local: install ## ## win: why.nsi ## "/cygdrive/c/Program Files (x86)/NSIS/makensis" /DVERSION=$(VERSION) why.nsi ## ## zip: ## zip -A -r why-$(VERSION).zip c:/why/bin c:/why/lib c:/coq/lib/contrib/why c:/coq/lib/contrib7/why ################ # documentation ################ DOC = doc/manual.pdf doc/manual.html doc: $(DOC) doc/manual.pdf: doc/manual.tex doc/version.tex make -C doc manual.pdf doc/manual.html: doc/manual.tex doc/version.tex make -C doc manual.html clean:: make -C doc clean ########## # API DOC ########## .PHONY: apidoc apidoc: mkdir -p apidoc $(OCAMLDOC) -d apidoc -html -I src $(LIBINCLUDES) -I +sqlite3 \ $(LIBML) $(LIBMLI) $(MNGML) $(MNGMLI) clean:: rm -f apidoc/* ################ # generic rules ################ %.cmi: %.mli $(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) $< %.cmo %cmi: %.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 %.output: %.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: otags src/*.mli src/*.ml c/*.mli c/*.ml intf/*.mli intf/*.ml wc: ocamlwc -p src/*.ml* src/*/*.ml* dep: $(MAKE) depend cat .depend* | ocamldot | dot -Tpdf > dep.pdf # $(PDFVIEWER) dep.pdf # distrib ######### # NAME=why-$(VERSION) # EXPORT=export/$(NAME) # # WWW = /users/www-perso/projets/why # FTP = $(WWW)/download # WWWKRAKATOA = /users/www-perso/projets/krakatoa # # FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/why-ide.sh \ # mix/*.ml* \ # version.sh Version Makefile.in configure.in configure .depend .depend.coq \ # config/check_ocamlgraph.ml \ # README INSTALL COPYING LICENSE CHANGES \ # doc/Makefile doc/manual.ps doc/why.1 \ # examples-c/*/*.h examples-c/*/*.c \ # examples-c/Makefile examples-c/*/Makefile \ # examples-c/*/coq/*.v \ # examples/Makefile* \ # examples/*/*.mlw examples/*/*.why examples/*/*.v examples/*/*.sx \ # examples/*/.depend examples/*/Makefile \ # bench/bench.in bench/good*/*.mlw bench/good*/*.v \ # bench/c/bench bench/c/bench-files bench/c/*/*.c bench/c/*/*/*.c \ # bench/jc/bench bench/jc/good/*.jc \ # bench/java/bench bench/java/*/*.java bench/provers/*.mlw \ # tests/regtest.sh tests/java/*.java \ # tests/java/coq/*.v \ # tests/java/result/README tests/java/oracle/*.oracle \ # lib/coq*/*.v \ # lib/pvs/pvscontext.el lib/pvs/*.pvs lib/pvs/*.prf \ # lib/mizar/why.miz lib/mizar/dict/why.voc \ # lib/why/*.why lib/isabelle/*.thy lib/hol4/*.ml lib/harvey/*.rv \ # lib/java_api/java/*/*.java \ # lib/javacard_api/java/lang/*.java \ # lib/javacard_api/javacard/*/*.java \ # lib/javacard_api/javacardx/crypto/*.java \ # lib/javacard_api/com/sun/javacard/impl/*.java \ # lib/images/*.png \ # atp/*.ml atp/LICENSE.txt atp/Makefile atp/Mk_ml_file \ # ocamlgraph/configure.in ocamlgraph/configure ocamlgraph/.depend \ # ocamlgraph/Makefile.in ocamlgraph/META.in ocamlgraph/*/*.ml* \ # frama-c-plugin/Makefile frama-c-plugin/configure \ # frama-c-plugin/*.ml* frama-c-plugin/share/jessie/*.h # # # ne pas distribuer ces tests-la frama-c-plugin/tests/jessie/*.c # # 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 # # source: export/$(NAME).tar.gz # cp CHANGES CHANGES.caduceus export/$(NAME).tar.gz $(FTP) # # export/$(NAME).tar.gz: $(FILES) # rm -rf $(EXPORT) # mkdir -p $(EXPORT)/bin # cp --parents $(FILES) $(EXPORT) # cd $(EXPORT); rm -f $(GENERATED) # cd export; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar # # tarball-for-framac: # make tarball # cp export/$(NAME).tar.gz export/why-for-framac.tar.gz # # 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 */*.ml */*/*.ml */*/*.ml[ily4] ######### # myself ######### Makefile: Makefile.in config.status ./config.status --file $@ src/config.ml: src/config.ml.in config.status ./config.status --file $@ doc/version.tex: doc/version.tex.in config.status ./config.status --file $@ config.status: configure Version ./config.status --recheck 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 ################################################################# # 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.