Skip to content

GitLab

why3
why3
Commit 3e4ca0ac authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files
Options

Depend on the proper executable file when updating realizations.

parent 2f4c8e72
Hide whitespace changes
Inline Side-by-side
Showing with 18 additions and 18 deletions
Makefile.in
View file @ 3e4ca0ac
......@@ -944,31 +944,31 @@ clean:: clean-coq
update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp
update-coq-int: bin/why3 drivers/coq-realizations.aux theories/int.why
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
update-coq-bool: bin/why3 drivers/coq-realizations.aux theories/bool.why
update-coq-bool: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bool.why
for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bool.$$f -o lib/coq/bool/; done
update-coq-real: bin/why3 drivers/coq-realizations.aux theories/real.why
update-coq-real: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/real.why
for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
update-coq-number: bin/why3 drivers/coq-realizations.aux theories/number.why
update-coq-number: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/number.why
for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T number.$$f -o lib/coq/number/; done
update-coq-set: bin/why3 drivers/coq-realizations.aux theories/set.why
update-coq-set: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/set.why
for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T set.$$f -o lib/coq/set/; done
update-coq-map: bin/why3 drivers/coq-realizations.aux theories/map.why
update-coq-map: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/map.why
for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T map.$$f -o lib/coq/map/; done
update-coq-list: bin/why3 drivers/coq-realizations.aux theories/list.why
update-coq-list: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/list.why
for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T list.$$f -o lib/coq/list/; done
update-coq-option: bin/why3 drivers/coq-realizations.aux theories/option.why
update-coq-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/option.why
for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T option.$$f -o lib/coq/option/; done
update-coq-fp: bin/why3 drivers/coq-realizations.aux theories/floating_point.why
update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/floating_point.why
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
else
......@@ -1042,7 +1042,7 @@ install_no_local::
install_local:: drivers/pvs-realizations.aux
update-pvs: bin/why3 drivers/pvs-realizations.aux
update-pvs: bin/why3realize.@OCAMLBEST@ drivers/pvs-realizations.aux
for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done
for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
for f in $(PVSLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -D drivers/pvs-realize.drv -T list.$$f -o lib/pvs/list/; done
......@@ -1136,42 +1136,42 @@ install_local::
update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
$(ISABELLELIBS_INT): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_INT): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
mkdir -p lib/isabelle/int
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T int.$(notdir $(basename $@)) -o lib/isabelle/int/
$(ISABELLELIBS_BOOL): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_BOOL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/bool.why
mkdir -p lib/isabelle/bool
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T bool.$(notdir $(basename $@)) -o lib/isabelle/bool/
$(ISABELLELIBS_REAL): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_REAL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/real.why
mkdir -p lib/isabelle/real
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T real.$(notdir $(basename $@)) -o lib/isabelle/real/
$(ISABELLELIBS_NUMBER): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_NUMBER): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/number.why
mkdir -p lib/isabelle/number
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T number.$(notdir $(basename $@)) -o lib/isabelle/number/
$(ISABELLELIBS_SET): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_SET): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/set.why
mkdir -p lib/isabelle/set
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T set.$(notdir $(basename $@)) -o lib/isabelle/set/
$(ISABELLELIBS_MAP): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_MAP): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/map.why
mkdir -p lib/isabelle/map
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T map.$(notdir $(basename $@)) -o lib/isabelle/map/
$(ISABELLELIBS_LIST): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_LIST): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/list.why
mkdir -p lib/isabelle/list
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T list.$(notdir $(basename $@)) -o lib/isabelle/list/
$(ISABELLELIBS_OPTION): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_OPTION): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/option.why
mkdir -p lib/isabelle/option
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
......
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