########################################################################## # # # 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. # # # ########################################################################## VERBOSEMAKE ?= @VERBOSEMAKE@ ifeq ($(VERBOSEMAKE),yes) QUIET = else QUIET = yes endif # where to install the binaries DESTDIR = prefix=@prefix@ datarootdir=@datarootdir@ exec_prefix=@exec_prefix@ BINDIR=$(DESTDIR)@bindir@ LIBDIR=$(DESTDIR)@libdir@ EXE=@EXE@ STRIP=@STRIP@ # where to install the man page MANDIR=$(DESTDIR)@mandir@ # other variables OCAMLC = @OCAMLC@ OCAMLOPT = @OCAMLOPT@ OCAMLDEP = @OCAMLDEP@ OCAMLLEX = @OCAMLLEX@ OCAMLYACC= @OCAMLYACC@ OCAMLDOC = @OCAMLDOC@ OCAMLLIB = @OCAMLLIB@ OCAMLBEST= @OCAMLBEST@ OCAMLVERSION = @OCAMLVERSION@ CAMLP4 = @CAMLP4O@ PSVIEWER = @PSVIEWER@ PDFVIEWER = @PDFVIEWER@ DYNLINK = @DYNLINK@ ifeq ($(DYNLINK),Dynlink) DYNLINKBFLAGS = dynlink.cma DYNLINKOFLAGS = dynlink.cmxa else DYNLINKBFLAGS = DYNLINKOFLAGS = endif INCLUDES = -I src/core -I src/util -I src/driver -I src/parser -I src/printer \ -I src/transform -I src/programs -I src BFLAGS = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cma unix.cma $(DYNLINKBFLAGS) # no -warn-error because some do not compile all files (e.g. those linked to APRON) OFLAGS = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cmxa unix.cmxa $(DYNLINKOFLAGS) COQC7 = @COQC7@ COQC8 = @COQC8@ COQDEP = @COQDEP@ COQLIB = "@COQLIB@" COQVER = @COQVER@ GENERATED = src/version.ml src/parser/parser.mli src/parser/parser.ml \ src/parser/lexer.ml src/driver/driver_lexer.ml \ src/driver/driver_parser.mli src/driver/driver_parser.ml \ src/programs/pgm_lexer.ml src/programs/pgm_parser.mli \ src/programs/pgm_parser.ml src/driver/dynlink_compat.ml # main targets ############## BINARY=bin/why.$(OCAMLBEST) BINARYL=bin/whyl.$(OCAMLBEST) TOOLS=bin/why-cpulimit all: .depend $(BINARY) $(BINARYL) $(TOOLS) # refrain parallel make (-j nn) from starting ocaml compilation too early *.cm*: .depend opt: bin/why.opt bin/whyl.opt byte: bin/why.byte bin/whyl.byte .PHONY: check PRELUDE=lib/why/prelude.why $(WHYLIBS) # sanity check: the prelude files do typecheck check: $(BINARY) $(PRELUDE) WHYLIB=lib $(BINARY) --no-pervasives -tc lib/why/prelude.why for f in $(WHYLIBS) ; do \ WHYLIB=lib $(BINARY) -tc $$f; \ done # version number ################ include Version doc/version.tex src/version.ml: Version version.sh config.status BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) COQVER=$(COQVER) ./version.sh # why ##### CORE_CMO := ident.cmo ty.cmo term.cmo pattern.cmo decl.cmo theory.cmo\ task.cmo pretty.cmo trans.cmo env.cmo register.cmo CORE_CMO := $(addprefix src/core/,$(CORE_CMO)) UTIL_CMO := pp.cmo loc.cmo prtree.cmo util.cmo hashcons.cmo \ sysutil.cmo hashweak.cmo UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO)) PARSER_CMO := parser.cmo lexer.cmo denv.cmo typing.cmo PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO)) TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\ split_conjunction.cmo encoding_decorate.cmo\ remove_logic_definition.cmo eliminate_inductive.cmo\ compile_match.cmo eliminate_algebraic.cmo\ eliminate_let.cmo eliminate_definition.cmo TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO)) DRIVER_CMO := call_provers.cmo dynlink_compat.cmo driver_parser.cmo\ driver_lexer.cmo driver.cmo DRIVER_CMO := $(addprefix src/driver/,$(DRIVER_CMO)) PRINTER_CMO := print_real.cmo alt_ergo.cmo why3.cmo smt.cmo coq.cmo PRINTER_CMO := $(addprefix src/printer/,$(PRINTER_CMO)) CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\ $(TRANSFORM_CMO) $(PRINTER_CMO) src/main.cmo CMX = $(CMO:.cmo=.cmx) bin/why.opt: $(CMX) echo $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(TRANSFORM_CMO) $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ nums.cmxa $^ $(STRIP) $@ bin/why.byte: $(CMO) $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) -o $@ nums.cma $^ bin/why.static: $(CMX) src/why.cmx $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) -cclib -static $(OFLAGS) -o $@ nums.cmxa $^ $(STRIP) $@ bin/top: $(CMO) ocamlmktop $(BFLAGS) -o $@ nums.cma $^ # test targets ############## test: bin/why.byte $(TOOLS) mkdir -p output_why3 ocamlrun -bt bin/why.byte -I theories/ --driver drivers/why3.drv \ --output-dir output_why3 --all-goals src/test.why bin/why.byte --driver drivers/alt_ergo.drv -I theories/ \ --output-file - --goal Test.G src/test.why --timeout 3 bin/why.byte --driver drivers/alt_ergo.drv -I theories/ \ --call --goal Test.G src/test.why --timeout 3 bin/why.byte --driver drivers/coq.drv -I theories/ \ --output-file tmp.v --goal Test.G src/test.why echo bin/why.byte --call --timeout 1 --driver drivers/alt_ergo.drv -I theories/ \ --all-goals theories/real.why @mkdir -p theories/coq @printf "*** Checking Coq file generation ***\\n" @for i in int.Abs int.EuclideanDivision int.ComputerDivision \ real.Abs real.FromIntTest real.ExpLog real.Trigonometric \ floating_point.Test array.TestBv32 \ ; do \ printf "Generate Coq file for $$i" && bin/why.byte \ --driver drivers/coq.drv -I theories/ \ --output-dir theories/coq --goals-of $$i ; done @printf "*** Checking Coq compilation ***\\n" @for i in theories/coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done testl: bin/whyl.byte ocamlrun -bt bin/whyl.byte -I theories/ src/programs/test.mlw examples/programs/%: bin/whyl.byte bin/whyl.byte -I theories examples/programs/$*.mlw # programs ########## PGM_CMO := pgm_parser.cmo pgm_lexer.cmo pgm_typing.cmo pgm_main.cmo PGM_CMO := $(addprefix src/programs/, $(PGM_CMO)) WHYL_CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\ $(TRANSFORM_CMO) $(PRINTER_CMO) $(PGM_CMO) WHYL_CMX = $(WHYL_CMO:.cmo=.cmx) bin/whyl.opt: $(WHYL_CMX) $(if $(QUIET), @echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ nums.cmxa $^ $(STRIP) $@ bin/whyl.byte: $(WHYL_CMO) $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) -o $@ nums.cma $^ #tools ###### bin/why-cpulimit: src/tools/@CPULIMIT@.c $(CC) -o $@ $^ # graphical interface ##################### GCMO = $(CMO) intf/colors.cmo intf/tags.cmo intf/tools.cmo intf/tagsplit.cmo\ intf/astprinter.cmo intf/astnprinter.cmo intf/astpprinter.cmo\ intf/model.cmo intf/cache.cmo intf/gConfig.cmo intf/hilight.cmo\ intf/whyhilight.cmo intf/pprinter.cmo intf/preferences.cmo intf/stat.cmo GCMX = $(GCMO:.cmo=.cmx) gwhy-yes: bin/gwhy.$(OCAMLBEST) gwhy-no: gwhy: bin/gwhy.$(OCAMLBEST) bin/gwhy.opt: $(GCMX) $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ unix.cmxa threads.cmxa nums.cmxa str.cmxa graph.cmxa lablgtk.cmxa gtkThread.cmx $^ $(STRIP) $@ bin/gwhy.static: $(GCMX) $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) -cclib -static $(OFLAGS) -o $@ unix.cmxa threads.cmxa nums.cmxa str.cmxa graph.cmxa lablgtk.cmxa gtkThread.cmx $^ $(STRIP) $@ bin/gwhy.byte: $(GCMO) $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) -o $@ unix.cma str.cma nums.cma graph.cma lablgtk.cma threads.cma gtkThread.cmo $^ # bench ####### .PHONY: bench test WHYVO=lib/coq/Why.vo bench/bench : bench/bench.in config.status ./config.status --file bench/bench bench:: $(BINARY) $(BINARYL) bench/bench $(TOOLS) sh bench/bench "$(BINARY) -I theories/" "$(BINARYL) -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) $(BINARY) byte \ $(TOOLS) bin/why.byte --driver bench/plugins/helloworld.drv -I theories/ \ --output-file - --goal Test.G src/test.why bin/why.$(OCAMLBEST) --driver bench/plugins/helloworld.drv -I theories/ \ --output-file - --goal Test.G src/test.why bin/why.$(OCAMLBEST) --driver bench/plugins/simplify_array.drv -I theories/ \ --output-file - --goal Test_simplify_array.G src/test.why # installation ############## install: install-binary install-lib install-man BINARYFILES = $(BINARY) bin/gwhy.$(OCAMLBEST) # install-binary should not depend on $(BINARYFILES); otherwise it # enforces the compilation of gwhy, even when lablgtk2 is not installed install-binary: mkdir -p $(BINDIR) cp -f $(BINARY) $(BINDIR)/why$(EXE) if test -f bin/gwhy.$(OCAMLBEST); then \ cp -f bin/gwhy.$(OCAMLBEST) $(BINDIR)/gwhy-bin$(EXE); \ fi install-lib: mkdir -p $(LIBDIR)/why/why # cp -f $(PRELUDE) $(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) $(CADUCEUS) $(JESSIE) bin/gwhy.$(OCAMLBEST) byte bin/gwhy.byte cp $(BINARY) $$HOME/bin/why cp $(WHYCONFIG) $$HOME/bin/why cp $(CADUCEUS) $$HOME/bin/caduceus cp $(JESSIE) $$HOME/bin/jessie if test -f bin/gwhy.$(OCAMLBEST); then \ cp -f bin/gwhy.$(OCAMLBEST) $$HOME/bin/gwhy; \ fi local: install # local: bin/why.opt $(CADUCEUS) $(WHY2HTML) $(DP) $(RVMERGE) coq-@COQ@ # cp -f bin/why.opt $$HOME/bin/$$OSTYPE/why # cp -f $(CADUCEUS) $$HOME/bin/$$OSTYPE/caduceus # cp -f $(WHY2HTML) $$HOME/bin/$$OSTYPE/why2html # cp -f $(DP) $$HOME/bin/$$OSTYPE/dp # cp -f $(RVMERGE) $$HOME/bin/$$OSTYPE/rv_merge # # mkdir -p $(COQLIB)/contrib7/why # # cp -f $(VO7) $(VFILES) $(COQLIB)/contrib7/why # # mkdir -p $(COQLIB)/contrib/why # # cp -f $(VO8) $(VFILES) $(COQLIB)/contrib/why # mkdir -p $(PVSLIB)/why # cp $(PVSFILES) $(PVSLIB)/why # mkdir -p $(MIZFILES)/mml/dict # cp lib/mizar/why.miz $(MIZFILES)/mml # cp lib/mizar/dict/why.voc $(MIZFILES)/mml/dict # mkdir -p $$HOME/man/man1 # cp -f doc/*.1 $$HOME/man/man1 demons: $(STATICBINARY) doc/manual.ps cp -f $(STATICBINARY) /users/demons/demons/bin/$$OSTYPE/why cp doc/manual.ps /users/demons/demons/docs/why.ps 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 # doc DOC=doc/manual.ps doc/manual.html doc/caduceus.ps doc/caduceus.html \ doc/krakatoa.pdf doc/krakatoa.html \ doc/main.pdf doc/main.html doc:: $(DOC) doc/manual.ps: doc/manual.tex doc/version.tex make -C doc manual.ps # doc/version.tex: Version Makefile.in # echo '\newcommand{\whyversion}'"{$(VERSION)}" > $@ # echo '\newcommand{\caduceusversion}'"{$(CVERSION)}" >> $@ # echo '\newcommand{\jessieversion}'"{$(JCVERSION)}" >> $@ # echo '\newcommand{\krakatoaversion}'"{$(KVERSION)}" >> $@ doc/manual.html: doc/manual.tex doc/version.tex make -C doc manual.html doc/caduceus.ps: doc/caduceus.tex doc/version.tex make -C doc caduceus.ps doc/caduceus.html: doc/caduceus.tex doc/version.tex make -C doc caduceus.html doc/krakatoa.pdf: doc/krakatoa.tex doc/version.tex make -C doc krakatoa.pdf doc/krakatoa.html: doc/krakatoa.tex doc/version.tex make -C doc krakatoa.html doc/main.pdf: doc/main.tex doc/version.tex make -C doc main.pdf doc/main.html: doc/main.tex doc/version.tex make -C doc main.html # API HTML DOC ############## OCAMLDOCSRC = intf/model.mli $(WHYCONFIGCMO:.cmo=.ml) $(WHYCONFIGCMI:.cmi=.mli) # $(JCCMO:.cmo=.ml) $(JCCMI:.cmi=.mli) apidoc: $(OCAMLDOCSRC) mkdir -p ocamldoc rm -f ocamldoc/* $(OCAMLDOC) -d ocamldoc -html $(INCLUDES) @INCLUDEGTK2@ $(OCAMLDOCSRC) # special rules ############### # CAMLP4=@CAMLP4O@ pa_extend.cmo pa_macro.cmo # src/%.cmo: src/%.ml4 # $(OCAMLC) -c $(BFLAGS) -pp "$(CAMLP4) -DOCAML@OCAMLV@ -impl" -impl $< # src/%.cmx: src/%.ml4 # $(OCAMLOPT) -c $(OFLAGS) -pp "$(CAMLP4) -DOCAML@OCAMLV@ -impl" -impl $< # src/%.ml: src/%.ml4 # $(CAMLP4) pr_o.cmo -DOCAML@OCAMLV@ -impl $< > $@ # generic rules ############### .SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .v .vo .ml4 .cmxs .mli.cmi: $(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) $(APRONLIB) $(ATPLIB) -c $(BFLAGS) $< .ml.cmi: $(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) $(APRONLIB) $(ATPLIB) -c $(BFLAGS) $< .ml.cmo: $(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) $(APRONLIB) $(ATPLIB) -c $(BFLAGS) $< .ml.o: $(OCAMLOPT) $(APRONLIB) $(ATPLIB) -c $(OFLAGS) $< .ml.cmx: $(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) $(APRONLIB) $(ATPLIB) -c $(OFLAGS) $< %.cmxs: %.ml %.cmx $(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(INCLUDES) -o $@ $< .mll.ml: $(OCAMLLEX) $< .mly.ml: $(OCAMLYACC) -v $< .mly.mli: $(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/gwhy.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 Makefile config.status: configure ./config.status --recheck configure: configure.in autoconf src/driver/dynlink_compat.ml: src/driver/dynlink_compat.ml.in config.status ./config.status --file src/driver/dynlink_compat.ml # clean and depend ################## clean:: rm -f src/*.cm[iox] src/*.o src/*~ src/*.annot src/*.output rm -f src/*/*.cm[iox] src/*/*.o src/*/*~ src/*/*.annot src/*/*.output rm -f c/*.cm[iox] c/*.o c/*~ c/*.annot c/*.output rm -f intf/*.cm[iox] intf/*.o intf/*~ intf/*.annot rm -f tools/*.cm[iox] tools/*.o tools/*~ tools/*.annot rm -f jc/*.cm[iox] jc/*.o jc/*~ jc/*.annot jc/*.output rm -f java/*.cm[iox] java/*.o java/*~ java/*.annot java/*.output rm -f ml/*.cm[iox] ml/*.o ml/*~ ml/*.annot rm -f ml/parsing/*.cm[iox] ml/parsing/*.o ml/parsing/*~ \ ml/parsing/*.annot ml/parsing/*.output rm -f ml/utils/*.cm[iox] ml/utils/*.o ml/utils/*~ ml/utils/*.annot rm -f ml/typing/*.cm[iox] ml/typing/*.o ml/typing/*~ ml/typing/*.annot rm -f bin/why.opt bin/why.byte bin/why.static bin/top rm -f bin/caduceus.opt bin/caduceus.byte rm -f bin/jessie.opt bin/jessie.byte rm -f bin/jessica.opt bin/jessica.byte rm -f bin/why-obfuscator.opt bin/why-obfuscator.byte rm -f bin/rv_merge.opt bin/rv_merge.byte rm -f bin/why-stat.opt bin/why-stat.byte rm -f bin/tool-stat.opt bin/tool-stat.byte rm -f bin/why2html.opt bin/why2html.byte rm -f bin/why-dp.opt bin/why-dp.byte rm -f bin/why-cpulimit rm -f lib/coq*/*.vo lib/coq*/*~ rm -f $(GENERATED) rm -rf output_why3 rm -f ergo.why rm -rf bench/plugins/*.cm[iox]* bench/plugins/*.annot # make -C atp clean # make -C doc clean # if test -d examples-v7; then \ # make -C examples-v7 clean ; \ # fi # make -C examples clean dist-clean:: clean rm -f Makefile config.status config.cache config.log coq-clean:: rm -f lib/coq*/*.vo examples/*/*.vo rm .depend.coq .PHONY: depend .depend depend: $(GENERATED) rm -f .depend $(OCAMLDEP) -slash $(INCLUDES) src/*/*.ml src/*/*.mli src/*.ml src/*.mli bench/plugins/*.ml > .depend ifeq ($(FRAMAC),yes) # $(MAKE) -C $(JESSIE_PLUGIN_PATH) depend endif .depend.coq: #lib/coq*/*.v if test @COQ@ = yes; then \ rm -f .depend.coq; \ $(COQDEP) -I lib/coq lib/coq/*.v > .depend.coq; \ $(COQDEP) -I lib/coq-v7 lib/coq-v7/*.v >> .depend.coq; \ else touch .depend.coq; \ fi alldepend: make -C examples-v7 depend make -C examples depend include .depend include .depend.coq ################################################################# # 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 (version.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.