########################################################################## # # # 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) DYNLINKCMA = dynlink.cma DYNLINKCMXA = dynlink.cmxa else DYNLINKCMA = DYNLINKCMXA = endif BFLAGS = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ OFLAGS = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ # external libraries common to all binaries EXTCMA = str.cma unix.cma nums.cma $(DYNLINKCMA) EXTCMXA = $(EXTCMA:.cma=.cmxa) ############### # main target ############### all: @OCAMLBEST@ .PHONY: byte opt clean depend all ############# # Why library ############# LIBGENERATED = src/config.ml \ src/parser/parser.mli src/parser/parser.ml src/parser/parser.output \ src/parser/lexer.ml src/driver/driver_lexer.ml \ src/driver/driver_parser.mli src/driver/driver_parser.ml \ src/driver/driver_parser.output \ src/driver/dynlink_compat.ml depend: $(LIBGENERATED) LIBDIRS=core util parser transform driver printer LIBCLEAN=$(addprefix src/, $(LIBDIRS)) LIBCLEAN:=$(addsuffix /*.cm[iox], $(LIBCLEAN)) \ $(addsuffix /*.annot, $(LIBCLEAN)) \ $(addsuffix /*.o, $(LIBCLEAN)) clean:: rm -f $(LIBCLEAN) $(LIBGENERATED) rm -f why.cm[iox] why.a why.o $(LIBCMA) $(LIBCMXA) include Version doc/version.tex src/config.ml: Version version.sh config.status BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) COQVER=@COQVER@ ./version.sh 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 := ptree.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 := driver_ast.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)) LIBCMO = src/config.cmo $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\ $(TRANSFORM_CMO) $(PRINTER_CMO) LIBCMX = $(LIBCMO:.cmo=.cmx) LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS)) $(LIBCMO) $(LIBCMX): INCLUDES=$(LIBINCLUDES) $(LIBCMX): OFLAGS+=-for-pack Why LIBCMA = why.cma LIBCMXA = why.cmxa byte: $(LIBCMA) opt: $(LIBCMA) $(LIBCMXA) $(LIBCMA): why.cmo $(OCAMLC) -a $(BFLAGS) -o $@ $^ $(LIBCMXA): why.cmx $(OCAMLOPT) -a $(OFLAGS) -o $@ $^ why.cmo: $(LIBCMO) $(OCAMLC) $(BFLAGS) -pack -o $@ $(LIBCMO) why.cmx: $(LIBCMX) $(OCAMLOPT) $(INCLUDES) -pack -o $@ $(LIBCMX) include .depend.lib .depend.lib: $(LIBGENERATED) $(OCAMLDEP) -slash $(LIBINCLUDES) $(LIBCMO:.cmo=.ml) $(LIBCMO:.cmo=.mli) > $@ depend: .depend.lib ################## # why binary ################## byte: bin/why.byte opt: bin/why.opt bin/why.opt: $(LIBCMXA) src/main.cmx $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^ $(STRIP) $@ bin/why.byte: $(LIBCMA) src/main.cmo $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^ clean:: rm -f src/main.cm[iox] src/main.annot rm -f bin/why.byte bin/why.opt ########## # whyml ########## PGM_GENERATED = src/programs/pgm_lexer.ml src/programs/pgm_parser.mli \ src/programs/pgm_parser.output src/programs/pgm_parser.ml PGM_CMO := pgm_parser.cmo pgm_lexer.cmo pgm_typing.cmo pgm_main.cmo PGM_CMO := $(addprefix src/programs/, $(PGM_CMO)) PGM_CMX = $(PGM_CMO:.cmo=.cmx) $(PGM_CMO) $(PGM_CMX): INCLUDES=-I src/programs/ opt: bin/whyml.opt byte: bin/whyml.byte bin/whyml.opt: $(LIBCMXA) $(PGM_CMX) $(if $(QUIET), @echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^ $(STRIP) $@ bin/whyml.byte: $(LIBCMA) $(PGM_CMO) $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^ include .depend.programs .depend.programs: $(PGM_GENERATED) $(OCAMLDEP) -slash -I src/programs/ $(PGM_CMO:.cmo=.ml) $(PGM_CMO:.cmo=.mli) > $@ depend: .depend.programs clean:: rm -f $(PGM_GENERATED) rm -f src/programs/*.cm[iox] src/programs/*.o src/programs/*.annot rm -f bin/whyml.byte bin/whyml.opt ############### # proof manager ############### src/orm/sql_orm_header.ml: src/orm/sql_access.ml src/orm/convert.ml ocaml src/orm/convert.ml $< $@ ORM_CMO := printer_utils.cmo sql_orm_header.cmo sql_orm.cmo ORM_CMO := $(addprefix src/orm/,$(ORM_CMO)) $(ORM_CMO): INCLUDES=-I src/orm -I +sqlite3 src/manager/db.ml: $(ORM_CMO) src/manager/orm_schema.ml ocaml -I src/orm src/manager/orm_schema.ml src/manager/orm_schema.ml: $(ORM_CMO) MANAGER_CMO := db.cmo MANAGER_CMO := $(addprefix src/manager/,$(MANAGER_CMO)) $(MANAGER_CMO): INCLUDES=-I src/manager -I +sqlite3 -I +threads bin/manager.byte: $(LIBCMA) $(MANAGER_CMO) $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) \ -thread -I +sqlite3 -I +threads $(EXTCMA) threads.cma sqlite3.cma -o $@ $^ # graphical interface ##################### IDE_CMO := ide_main.cmo IDE_CMO := $(addprefix src/ide/,$(IDE_CMO)) IDE_CMX = $(IDE_CMO:.cmo=.cmx) $(IDE_CMO) $(IDE_CMX): INCLUDES=-I src/ide/ byte: ide-byte-@LABLGTK2@ opt: ide-opt-@LABLGTK2@ ide-byte-yes: bin/whyide.byte ide-byte-no: ide-opt-yes: bin/whyide.opt ide-opt-no: bin/whyide.opt: $(LIBCMXA) $(IDE_CMX) $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) -I +threads -o $@ $(EXTCMXA) threads.cmxa lablgtk.cmxa lablgtksourceview.cmxa gtkThread.cmx $^ $(STRIP) $@ bin/whyide.byte: $(GCMO) $(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) -I +threads -o $@ $(EXTCMA) lablgtk.cma lablgtksourceview.cma threads.cma gtkThread.cmo $^ include .depend.ide .depend.ide: $(OCAMLDEP) -slash -I src/ide/ $(IDE_CMO:.cmo=.ml) $(IDE_CMO:.cmo=.mli) > $@ depend: .depend.ide clean:: rm -f bin/whyide.byte bin/whyide.opt rm -f src/ide/*.cm[iox] src/ide/*.o src/ide/*.annot # 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/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 #tools ###### bin/why-cpulimit: src/tools/@CPULIMIT@.c $(CC) -o $@ $^ # 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 -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 # 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 # 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 DOC ############## APIDOCSRC = $(UTIL_CMO:.cmo=.mli) $(CORE_CMO:.cmo=.mli) \ src/driver/call_provers.mli \ src/driver/driver.mli \ src/manager/state.mli .PHONY: apidoc apidoc: $(APIDOCSRC) rm -f apidoc/* mkdir -p apidoc $(OCAMLDOC) -d apidoc -html -I src/util -I src/core -I src/driver \ $(APIDOCSRC) # 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/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 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 *~ */*~ */*/*~ distclean:: clean rm -f Makefile config.status config.cache config.log ################################################################# # 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.