Commit 7f76c851 authored by Andrei Paskevich's avatar Andrei Paskevich

trick ocamldep by putting an empty why.ml in src.

If this works, it will be a less intrusive way to 
get dependencies right, than to use lib/why.mli.
parent a68c0d1b
...@@ -59,10 +59,8 @@ OCAMLVERSION = @OCAMLVERSION@ ...@@ -59,10 +59,8 @@ OCAMLVERSION = @OCAMLVERSION@
#PSVIEWER = @PSVIEWER@ #PSVIEWER = @PSVIEWER@
#PDFVIEWER = @PDFVIEWER@ #PDFVIEWER = @PDFVIEWER@
BFLAGS = -w Ae -dtypes -g -I lib $(INCLUDES) BFLAGS = -w Ae -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Ae -dtypes -I lib $(INCLUDES) OFLAGS = -w Ae -dtypes -I src $(INCLUDES)
DEPFLAGS = -I lib
# external libraries common to all binaries # external libraries common to all binaries
...@@ -84,10 +82,6 @@ all: @OCAMLBEST@ ...@@ -84,10 +82,6 @@ all: @OCAMLBEST@
.PHONY: byte opt clean depend all .PHONY: byte opt clean depend all
depend:
rm -f $^
make $^
############# #############
# Why library # Why library
############# #############
...@@ -124,7 +118,7 @@ LIBMODULES = src/config \ ...@@ -124,7 +118,7 @@ LIBMODULES = src/config \
$(addprefix src/printer/, $(LIB_PRINTER)) $(addprefix src/printer/, $(LIB_PRINTER))
LIBDIRS = util core parser driver transform printer LIBDIRS = util core parser driver transform printer
LIBINCLUDES = -I src/ $(addprefix -I src/, $(LIBDIRS)) LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
LIBML = $(addsuffix .ml, $(LIBMODULES)) LIBML = $(addsuffix .ml, $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES)) LIBMLI = $(addsuffix .mli, $(LIBMODULES))
...@@ -136,8 +130,8 @@ $(LIBCMX): OFLAGS += -for-pack Why ...@@ -136,8 +130,8 @@ $(LIBCMX): OFLAGS += -for-pack Why
# build targets # build targets
byte: lib/why.cma byte: src/why.cma
opt: lib/why.cmxa opt: src/why.cmxa
src/why.cma: src/why.cmo src/why.cma: src/why.cmo
$(OCAMLC) -a $(BFLAGS) -o $@ $^ $(OCAMLC) -a $(BFLAGS) -o $@ $^
...@@ -151,23 +145,12 @@ src/why.cmo: $(LIBCMO) ...@@ -151,23 +145,12 @@ src/why.cmo: $(LIBCMO)
src/why.cmx: $(LIBCMX) src/why.cmx: $(LIBCMX)
$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^ $(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
lib/why.cma: src/why.cma
cp -f src/why.o lib/why.o
cp -f $^ $@
lib/why.cmxa: src/why.cmxa
cp -f src/why.a lib/why.a
cp -f $^ $@
lib/why.cmi: src/why.cmo src/why.cmx
cp -f src/why.cmi lib/why.cmi
# depend target # depend target
include .depend.lib include .depend.lib
.depend.lib: src/config.ml $(LIBGENERATED) .depend.lib: src/config.ml $(LIBGENERATED)
$(OCAMLDEP) $(DEPFLAGS) -slash $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@ $(OCAMLDEP) -slash -I src $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
depend: .depend.lib depend: .depend.lib
...@@ -191,16 +174,17 @@ clean:: ...@@ -191,16 +174,17 @@ clean::
byte: bin/why.byte byte: bin/why.byte
opt: bin/why.opt opt: bin/why.opt
bin/why.opt: lib/why.cmxa src/main.cmx bin/why.opt: src/why.cmxa src/main.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@ $(STRIP) $@
bin/why.byte: lib/why.cma src/main.cmo bin/why.byte: src/why.cma src/main.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
src/main.cmo src/main.cmx: lib/why.cmi src/main.cmo: src/why.cmo
src/main.cmx: src/why.cmx
clean:: clean::
rm -f src/main.cm[iox] src/main.annot src/main.o rm -f src/main.cm[iox] src/main.annot src/main.o
...@@ -229,12 +213,12 @@ $(PGMCMO) $(PGMCMX): INCLUDES = -I src/programs ...@@ -229,12 +213,12 @@ $(PGMCMO) $(PGMCMX): INCLUDES = -I src/programs
byte: bin/whyml.byte byte: bin/whyml.byte
opt: bin/whyml.opt opt: bin/whyml.opt
bin/whyml.opt: lib/why.cmxa $(PGMCMX) bin/whyml.opt: src/why.cmxa $(PGMCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \ $(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@ $(STRIP) $@
bin/whyml.byte: lib/why.cma $(PGMCMO) bin/whyml.byte: src/why.cma $(PGMCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
...@@ -243,7 +227,7 @@ bin/whyml.byte: lib/why.cma $(PGMCMO) ...@@ -243,7 +227,7 @@ bin/whyml.byte: lib/why.cma $(PGMCMO)
include .depend.programs include .depend.programs
.depend.programs: $(PGMGENERATED) .depend.programs: $(PGMGENERATED)
$(OCAMLDEP) $(DEPFLAGS) -slash -I src/programs $(PGMML) $(PGMMLI) > $@ $(OCAMLDEP) -slash -I src -I src/programs $(PGMML) $(PGMMLI) > $@
depend: .depend.programs depend: .depend.programs
...@@ -274,12 +258,12 @@ opt: bin/manager.opt ...@@ -274,12 +258,12 @@ opt: bin/manager.opt
bin/manager.opt bin/manager.byte: INCLUDES = -I +sqlite3 bin/manager.opt bin/manager.byte: INCLUDES = -I +sqlite3
bin/manager.opt: lib/why.cmxa $(MNGCMX) bin/manager.opt: src/why.cmxa $(MNGCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \ $(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) sqlite3.cmxa $^ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) sqlite3.cmxa $^
$(STRIP) $@ $(STRIP) $@
bin/manager.byte: lib/why.cma $(MNGCMO) bin/manager.byte: src/why.cma $(MNGCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) sqlite3.cma $^ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) sqlite3.cma $^
...@@ -288,7 +272,7 @@ bin/manager.byte: lib/why.cma $(MNGCMO) ...@@ -288,7 +272,7 @@ bin/manager.byte: lib/why.cma $(MNGCMO)
include .depend.manager include .depend.manager
.depend.manager: .depend.manager:
$(OCAMLDEP) $(DEPFLAGS) -slash -I src/manager/ $(MNGML) $(MNGMLI) > $@ $(OCAMLDEP) -slash -I src -I src/manager $(MNGML) $(MNGMLI) > $@
depend: .depend.manager depend: .depend.manager
...@@ -322,14 +306,14 @@ endif ...@@ -322,14 +306,14 @@ endif
bin/whyide.opt bin/whyide.byte: INCLUDES = -I +lablgtk2 -I +threads bin/whyide.opt bin/whyide.byte: INCLUDES = -I +lablgtk2 -I +threads
bin/whyide.opt: lib/why.cmxa $(IDE_CMX) bin/whyide.opt: src/why.cmxa $(IDE_CMX)
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^ lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^
$(STRIP) $@ $(STRIP) $@
bin/whyide.byte: lib/why.cma $(IDE_CMO) bin/whyide.byte: src/why.cma $(IDE_CMO)
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
lablgtk.cma lablgtksourceview2.cma gtkThread.cmo $^ lablgtk.cma lablgtksourceview2.cma gtkThread.cmo $^
...@@ -339,7 +323,7 @@ bin/whyide.byte: lib/why.cma $(IDE_CMO) ...@@ -339,7 +323,7 @@ bin/whyide.byte: lib/why.cma $(IDE_CMO)
include .depend.ide include .depend.ide
.depend.ide: .depend.ide:
$(OCAMLDEP) $(DEPFLAGS) -slash -I src/ide $(IDEML) $(IDEMLI) > $@ $(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
depend: .depend.ide depend: .depend.ide
...@@ -366,7 +350,7 @@ src/coq-plugin/whytac.cmxs: INCLUDES = $(addprefix -I @COQLIB@/, $(COQTREES)) ...@@ -366,7 +350,7 @@ src/coq-plugin/whytac.cmxs: INCLUDES = $(addprefix -I @COQLIB@/, $(COQTREES))
#src/coq-plugin/whytac.cmo: BFLAGS+=-rectypes #src/coq-plugin/whytac.cmo: BFLAGS+=-rectypes
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes
src/coq-plugin/whytac.cmxs: lib/why.cmxa src/coq-plugin/whytac.ml src/coq-plugin/whytac.cmxs: src/why.cmxa src/coq-plugin/whytac.ml
$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^ $(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
####### #######
...@@ -603,8 +587,7 @@ otags: ...@@ -603,8 +587,7 @@ otags:
wc: wc:
ocamlwc -p src/*.ml* src/*/*.ml* ocamlwc -p src/*.ml* src/*/*.ml*
dep: dep: depend
$(MAKE) depend
cat .depend* | ocamldot | dot -Tpdf > dep.pdf cat .depend* | ocamldot | dot -Tpdf > dep.pdf
# $(PDFVIEWER) dep.pdf # $(PDFVIEWER) dep.pdf
...@@ -755,6 +738,10 @@ distclean: clean ...@@ -755,6 +738,10 @@ distclean: clean
rm -f config.status config.cache config.log \ rm -f config.status config.cache config.log \
Makefile src/config.ml doc/version.tex Makefile src/config.ml doc/version.tex
depend:
rm -f $^
$(MAKE) $^
################################################################# #################################################################
# Building the Why platform with ocamlbuild (OCaml 3.10 needed) # # Building the Why platform with ocamlbuild (OCaml 3.10 needed) #
################################################################# #################################################################
......
(* This file is a stub for ocamldep. Do not delete it. *)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment