Makefile: renamed .why to .mlw for stdlib files

parent 544987d5
......@@ -1091,40 +1091,40 @@ drivers/coq-realizations.aux: Makefile
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-seq update-coq-bv update-coq-ieee_float
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/int.why
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/int.mlw
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T int.$$f -o $(GENERATED_PREFIX_COQ)/int/; done
update-coq-bool: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/bool.why
update-coq-bool: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/bool.mlw
for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T bool.$$f -o $(GENERATED_PREFIX_COQ)/bool/; done
update-coq-real: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/real.why
update-coq-real: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/real.mlw
for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T real.$$f -o $(GENERATED_PREFIX_COQ)/real/; done
update-coq-number: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/number.why
update-coq-number: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/number.mlw
for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T number.$$f -o $(GENERATED_PREFIX_COQ)/number/; done
update-coq-set: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/set.why
update-coq-set: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/set.mlw
for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T set.$$f -o $(GENERATED_PREFIX_COQ)/set/; done
update-coq-map: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/map.why
update-coq-map: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/map.mlw
for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T map.$$f -o $(GENERATED_PREFIX_COQ)/map/; done
update-coq-list: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/list.why
update-coq-list: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/list.mlw
for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T list.$$f -o $(GENERATED_PREFIX_COQ)/list/; done
update-coq-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/option.why
update-coq-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/option.mlw
for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T option.$$f -o $(GENERATED_PREFIX_COQ)/option/; done
update-coq-seq: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/seq.why
update-coq-seq: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/seq.mlw
for f in $(COQLIBS_SEQ_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T seq.$$f -o $(GENERATED_PREFIX_COQ)/seq/; done
update-coq-bv: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/bv.why
update-coq-bv: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/bv.mlw
for f in $(COQLIBS_BV_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T bv.$$f -o $(GENERATED_PREFIX_COQ)/bv/; done
update-coq-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/ieee_float.why
update-coq-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/ieee_float.mlw
for f in $(COQLIBS_IEEEFLOAT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T ieee_float.$$f -o $(GENERATED_PREFIX_COQ)/ieee_float/; done
update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/floating_point.why
update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/floating_point.mlw
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T floating_point.$$f -o $(GENERATED_PREFIX_COQ)/floating_point/; done
......@@ -1355,55 +1355,55 @@ endif
update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
$(ISABELLELIBS_INT): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/int.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/int.mlw
$(SHOW) "Generating Isabelle realization for int.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/int
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/int/
$(ISABELLELIBS_BOOL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/bool.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/bool.mlw
$(SHOW) "Generating Isabelle realization for bool.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/bool
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bool/
$(ISABELLELIBS_REAL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/real.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/real.mlw
$(SHOW) "Generating Isabelle realization for real.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/real
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/real/
$(ISABELLELIBS_NUMBER): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/number.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/number.mlw
$(SHOW) "Generating Isabelle realization for number.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/number
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/number/
$(ISABELLELIBS_SET): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/set.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/set.mlw
$(SHOW) "Generating Isabelle realization for set.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/set
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/set/
$(ISABELLELIBS_MAP): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/map.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/map.mlw
$(SHOW) "Generating Isabelle realization for map.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/map
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/map/
$(ISABELLELIBS_LIST): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/list.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/list.mlw
$(SHOW) "Generating Isabelle realization for list.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/list
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/list/
$(ISABELLELIBS_OPTION): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/option.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/option.mlw
$(SHOW) "Generating Isabelle realization for option.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/option
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/option/
$(ISABELLELIBS_BV): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/bv.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/bv.mlw
$(SHOW) "Generating Isabelle realization for bv.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/bv
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bv/
......@@ -1998,7 +1998,7 @@ STDLIBS = \
STDLIBFILES = $(patsubst %,stdlib/%.mlw, $(STDLIBS))
# TODO: remove the hack about int.why once it has become builtin
# TODO: remove the hack about int.mlw once it has become builtin
stdlibdoc: $(STDLIBFILES) bin/why3doc.@OCAMLBEST@
mkdir -p doc/stdlibdoc
sed -e "s/use import Int/use import int.Int/" stdlib/int.mlw > int.mlw
......
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