Commit 12b97bbb authored by Guillaume Melquiond's avatar Guillaume Melquiond

Make sure that the opt and byte targets can be built concurrently.

The main issue is that both ocamlc and ocamlopt write a .cmi file when
there is no .mli file, so the .cmi file might end up being corrupted due
to concurrent accesses.

The ugly fix is to prevent ocamlopt from creating a .cmi file by lying to
it: ".mli files are no interface files, .but cmi files are". So ocamlopt
behaves as if there had been a .mli file in the first place and does not
try to produce a compiled interface from the .ml file. Note that we use
the .cmi file because it happens to have the same base name, but any other
file would have worked, e.g. the .dep file, since ocamlopt does not even
read the file to check that it is actually an interface file.

Since ocamlopt now believes that the .ml file has an interface, it needs a
compiled interface to check its signature against, so the .cmi file has to
be created beforehand. So the .cmx file is made to depend on the .cmi file
and the .cmi file on the .cmo file.

This might seem to add a dependency from the opt build on the byte build,
but since ocamldep already says that the tools depend on lib/why3/why3.cmo
due to the pack, this does not make the situation any worse.

Note that there is a single file for which the .cmi hack cannot be used:
src/tools/why3extract.ml. Indeed, if we lie to ocamlopt, it will try to
use lib/why3/why3extract.cmi as the compiled interface (?!) and thus fail
to compile src/tools/why3extract.ml, obviously. So the hack is disabled
for this file, which means that src/tools/why3extract.cmi could end up
being corrupted, but we do not care.
parent aa6a5ee8
......@@ -110,6 +110,9 @@ OFLAGS += -bin-annot
BFLAGS += -bin-annot
endif
# see http://caml.inria.fr/mantis/view.php?id=4991
CMIHACK = -intf-suffix .cmi
# external libraries common to all binaries
EXTOBJS = @MENHIRLIB@
......@@ -261,9 +264,9 @@ lib/why3/why3.cmo: $(LIBCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
lib/why3/why3.cmx: $(LIBCMX)
lib/why3/why3.cmx: $(LIBCMX) lib/why3/why3.cmo
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
$(HIDE)$(OCAMLOPT) $(OFLAGS) $(CMIHACK) -pack -o $@ $(filter %.cmx, $^)
# clean and depend
......@@ -1302,9 +1305,9 @@ lib/why3/why3extract.cmo: $(OCAMLLIBS_CMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
lib/why3/why3extract.cmx: $(OCAMLLIBS_CMX)
lib/why3/why3extract.cmx: $(OCAMLLIBS_CMX) lib/why3/why3extract.cmo
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
$(HIDE)$(OCAMLOPT) $(OFLAGS) $(CMIHACK) -pack -o $@ $(filter %.cmx, $^)
install_no_local_lib::
$(MKDIR_P) $(OCAMLINSTALLLIB)/why3
......@@ -1814,16 +1817,26 @@ clean::
# suppress "unused rec" warning for Menhir-produced files
%.cmx: %.ml %.mly
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) -w -39 $<
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) -w -39 $(CMIHACK) $<
%.cmo: %.ml
$(SHOW) 'Ocamlc $<'
$(HIDE)$(OCAMLC) -c $(BFLAGS) $<
%.cmx: %.ml
%.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 (!!!)
src/tools/why3extract.cmx: src/tools/why3extract.ml
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) $<
%.cmx: %.ml
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) $(CMIHACK) $<
%.cma:
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) -a $(BFLAGS) -o $@ $^
......@@ -1850,7 +1863,9 @@ clean::
%.dep: %.ml
$(SHOW) 'Ocamldep $<'
$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< $(TOTARGET)
$(HIDE)($(OCAMLDEP) $(DEPFLAGS) $<; \
echo '$*.cmx : $*.cmi'; \
echo '$*.cmi : $*.cmo') $(TOTARGET)
%.opt:
$(SHOW) 'Linking $@'
......
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