mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
2442 lines
79 KiB
Makefile
2442 lines
79 KiB
Makefile
####################################################################
|
|
# #
|
|
# The Why3 Verification Platform / The Why3 Development Team #
|
|
# Copyright 2010-2025 -- Inria - CNRS - Paris-Saclay University #
|
|
# #
|
|
# This software is distributed under the terms of the GNU Lesser #
|
|
# General Public License version 2.1, with the special exception #
|
|
# on linking described in file LICENSE. #
|
|
####################################################################
|
|
|
|
.DELETE_ON_ERROR:
|
|
|
|
VERBOSEMAKE ?= @enable_verbose_make@
|
|
|
|
ifeq ($(VERBOSEMAKE),yes)
|
|
SHOW = @true
|
|
HIDE =
|
|
else
|
|
SHOW = @echo
|
|
HIDE = @
|
|
endif
|
|
|
|
# install the binaries
|
|
DESTDIR =
|
|
|
|
prefix = @prefix@
|
|
exec_prefix = @exec_prefix@
|
|
datarootdir = @datarootdir@
|
|
|
|
ifneq (@OCAML_OS_TYPE@,Win32)
|
|
BINDIR = $(DESTDIR)@bindir@
|
|
LIBDIR = $(DESTDIR)@libdir@
|
|
DATADIR = $(DESTDIR)@datarootdir@
|
|
MANDIR = $(DESTDIR)@mandir@
|
|
else
|
|
# Convert every \ to / in Windows paths so that the \ do not need to be escaped
|
|
BINDIR = $(subst \,/,$(DESTDIR)@bindir@)
|
|
LIBDIR = $(subst \,/,$(DESTDIR)@libdir@)
|
|
DATADIR = $(subst \,/,$(DESTDIR)@datarootdir@)
|
|
MANDIR = $(subst \,/,$(DESTDIR)@mandir@)
|
|
endif
|
|
TOOLDIR = $(LIBDIR)/why3/commands
|
|
|
|
# OS specific stuff
|
|
EXE = @EXE@
|
|
|
|
# other variables
|
|
CC = @CC@
|
|
MKDIR_P = @MKDIR_P@
|
|
INSTALL = @INSTALL@
|
|
INSTALL_DATA = @INSTALL_DATA@
|
|
|
|
ifeq (@enable_ocamlfind@,yes)
|
|
OCAMLC = @OCAMLFIND@ ocamlc
|
|
OCAMLOPT = @OCAMLFIND@ ocamlopt
|
|
OCAMLDEP = @OCAMLFIND@ ocamldep
|
|
OCAMLDOC = @OCAMLFIND@ ocamldoc
|
|
else
|
|
OCAMLC = @OCAMLC@
|
|
OCAMLOPT = @OCAMLOPT@
|
|
OCAMLDEP = @OCAMLDEP@
|
|
OCAMLDOC = @OCAMLDOC@
|
|
endif
|
|
|
|
OCAMLFIND = @OCAMLFIND@
|
|
OCAMLLEX = @OCAMLLEX@
|
|
OCAMLYACC = @OCAMLYACC@
|
|
OCAMLLIB = @OCAMLLIB@
|
|
OCAMLINSTALLLIB = $(DESTDIR)@OCAMLINSTALLLIB@
|
|
OCAMLBEST = @OCAMLBEST@
|
|
OCAMLVERSION = @OCAMLVERSION@
|
|
CC = gcc
|
|
COQC = @COQC@
|
|
COQDEP = @COQDEP@
|
|
COQFLAGS = @COQFLAGS@
|
|
FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@
|
|
MENHIR = @MENHIR@
|
|
|
|
DEPFLAGS = -slash
|
|
|
|
ifeq (@enable_why3_lib@,yes)
|
|
INCLUDES += -I lib/why3
|
|
endif
|
|
ifeq (@OCAMLBEST@,opt)
|
|
# the semantics of the -native flag changed in ocaml 4.03.0
|
|
#DEPFLAGS += -native
|
|
endif
|
|
|
|
ifeq (@OCAMLBEST@,opt)
|
|
SHAREDBEST=cmxs
|
|
else
|
|
SHAREDBEST=cma
|
|
endif
|
|
|
|
ifeq (@LATEX@,rubber)
|
|
LATEXCOMP=rubber --warn all --pdf
|
|
LATEXCLEAN=rubber --pdf --clean
|
|
endif
|
|
|
|
ifeq (@LATEX@,latexmk)
|
|
LATEXCOMP=LATEXOPTS= latexmk --pdf
|
|
LATEXCLEAN=LATEXOPTS= latexmk --pdf -C
|
|
endif
|
|
|
|
ifeq (@LATEX@,pdflatex)
|
|
LATEXCOMP=pdflatex
|
|
LATEXCLEAN=true
|
|
endif
|
|
|
|
SPHINX = @SPHINX@
|
|
|
|
EMACS = @EMACS@
|
|
|
|
#PSVIEWER = @PSVIEWER@
|
|
#PDFVIEWER = @PDFVIEWER@
|
|
|
|
EXTINCLUDES = @WHY3INCLUDE@ @REINCLUDE@ @ZIPINCLUDE@ @MENHIRINCLUDE@ @BIGINTINCLUDE@ @INFERINCLUDE@ @YOJSONINCLUDES@
|
|
|
|
# warnings are enabled and non fatal by default, except:
|
|
# - disabled:
|
|
# 4 Fragile pattern matching: matching that will remain complete even
|
|
# if additional constructors are added to one of the variant types
|
|
# matched.
|
|
# 9 Missing fields in a record pattern.
|
|
# 41 Ambiguous constructor or label name.
|
|
# 42 Reliance on type-directed disambiguation
|
|
# 44 Open statement shadows an already defined identifier.
|
|
# 45 Open statement shadows an already defined label or constructor.
|
|
# 52 The argument of this constructor should not be matched against a
|
|
# constant pattern; the actual value of the argument could change
|
|
# in the future.
|
|
# - fatal:
|
|
# 5 Partially applied function: expression whose result has function
|
|
# type and is ignored.
|
|
# 8 Partial match: missing cases in pattern-matching.
|
|
# 14 Illegal backslash escape in string
|
|
# 48 Implicit elimination of optional arguments.
|
|
# 50 Unexpected documentation comment.
|
|
|
|
WARNINGS = A-4-9-41-42-44-45-52@5@8@14@48@50
|
|
|
|
FLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g -thread $(INCLUDES)
|
|
OFLAGS = $(FLAGS)
|
|
BFLAGS = $(FLAGS)
|
|
|
|
ifeq (@enable_ocamlfind@,yes)
|
|
FLAGS += $(addprefix -package ,$(EXTPKGS))
|
|
OLINKFLAGS += -linkpkg -linkall
|
|
BLINKFLAGS += -linkpkg -linkall
|
|
else
|
|
FLAGS += $(EXTINCLUDES)
|
|
OLINKFLAGS = -linkall $(EXTCMXA)
|
|
BLINKFLAGS = -linkall $(EXTCMA)
|
|
endif
|
|
|
|
|
|
# see http://caml.inria.fr/mantis/view.php?id=4991
|
|
CMIHACK = -intf-suffix .cmi
|
|
|
|
CMP_CP = cmp -s $< $@ || cp $< $@
|
|
|
|
# external libraries common to all binaries
|
|
|
|
ifeq (@menhirlib_cmo@,yes)
|
|
EXTOBJS = menhirLib
|
|
EXTLIBS =
|
|
else
|
|
EXTOBJS =
|
|
EXTLIBS = menhirLib
|
|
endif
|
|
|
|
EXTLIBS += @RELIB@ unix zarith dynlink result easy_format biniou yojson @ZIPLIB@ @WHY3LIB@ @INFERLIB@
|
|
EXTPKGS = menhirLib @RELIB@ unix zarith dynlink yojson @ZIPLIB@ @MLMPFR@ @WHY3LIB@ @INFERPKG@ @SEXPLIB@ @SEXPLIBPPX@
|
|
|
|
EXTCMA = $(addsuffix .cmo,$(EXTOBJS)) $(addsuffix .cma,$(EXTLIBS))
|
|
EXTCMXA = $(addsuffix .cmx,$(EXTOBJS)) $(addsuffix .cmxa,$(EXTLIBS))
|
|
|
|
INSTALLED_LIB_EXTS = a cma cmx cmi cmxa cmxs cmt cmti
|
|
COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo annot dep conflicts
|
|
|
|
TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})
|
|
|
|
# Variables added for checking realizations
|
|
GENERATED_PREFIX_COQ="lib/coq"
|
|
GENERATED_PREFIX_ISABELLE=lib/isabelle
|
|
|
|
ifeq (@enable_why3_lib@,yes)
|
|
WHY3CMA = lib/why3/why3.cma
|
|
WHY3CMXA = lib/why3/why3.cmxa
|
|
else
|
|
WHY3CMA =
|
|
WHY3CMXA =
|
|
endif
|
|
|
|
###############
|
|
# main target
|
|
###############
|
|
|
|
ifeq (@enable_why3_lib@,yes)
|
|
all: @OCAMLBEST@
|
|
else
|
|
all:
|
|
endif
|
|
|
|
plugins: plugins.@OCAMLBEST@
|
|
opt: plugins.opt
|
|
byte: plugins.byte
|
|
|
|
ifeq (@enable_local@,yes)
|
|
all: install_local
|
|
endif
|
|
|
|
.PHONY: byte opt clean depend all install install-lib uninstall
|
|
.PHONY: install-bin install-data uninstall-bin uninstall-data
|
|
.PHONY: install-bash install-emacs install-framac
|
|
.PHONY: uninstall-bash uninstall-emacs uninstall-framac
|
|
.PHONY: ide install-ide uninstall-ide
|
|
.PHONY: coq install-coq uninstall-coq clean-coq
|
|
.PHONY: pvs install-pvs uninstall-pvs clean-pvs
|
|
.PHONY: install-isabelle clean-isabelle
|
|
.PHONY: plugins plugins.byte plugins.opt
|
|
.PHONY: trywhy3 clean-trywhy3
|
|
|
|
.SUFFIXES:
|
|
|
|
MAKEINC =
|
|
CLEANDIRS =
|
|
CLEANLIBS =
|
|
GENERATED =
|
|
|
|
##############
|
|
# Why3 library
|
|
##############
|
|
|
|
LIBGENERATED = \
|
|
src/util/config.ml \
|
|
src/util/rc.ml src/util/lexlib.ml src/util/mysexplib.ml \
|
|
src/util/json_parser.mli src/util/json_parser.ml \
|
|
src/util/json_lexer.ml src/util/mlmpfr_wrapper.ml \
|
|
src/parser/lexer.ml \
|
|
src/core/parser_tokens.mli src/core/parser_tokens.ml \
|
|
src/parser/parser.mli src/parser/parser.ml \
|
|
src/parser/parser_messages.ml \
|
|
src/driver/driver_parser.mli src/driver/driver_parser.ml \
|
|
src/driver/driver_lexer.ml \
|
|
src/driver/sexp.ml \
|
|
src/session/compress.ml src/session/xml.ml \
|
|
src/session/strategy_parser.ml
|
|
|
|
LIB_UTIL = exn_printer mysexplib config bigInt mlmpfr_wrapper util opt lists strings \
|
|
pp extmap extset exthtbl weakhtbl diffmap hcpt \
|
|
hashcons wstdlib getopt \
|
|
json_base json_parser json_lexer \
|
|
debug loc print_tree \
|
|
cmdline sysutil lexlib rc plugin bigInt number constant vector pqueue
|
|
|
|
ifeq (@enable_re@,no)
|
|
LIBGENERATED += src/util/re.ml
|
|
LIB_UTIL += re
|
|
endif
|
|
|
|
LIB_CORE = \
|
|
ident ty term pattern decl coercion theory \
|
|
parser_tokens keywords \
|
|
task pretty dterm env trans printer model_parser
|
|
|
|
LIB_DRIVER = prove_client whyconf call_provers driver_parser driver_lexer driver \
|
|
autodetection smtv2_model_defs sexp smtv2_model_parser
|
|
|
|
LIB_MLW = ity expr pdecl eval_match typeinv vc pmodule dexpr big_real \
|
|
pinterp_core rac pinterp check_ce
|
|
|
|
ifeq (@enable_infer@,yes)
|
|
LIB_INFER = o2oterm domain infer_why3 quant_domain union_find disjunctive_term_domain uf_domain infer_cfg infer_loop
|
|
endif
|
|
|
|
ifeq (@enable_bddinfer@,yes)
|
|
LIB_BDDINFER = bddparam abstract ast interp_expression infer why3infer
|
|
endif
|
|
|
|
LIB_EXTRACT = mltree compile mlinterp pdriver ml_printer \
|
|
c ocaml cakeml java
|
|
|
|
LIB_PARSER = ptree ptree_helpers glob typing \
|
|
parser_messages parser typing report lexer mlw_printer \
|
|
sexp_parser
|
|
|
|
LIB_TRANSFORM = simplify_formula inlining split_goal \
|
|
args_wrapper reduction_engine compute \
|
|
remove_unused detect_polymorphism \
|
|
fold_defs eliminate_quantifiers \
|
|
eliminate_definition extensional \
|
|
abstract_quantifiers eliminate_unknown_types \
|
|
eliminate_unknown_lsymbols eliminate_symbol \
|
|
eliminate_inductive eliminate_let eliminate_if \
|
|
libencoding eliminate_algebraic discriminate encoding \
|
|
encoding_select encoding_guards_full encoding_tags_full \
|
|
encoding_guards encoding_tags encoding_twin \
|
|
encoding_sort simplify_array filter_trigger \
|
|
abstraction close_epsilon lift_epsilon \
|
|
eliminate_gnatprove_guard_epsilon \
|
|
eliminate_epsilon instantiate_predicate smoke_detector \
|
|
prop_curry eliminate_literal \
|
|
generic_arg_trans_utils case apply subst \
|
|
introduction ind_itp destruct cut congruence \
|
|
rec_logic gnat_rewrite eliminate_unused gnat_split_conj \
|
|
gnat_split_disj gnat_trivial \
|
|
eliminate_unused_hypo eliminate_literal induction induction_pr \
|
|
induction induction_pr prepare_for_counterexmp \
|
|
reflection keep_only_arithmetic
|
|
|
|
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\
|
|
pvs isabelle \
|
|
simplify gappa cvc3 yices mathematica
|
|
|
|
LIB_SESSION = compress xml termcode session_itp \
|
|
strategy strategy_parser controller_itp \
|
|
server_utils itp_communication \
|
|
itp_server json_util unix_scheduler
|
|
|
|
LIB_CMIONLY = driver/driver_ast
|
|
|
|
LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \
|
|
$(addprefix src/core/, $(LIB_CORE)) \
|
|
$(addprefix src/driver/, $(LIB_DRIVER)) \
|
|
$(addprefix src/mlw/, $(LIB_MLW)) \
|
|
$(addprefix src/infer/, $(LIB_INFER)) \
|
|
$(addprefix src/extract/, $(LIB_EXTRACT)) \
|
|
$(addprefix src/parser/, $(LIB_PARSER)) \
|
|
$(addprefix src/bddinfer/, $(LIB_BDDINFER)) \
|
|
$(addprefix src/transform/, $(LIB_TRANSFORM)) \
|
|
$(addprefix src/printer/, $(LIB_PRINTER)) \
|
|
$(addprefix src/session/, $(LIB_SESSION))
|
|
|
|
LIBDIRS = util core driver mlw extract parser transform printer session gnat
|
|
|
|
ifeq (@enable_infer@,yes)
|
|
LIBDIRS += infer
|
|
endif
|
|
|
|
ifeq (@enable_bddinfer@,yes)
|
|
LIBDIRS += bddinfer
|
|
endif
|
|
|
|
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
|
|
|
|
LIBDEP = $(addsuffix .dep, $(LIBMODULES)) $(LIB_CMIONLY:%=src/%.dep)
|
|
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
|
|
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
|
|
LIBCMI = $(addsuffix .cmi, $(LIBMODULES)) $(LIB_CMIONLY:%=src/%.cmi)
|
|
|
|
$(LIBDEP) $(LIBCMO) $(LIBCMX) $(LIBCMI): INCLUDES += $(LIBINCLUDES)
|
|
$(LIBCMX): OFLAGS += -for-pack Why3
|
|
|
|
$(LIBDEP): $(LIBGENERATED)
|
|
|
|
src/parser/ptree.cmx src/parser/ptree.cmo: FLAGS += -w -70
|
|
src/util/mysexplib.cmx src/util/mysexplib.cmo: FLAGS += -w -70
|
|
|
|
# Mlmpfr
|
|
|
|
ifeq (@enable_mpfr@,yes)
|
|
|
|
ifeq (@old_mpfr@,yes)
|
|
src/util/mlmpfr_wrapper.ml: src/util/mlmpfr_old.ml Makefile
|
|
$(HIDE)$(CMP_CP)
|
|
else ifeq (@enable_mpfr@,yes)
|
|
src/util/mlmpfr_wrapper.ml: src/util/mlmpfr_real.ml Makefile
|
|
$(HIDE)$(CMP_CP)
|
|
endif
|
|
|
|
else
|
|
src/util/mlmpfr_wrapper.ml: src/util/mlmpfr_dummy.ml Makefile
|
|
$(HIDE)$(CMP_CP)
|
|
endif
|
|
|
|
# Ocamlzip
|
|
|
|
ifeq (@enable_zip@,yes)
|
|
src/session/compress.ml: src/session/compress_z.ml Makefile
|
|
$(HIDE)$(CMP_CP)
|
|
else
|
|
src/session/compress.ml: src/session/compress_none.ml Makefile
|
|
$(HIDE)$(CMP_CP)
|
|
endif
|
|
|
|
# sexp_conv
|
|
|
|
ifeq (@enable_sexp@, yes)
|
|
src/util/mysexplib.ml: src/util/mysexplib-real.ml Makefile
|
|
$(HIDE)$(CMP_CP)
|
|
else
|
|
src/util/mysexplib.ml: src/util/mysexplib-dummy.ml Makefile
|
|
$(HIDE)$(CMP_CP)
|
|
endif
|
|
|
|
.PHONY: initialize_messages update-parsing-error-handling
|
|
|
|
PARSERS=src/parser/parser_common.mly src/parser/parser.mly
|
|
|
|
src/parser/parser_messages.ml: src/parser/handcrafted.messages
|
|
@rm -f src/parser/parser_messages.ml src/parser/parser_messages.ml.tmp
|
|
@$(MENHIR) --explain --strict $(PARSERS) --base src/parser/parser --update-errors \
|
|
src/parser/handcrafted.messages > src/parser/handcrafted.messages.temp
|
|
@if ! diff -b src/parser/handcrafted.messages src/parser/handcrafted.messages.temp > /dev/null; then \
|
|
echo "Parsing error handling must be updated, the file 'src/parser/handcrafted.messages.temp' \
|
|
contains an updated version that must be checked before replacing 'src/parser/handcrafted.messages'"; \
|
|
exit 1; \
|
|
fi
|
|
@rm -f src/parser/handcrafted.messages.temp
|
|
$(MENHIR) --explain --strict $(PARSERS) --base src/parser/parser --compile-errors \
|
|
src/parser/handcrafted.messages > src/parser/parser_messages.ml
|
|
|
|
clean::
|
|
rm -f src/parser/parser_messages.ml.tmp src/parser/handcrafted.messages.temp
|
|
|
|
# debug optimisation ppx
|
|
|
|
ifeq (@enable_ppx@,yes)
|
|
src/util/ppx_debug_optim$(EXE): src/util/debug_optim.ml
|
|
$(SHOW) 'Linking $@'
|
|
$(HIDE) $(OCAMLFIND) opt -package ppxlib -linkpkg src/util/debug_optim.ml -o $@
|
|
|
|
ifeq (@OCAML_OS_TYPE@,Win32)
|
|
# Relative calls to executable on Windows cannot use / as path separator
|
|
PPX_DEBUG_OPTIM_EXE = src\\util\\ppx_debug_optim$(EXE)
|
|
else
|
|
PPX_DEBUG_OPTIM_EXE = src/util/ppx_debug_optim$(EXE)
|
|
endif
|
|
|
|
src/transform/reflection.cmx: src/util/ppx_debug_optim$(EXE)
|
|
src/transform/reflection.cmx: OFLAGS += -ppx $(PPX_DEBUG_OPTIM_EXE)
|
|
src/extract/mlinterp.cmx: src/util/ppx_debug_optim$(EXE)
|
|
src/extract/mlinterp.cmx: OFLAGS += -ppx $(PPX_DEBUG_OPTIM_EXE)
|
|
|
|
clean::
|
|
rm -f src/util/ppx_debug_optim$(EXE)
|
|
endif
|
|
|
|
# Re
|
|
|
|
ifeq (@enable_re@,no)
|
|
src/util/re.ml: src/util/recompat.ml Makefile
|
|
$(CMP_CP)
|
|
LIBGENERATED += src/util/re.ml
|
|
endif
|
|
GENERATED += src/util/re.ml
|
|
|
|
# build targets
|
|
|
|
byte: lib/why3/why3.cma
|
|
opt: lib/why3/why3.cmxa lib/why3/why3.cmxs
|
|
|
|
lib/why3/why3.cma: lib/why3/why3.cmo
|
|
lib/why3/why3.cmxa: lib/why3/why3.cmx
|
|
lib/why3/why3.cmxs: lib/why3/why3.cmx
|
|
|
|
lib/why3/why3.cmo: $(LIBCMO)
|
|
$(SHOW) 'Linking $@'
|
|
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
|
|
|
|
lib/why3/why3.cmx: $(LIBCMX) lib/why3/why3.cmo
|
|
$(SHOW) 'Linking $@'
|
|
$(HIDE)$(OCAMLOPT) $(OFLAGS) $(CMIHACK) -pack -o $@ $(filter %.cmx, $^)
|
|
|
|
# clean and depend
|
|
|
|
MAKEINC += $(LIBDEP)
|
|
|
|
CLEANDIRS += src $(addprefix src/, $(LIBDIRS))
|
|
CLEANLIBS += lib/why3/why3
|
|
GENERATED += $(LIBGENERATED)
|
|
|
|
###############
|
|
# installation
|
|
###############
|
|
|
|
uninstall-data::
|
|
rm -rf $(DATADIR)/why3
|
|
|
|
install-data::
|
|
$(MKDIR_P) $(DATADIR)/why3
|
|
$(MKDIR_P) $(DATADIR)/why3/vim
|
|
$(MKDIR_P) $(DATADIR)/why3/vim/ftdetect
|
|
$(MKDIR_P) $(DATADIR)/why3/vim/syntax
|
|
$(MKDIR_P) $(DATADIR)/why3/lang
|
|
$(MKDIR_P) $(DATADIR)/why3/stdlib
|
|
$(MKDIR_P) $(DATADIR)/why3/stdlib/mach
|
|
$(MKDIR_P) $(DATADIR)/why3/stdlib/mach/java
|
|
$(MKDIR_P) $(DATADIR)/why3/drivers
|
|
$(MKDIR_P) $(DATADIR)/why3/extraction_drivers
|
|
$(INSTALL_DATA) stdlib/*.mlw $(DATADIR)/why3/stdlib
|
|
$(INSTALL_DATA) stdlib/mach/*.mlw $(DATADIR)/why3/stdlib/mach
|
|
$(INSTALL_DATA) stdlib/mach/java/*.mlw $(DATADIR)/why3/stdlib/mach/java
|
|
$(INSTALL_DATA) drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
|
|
$(INSTALL_DATA) extraction_drivers/*.drv $(DATADIR)/why3/extraction_drivers
|
|
$(INSTALL_DATA) LICENSE $(DATADIR)/why3/
|
|
$(INSTALL_DATA) share/provers-detection-data.conf $(DATADIR)/why3/
|
|
$(INSTALL_DATA) share/why3session.dtd $(DATADIR)/why3
|
|
$(INSTALL_DATA) share/Makefile.config $(DATADIR)/why3
|
|
$(INSTALL_DATA) share/vim/ftdetect/why3.vim $(DATADIR)/why3/vim/ftdetect/why3.vim
|
|
$(INSTALL_DATA) share/vim/syntax/why3.vim $(DATADIR)/why3/vim/syntax/why3.vim
|
|
$(INSTALL_DATA) share/lang/why3.lang $(DATADIR)/why3/lang/why3.lang
|
|
$(INSTALL_DATA) share/lang/why3c.lang $(DATADIR)/why3/lang/why3c.lang
|
|
$(INSTALL_DATA) share/lang/why3py.lang $(DATADIR)/why3/lang/why3py.lang
|
|
$(INSTALL_DATA) share/lang/coma.lang $(DATADIR)/why3/lang/coma.lang
|
|
|
|
ifeq (@enable_local@,yes)
|
|
else
|
|
install:: install-bin install-data
|
|
|
|
uninstall:: uninstall-bin uninstall-data
|
|
rm -rf $(LIBDIR)/why3
|
|
endif
|
|
|
|
uninstall-lib:
|
|
if test -d $(OCAMLINSTALLLIB) -a -w $(OCAMLINSTALLLIB); then \
|
|
rm -rf $(OCAMLINSTALLLIB)/why3; \
|
|
fi
|
|
|
|
uninstall:: uninstall-lib
|
|
|
|
install-lib::
|
|
$(MKDIR_P) $(OCAMLINSTALLLIB)/why3
|
|
$(INSTALL_DATA) $(wildcard $(addprefix lib/why3/why3., $(INSTALLED_LIB_EXTS))) \
|
|
lib/why3/META $(OCAMLINSTALLLIB)/why3
|
|
|
|
##################
|
|
# Why3 emacs mode
|
|
##################
|
|
|
|
%.elc: %.el
|
|
$(EMACS) --batch --no-init-file -f batch-byte-compile $<
|
|
|
|
clean::
|
|
rm -f share/emacs/why3.elc
|
|
|
|
uninstall-emacs:
|
|
rm -f $(DATADIR)/emacs/site-lisp/why3.el
|
|
rm -f $(DATADIR)/emacs/site-lisp/why3.elc
|
|
|
|
uninstall:: uninstall-emacs
|
|
|
|
install-emacs:
|
|
$(MKDIR_P) $(DATADIR)/emacs/site-lisp/
|
|
$(INSTALL_DATA) share/emacs/why3.el $(DATADIR)/emacs/site-lisp/why3.el
|
|
ifeq (@enable_emacs_compilation@,yes)
|
|
$(INSTALL_DATA) share/emacs/why3.elc $(DATADIR)/emacs/site-lisp/why3.elc
|
|
endif
|
|
|
|
install:: install-emacs
|
|
|
|
ifeq (@enable_emacs_compilation@,yes)
|
|
all: share/emacs/why3.elc
|
|
endif
|
|
|
|
|
|
##################
|
|
# Why3 plugins
|
|
##################
|
|
|
|
PLUGGENERATED = \
|
|
plugins/tptp/tptp_lexer.ml \
|
|
plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli \
|
|
plugins/coma/coma_lexer.ml \
|
|
plugins/coma/coma_parser.ml plugins/coma/coma_parser.mli \
|
|
plugins/python/py_lexer.ml \
|
|
plugins/python/py_parser.ml plugins/python/py_parser.mli \
|
|
plugins/microc/mc_lexer.ml \
|
|
plugins/microc/mc_parser.ml plugins/microc/mc_parser.mli \
|
|
plugins/cfg/cfg_lexer.ml \
|
|
plugins/cfg/cfg_parser.ml plugins/cfg/cfg_parser.mli \
|
|
plugins/parser/dimacs.ml \
|
|
plugins/ada_terms/ada_lexer.ml \
|
|
plugins/ada_terms/ada_parser.ml plugins/ada_terms/ada_parser.mli
|
|
|
|
PLUG_PARSER = genequlin dimacs
|
|
PLUG_PRINTER =
|
|
PLUG_TRANSFORM =
|
|
PLUG_TPTP = tptp_parser tptp_typing tptp_lexer tptp_printer
|
|
PLUG_COMA = coma_logic coma_syntax coma_parser coma_lexer coma_typing coma_main
|
|
PLUG_PYTHON = py_parser py_lexer py_main
|
|
PLUG_MICROC = mc_parser mc_lexer mc_printer mc_main
|
|
PLUG_CFG = cfg_parser cfg_lexer cfg_paths subregion_analysis cfg_main
|
|
ifeq (@enable_stackify@,yes)
|
|
PLUG_CFG += stackify cfg_stackify
|
|
endif
|
|
PLUG_ADA = ada_nametable ada_parser ada_lexer ada_main
|
|
|
|
PLUG_CMIONLY = tptp/tptp_ast python/py_ast microc/mc_ast cfg/cfg_ast
|
|
|
|
PLUGINS = genequlin dimacs tptp python microc coma cfg forward_propagation ada_terms gnat_json
|
|
|
|
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
|
|
COMAMODULES = $(addprefix plugins/coma/, $(PLUG_COMA))
|
|
PYTHONMODULES = $(addprefix plugins/python/, $(PLUG_PYTHON))
|
|
MICROCMODULES = $(addprefix plugins/microc/, $(PLUG_MICROC))
|
|
CFGMODULES = $(addprefix plugins/cfg/, $(PLUG_CFG))
|
|
ADAMODULES = $(addprefix plugins/ada_terms/, $(PLUG_ADA))
|
|
GNATJSONMODULES := $(addprefix plugins/gnat_json/, ptree_constructors gnat_ast gnat_ast_pretty gnat_ast_to_ptree)
|
|
|
|
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
|
|
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
|
|
|
|
COMACMO = $(addsuffix .cmo, $(COMAMODULES))
|
|
COMACMX = $(addsuffix .cmx, $(COMAMODULES))
|
|
|
|
PYTHONCMO = $(addsuffix .cmo, $(PYTHONMODULES))
|
|
PYTHONCMX = $(addsuffix .cmx, $(PYTHONMODULES))
|
|
|
|
MICROCCMO = $(addsuffix .cmo, $(MICROCMODULES))
|
|
MICROCCMX = $(addsuffix .cmx, $(MICROCMODULES))
|
|
|
|
ADACMO = $(addsuffix .cmo, $(ADAMODULES))
|
|
ADACMX = $(addsuffix .cmx, $(ADAMODULES))
|
|
|
|
GNATJSONCMO = $(addsuffix .cmo, $(GNATJSONMODULES))
|
|
GNATJSONCMX = $(addsuffix .cmx, $(GNATJSONMODULES))
|
|
|
|
ifeq (@enable_hypothesis_selection@,yes)
|
|
PLUG_TRANSFORM += hypothesis_selection
|
|
PLUGINS += hypothesis_selection
|
|
|
|
lib/plugins/hypothesis_selection.cmxs: EXTINCLUDES += -I @OCAMLGRAPHLIB@
|
|
lib/plugins/hypothesis_selection.cma: EXTINCLUDES += -I @OCAMLGRAPHLIB@
|
|
lib/plugins/hypothesis_selection.cmxs: EXTLIBS += graph.cmxa
|
|
lib/plugins/hypothesis_selection.cma: EXTOBJS += graph.cma
|
|
ifeq (@enable_ocamlfind@,yes)
|
|
lib/plugins/hypothesis_selection.cmxs: FLAGS += -package ocamlgraph -dontlink "$(EXTPKGS)" -linkpkg
|
|
lib/plugins/hypothesis_selection.cma: FLAGS += -package ocamlgraph -dontlink "$(EXTPKGS)" -linkpkg
|
|
endif
|
|
endif
|
|
|
|
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
|
|
$(addprefix plugins/printer/, $(PLUG_PRINTER)) \
|
|
$(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
|
|
$(TPTPMODULES) $(COMAMODULES) \
|
|
$(PYTHONMODULES) $(MICROCMODULES) $(CFGMODULES) \
|
|
$(ADAMODULES) $(GNATJSONMODULES)
|
|
|
|
PLUGDEP = $(addsuffix .dep, $(PLUGMODULES)) $(PLUG_CMIONLY:%=plugins/%.dep)
|
|
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
|
|
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
|
|
PLUGCMI = $(addsuffix .cmi, $(PLUGMODULES)) $(PLUG_CMIONLY:%=plugins/%.cmi)
|
|
|
|
PLUGDIRS = parser printer transform strategies tptp coma python microc cfg ada_terms gnat_json
|
|
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))
|
|
|
|
ifeq (@enable_stackify@,yes)
|
|
plugins/cfg/stackify.cmx: EXTINCLUDES += -I @OCAMLGRAPHLIB@
|
|
plugins/cfg/stackify.cmo: EXTINCLUDES += -I @OCAMLGRAPHLIB@
|
|
plugins/cfg/stackify.cmx: EXTLIBS += graph.cmxa
|
|
plugins/cfg/stackify.cmo: EXTOBJS += graph.cma
|
|
ifeq (@enable_ocamlfind@,yes)
|
|
plugins/cfg/stackify.cmx: FLAGS += -package ocamlgraph
|
|
plugins/cfg/stackify.cmo: FLAGS += -package ocamlgraph
|
|
lib/plugins/cfg.cmxs: FLAGS += -package ocamlgraph -dontlink "$(EXTPKGS)" -linkpkg
|
|
lib/plugins/cfg.cma: FLAGS += -package ocamlgraph -dontlink "$(EXTPKGS)" -linkpkg
|
|
endif
|
|
endif
|
|
|
|
$(PLUGDEP) $(PLUGCMO) $(PLUGCMX) $(PLUGCMI): INCLUDES += $(PLUGINCLUDES)
|
|
|
|
$(PLUGDEP): $(PLUGGENERATED)
|
|
|
|
LIBPLUGCMA = $(PLUGINS:%=lib/plugins/%.cma)
|
|
LIBPLUGCMXS = $(PLUGINS:%=lib/plugins/%.cmxs)
|
|
|
|
plugins.byte: $(LIBPLUGCMA)
|
|
plugins.opt : $(LIBPLUGCMXS)
|
|
|
|
lib/plugins:
|
|
mkdir lib/plugins
|
|
|
|
lib/plugins/%.cmxs: | lib/plugins
|
|
$(SHOW) 'Linking $@'
|
|
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
|
|
|
|
lib/plugins/%.cma: | lib/plugins
|
|
$(SHOW) 'Linking $@'
|
|
$(HIDE)$(OCAMLC) $(BFLAGS) -a -o $@ $^
|
|
|
|
$(PLUG_PARSER:%=lib/plugins/%.cmxs): lib/plugins/%.cmxs: plugins/parser/%.cmx
|
|
$(PLUG_PARSER:%=lib/plugins/%.cma): lib/plugins/%.cma: plugins/parser/%.cmo
|
|
$(PLUG_PRINTER:%=lib/plugins/%.cmxs): lib/plugins/%.cmxs: plugins/printer/%.cmx
|
|
$(PLUG_PRINTER:%=lib/plugins/%.cma): lib/plugins/%.cma: plugins/printer/%.cmo
|
|
$(PLUG_TRANSFORM:%=lib/plugins/%.cmxs): lib/plugins/%.cmxs: plugins/transform/%.cmx
|
|
$(PLUG_TRANSFORM:%=lib/plugins/%.cma): lib/plugins/%.cma: plugins/transform/%.cmo
|
|
lib/plugins/tptp.cmxs: $(TPTPCMX)
|
|
lib/plugins/tptp.cma: $(TPTPCMO)
|
|
lib/plugins/coma.cmxs: $(COMACMX)
|
|
lib/plugins/coma.cma: $(COMACMO)
|
|
lib/plugins/python.cmxs: $(PYTHONCMX)
|
|
lib/plugins/python.cma: $(PYTHONCMO)
|
|
lib/plugins/microc.cmxs: $(MICROCCMX)
|
|
lib/plugins/microc.cma: $(MICROCCMO)
|
|
lib/plugins/cfg.cmxs: $(addsuffix .cmx, $(CFGMODULES))
|
|
lib/plugins/cfg.cma: $(addsuffix .cmo, $(CFGMODULES))
|
|
lib/plugins/ada_terms.cmxs: $(ADACMX)
|
|
lib/plugins/ada_terms.cmo: $(ADACMO)
|
|
lib/plugins/gnat_json.cmxs: $(GNATJSONCMX)
|
|
lib/plugins/gnat_json.cmo: $(GNATJSONCMO)
|
|
|
|
# depend and clean targets
|
|
|
|
MAKEINC += $(PLUGDEP)
|
|
|
|
CLEANDIRS += plugins $(addprefix plugins/, $(PLUGDIRS)) lib/plugins
|
|
GENERATED += $(PLUGGENERATED)
|
|
|
|
uninstall-bin::
|
|
rm -f $(PLUGINS:%=$(LIBDIR)/why3/plugins/%.cma)
|
|
rm -f $(PLUGINS:%=$(LIBDIR)/why3/plugins/%.cmxs)
|
|
|
|
install-bin::
|
|
$(MKDIR_P) $(LIBDIR)/why3/plugins
|
|
$(INSTALL_DATA) $(wildcard $(LIBPLUGCMA) $(LIBPLUGCMXS)) $(LIBDIR)/why3/plugins
|
|
|
|
###############
|
|
# Why3 commands
|
|
###############
|
|
|
|
TOOLSGENERATED = src/tools/why3wc.ml
|
|
|
|
TOOLS_BIN = \
|
|
why3config why3execute why3extract why3prove \
|
|
why3realize why3replay why3show why3wc why3bench
|
|
|
|
TOOLS_FILES = main $(TOOLS_BIN)
|
|
|
|
TOOLSMODULES = $(addprefix src/tools/, $(TOOLS_FILES))
|
|
|
|
TOOLSDEP = $(addsuffix .dep, $(TOOLSMODULES))
|
|
TOOLSCMO = $(addsuffix .cmo, $(TOOLSMODULES))
|
|
TOOLSCMX = $(addsuffix .cmx, $(TOOLSMODULES))
|
|
|
|
$(TOOLSDEP) $(TOOLSCMO) $(TOOLSCMX): INCLUDES += -I src/tools
|
|
|
|
$(TOOLSDEP): $(TOOLSGENERATED)
|
|
|
|
byte: bin/why3.byte $(TOOLS_BIN:%=bin/%.cma)
|
|
opt: bin/why3.opt $(TOOLS_BIN:%=bin/%.cmxs)
|
|
|
|
bin/why3.opt: $(WHY3CMXA) src/tools/main.cmx
|
|
bin/why3.byte: $(WHY3CMA) src/tools/main.cmo
|
|
|
|
$(TOOLS_BIN:%=bin/%.cma): bin/%.cma: src/tools/%.cmo
|
|
$(TOOLS_BIN:%=bin/%.cmxs): bin/%.cmxs: src/tools/%.cmx
|
|
|
|
uninstall-bin::
|
|
rm -f $(BINDIR)/why3$(EXE)
|
|
rm -f $(TOOLS_BIN:%=bin/%.$(SHAREDBEST))
|
|
|
|
install-bin::
|
|
$(MKDIR_P) $(BINDIR)
|
|
$(INSTALL) bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
|
|
$(MKDIR_P) $(TOOLDIR)
|
|
$(INSTALL_DATA) $(TOOLS_BIN:%=bin/%.$(SHAREDBEST)) $(TOOLDIR)
|
|
|
|
install_local:: bin/why3$(EXE) $(TOOLS_BIN:%=bin/%.$(SHAREDBEST))
|
|
|
|
install_local:: share/drivers share/extraction_drivers share/stdlib
|
|
|
|
ifneq (@OCAML_OS_TYPE@,Win32)
|
|
bin/why3$(EXE): bin/why3.@OCAMLBEST@
|
|
ln -sf $(notdir $<) $@
|
|
|
|
share/drivers share/extraction_drivers share/stdlib: share/%:
|
|
ln -snf ../$* $@
|
|
else
|
|
# On Windows with --enable-local, why3 does not find the files inside of
|
|
# symbolic link folders. Make copies instead, and since this is not a link
|
|
# anymore, make the copies every time the compilation is run.
|
|
|
|
.PHONY: share/drivers share/extraction_drivers share/stdlib
|
|
|
|
bin/why3$(EXE): bin/why3.@OCAMLBEST@
|
|
cp $< $@
|
|
|
|
share/drivers share/extraction_drivers share/stdlib: share/%:
|
|
cp -r $* share/
|
|
|
|
ifeq (@enable_local@,yes)
|
|
clean::
|
|
rm -rf share/drivers
|
|
rm -rf share/extraction_drivers
|
|
rm -rf share/stdlib
|
|
endif
|
|
endif
|
|
|
|
MAKEINC += $(TOOLSDEP)
|
|
|
|
CLEANDIRS += src/tools
|
|
GENERATED += $(TOOLSGENERATED)
|
|
|
|
clean::
|
|
rm -f bin/why3*
|
|
|
|
############
|
|
# GNATWhy3 #
|
|
############
|
|
|
|
GNATWHY3_FILES := gnat_util gnat_loc gnat_expl gnat_counterexamples gnat_config\
|
|
gnat_scheduler gnat_manual gnat_report gnat_checks gnat_main
|
|
|
|
GNATWHY3MODULES := $(addprefix src/gnat/, $(GNATWHY3_FILES))
|
|
GNATWHY3DEP = $(addsuffix .dep, $(GNATWHY3MODULES))
|
|
GNATWHY3CMO = $(addsuffix .cmo, $(GNATWHY3MODULES))
|
|
# Import external printer parser for Ada
|
|
GNATWHY3CMX = $(addsuffix .cmx, $(GNATWHY3MODULES))
|
|
$(GNATWHY3CMO) $(GNATWHY3CMX): INCLUDES += -I src/util -I src/gnat
|
|
$(GNATWHY3DEP): DEPFLAGS += -I src/util -I src/gnat
|
|
|
|
# build targets
|
|
|
|
byte: bin/gnatwhy3.byte
|
|
opt: bin/gnatwhy3.opt
|
|
|
|
bin/gnatwhy3.opt: lib/why3/why3.cmxa $(GNATWHY3CMX)
|
|
bin/gnatwhy3.byte: lib/why3/why3.cma $(GNATWHY3CMO)
|
|
|
|
install_no_local::
|
|
cp -f bin/gnatwhy3.@OCAMLBEST@ $(BINDIR)/gnatwhy3$(EXE)
|
|
|
|
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
|
|
-include $(GNATWHY3DEP)
|
|
endif
|
|
|
|
CLEANDIRS += src/gnat
|
|
|
|
clean::
|
|
rm -f bin/gnatwhy3.byte bin/gnatwhy3.opt bin/gnatwhy3
|
|
|
|
##############
|
|
# Why3server #
|
|
##############
|
|
|
|
SERVER_MODULES := logging arraylist options queue readbuf request \
|
|
proc writebuf server-unix server-win
|
|
|
|
CPULIM_MODULES := cpulimit-unix cpulimit-win
|
|
|
|
SERVER_O := $(SERVER_MODULES:%=src/server/%.o)
|
|
|
|
CPULIM_O := $(CPULIM_MODULES:%=src/server/%.o)
|
|
|
|
TOOLS = lib/why3server$(EXE) lib/why3cpulimit$(EXE)
|
|
|
|
all: $(TOOLS)
|
|
|
|
lib/why3server$(EXE): $(SERVER_O)
|
|
$(CC) -Wall -o $@ $^
|
|
|
|
lib/why3cpulimit$(EXE): $(CPULIM_O)
|
|
$(CC) -Wall -o $@ $^
|
|
|
|
%.o: %.c
|
|
$(CC) -Wall -O -g -o $@ -c $<
|
|
|
|
uninstall-bin::
|
|
rm -f $(LIBDIR)/why3/why3server$(EXE) $(LIBDIR)/why3/why3cpulimit$(EXE)
|
|
rm -f $(LIBDIR)/why3/why3-call-pvs
|
|
|
|
install-bin::
|
|
$(MKDIR_P) $(LIBDIR)/why3
|
|
$(INSTALL) lib/why3server$(EXE) $(LIBDIR)/why3/why3server$(EXE)
|
|
$(INSTALL) lib/why3cpulimit$(EXE) $(LIBDIR)/why3/why3cpulimit$(EXE)
|
|
$(INSTALL) lib/why3-call-pvs $(LIBDIR)/why3/why3-call-pvs
|
|
|
|
clean::
|
|
rm -f $(SERVER_O) $(CPULIM_O) $(TOOLS)
|
|
|
|
.PHONY: install_spark2014 install_spark2014_dev
|
|
|
|
install_spark2014_dev: install_spark2014
|
|
$(MKDIR_P) $(DATADIR)/why3/images
|
|
for i in share/images/*.rc; do \
|
|
d=`basename $$i .rc`; \
|
|
$(INSTALL_DATA) $$i $(DATADIR)/why3/images; \
|
|
$(MKDIR_P) $(DATADIR)/why3/images/$$d; \
|
|
$(INSTALL_DATA) share/images/$$d/* $(DATADIR)/why3/images/$$d; \
|
|
done
|
|
$(INSTALL_DATA) share/images/*.png $(DATADIR)/why3/images
|
|
$(MKDIR_P) $(DATADIR)/why3/lang
|
|
# Install all Why3 tools
|
|
for f in bin/why3*.@OCAMLBEST@; do install -C "$$f" $(BINDIR)/"$$(basename "$$f" .@OCAMLBEST@)$(EXE)"; done
|
|
# Install lang files for Why3 IDE
|
|
for f in share/lang/*.lang; do $(INSTALL_DATA) "$$f" "$(DATADIR)/why3/lang/$$(basename $$f)"; done
|
|
|
|
install_spark2014: install-bin
|
|
mkdir -p $(BINDIR)
|
|
mkdir -p $(DATADIR)/why3
|
|
mkdir -p $(DATADIR)/why3/theories
|
|
mkdir -p $(DATADIR)/why3/drivers
|
|
mkdir -p $(DATADIR)/why3/libs
|
|
cp -rf stdlib/* $(DATADIR)/why3/theories
|
|
cp -f drivers/*.drv drivers/*.gen drivers/*.aux $(DATADIR)/why3/drivers
|
|
# also copy the fixed coq-realizations.aux file that we use for SPARK;
|
|
# This will possibly overwrite the one that was copied on the line
|
|
# before
|
|
cp -f coq-realizations.aux $(DATADIR)/why3/drivers
|
|
cp -f share/why3session.dtd $(DATADIR)/why3
|
|
cp -f lib/why3server$(EXE) $(BINDIR)/why3server$(EXE)
|
|
cp -f lib/why3cpulimit$(EXE) $(BINDIR)/why3cpulimit$(EXE)
|
|
cp -f bin/gnatwhy3.$(OCAMLBEST) $(BINDIR)/gnatwhy3$(EXE)
|
|
cp -f bin/why3.$(OCAMLBEST) $(BINDIR)/why3$(EXE)
|
|
cp -f bin/why3realize.$(SHAREDBEST) $(BINDIR)/
|
|
cp -f bin/why3config.$(SHAREDBEST) $(BINDIR)/
|
|
cp -f bin/why3session.$(SHAREDBEST) $(BINDIR)/
|
|
cp -f share/provers-detection-data.conf $(DATADIR)/why3/
|
|
# copying why3ide is optional, so this line is allowed to fail
|
|
-cp -f bin/why3ide.$(SHAREDBEST) $(BINDIR)/
|
|
cp -rf lib/coq $(DATADIR)/why3/libs
|
|
|
|
##########
|
|
# gallery
|
|
##########
|
|
|
|
# we export exactly the programs that have a why3session.xml file
|
|
|
|
.PHONY: gallery gallery-simple gallery-subs
|
|
|
|
gallery: gallery-simple gallery-subs
|
|
|
|
gallery-simple:
|
|
@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
|
|
@cd examples/; \
|
|
for x in `git ls-files */why3session.xml` ; do \
|
|
f=`dirname $$x`; \
|
|
if echo $$f | grep -q -e '\(_vc_sp\|^bignum\)$$'; then continue; fi; \
|
|
echo "exporting $$f"; \
|
|
mkdir -p $(GALLERYDIR)/$$f; \
|
|
WHY3CONFIG="" ../bin/why3.@OCAMLBEST@ session html $$x -o $(GALLERYDIR)/$$f; \
|
|
cp $$f.mlw $(GALLERYDIR)/$$f/; \
|
|
rm -f $(GALLERYDIR)/$$f/$$f.zip; \
|
|
git archive --format=zip -o $(GALLERYDIR)/$$f/$$f.zip HEAD $$f.mlw $$f; \
|
|
done
|
|
|
|
GALLERYSUBS=WP_revisited verifythis_2016_matrix_multiplication avl double_wp prover multiprecision
|
|
|
|
gallery-subs:
|
|
@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
|
|
@for d in $(GALLERYSUBS) ; do \
|
|
echo "exporting examples/$$d"; \
|
|
mkdir -p $(GALLERYDIR)/$$d; \
|
|
cd examples/$$d; \
|
|
WHY3CONFIG="" ../../bin/why3.@OCAMLBEST@ doc --no-stdlib --no-load-default-plugins -L ../../stdlib -L . --stdlib-url https://www.why3.org/stdlib/ --warn-off=unused_variable *.mlw -o $(GALLERYDIR)/$$d; \
|
|
cd ..; \
|
|
rm -f $(GALLERYDIR)/$$d/$$d.zip; \
|
|
git archive --format=zip -o $(GALLERYDIR)/$$d/$$d.zip HEAD $$d; \
|
|
cd ..; \
|
|
done
|
|
|
|
########
|
|
# XML DTD validation
|
|
########
|
|
|
|
.PHONY: xml-validate xml-validate-local
|
|
|
|
xml-validate:
|
|
@for x in `find examples/ -name why3session.xml`; do \
|
|
xmllint --noout --valid $$x 2>&1 | head -1; \
|
|
done
|
|
|
|
xml-validate-local:
|
|
@for x in `find examples/ -name why3session.xml -print`; do \
|
|
xmllint --nonet --noout --path share --valid $$x 2>&1 | sed -e '/I.O error/d' | head -1; \
|
|
done
|
|
|
|
###############
|
|
# IDE
|
|
###############
|
|
|
|
IDEGENERATED =
|
|
GENERATED += $(IDEGENERATED)
|
|
|
|
ifeq (@enable_ide@,yes)
|
|
|
|
IDE_FILES =
|
|
|
|
ifeq (@enable_statmemprof@,yes)
|
|
IDE_FILES += statmemprof
|
|
|
|
bin/why3ide.cmxs bin/why3ide.cma: EXTPKGS += @STATMEMPROFPKG@
|
|
endif
|
|
|
|
IDE_FILES += gconfig ide_utils why3ide
|
|
|
|
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
|
|
|
|
IDEDEP = $(addsuffix .dep, $(IDEMODULES))
|
|
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
|
|
IDECMX = $(addsuffix .cmx, $(IDEMODULES))
|
|
|
|
$(IDEDEP) $(IDECMO) $(IDECMX): INCLUDES += -I src/ide
|
|
|
|
$(IDEDEP): $(IDEGENERATED)
|
|
|
|
# build targets
|
|
|
|
byte: bin/why3ide.cma
|
|
opt: bin/why3ide.cmxs
|
|
|
|
bin/why3ide.cmxs bin/why3ide.cma: FLAGS += $(addprefix -package ,@LABLGTKPKG@) -dontlink "$(EXTPKGS)" -linkpkg
|
|
|
|
bin/why3ide.cmxs: $(IDECMX)
|
|
bin/why3ide.cma: $(IDECMO)
|
|
|
|
# depend and clean targets
|
|
|
|
MAKEINC += $(IDEDEP)
|
|
|
|
CLEANDIRS += src/ide
|
|
|
|
ide: bin/why3ide.$(SHAREDBEST)
|
|
|
|
uninstall-ide:
|
|
rm -f $(TOOLDIR)/why3ide.$(SHAREDBEST)
|
|
rm -rf $(DATADIR)/why3/images
|
|
|
|
uninstall:: uninstall-ide
|
|
|
|
install-ide:
|
|
$(MKDIR_P) $(TOOLDIR)
|
|
$(INSTALL_DATA) bin/why3ide.$(SHAREDBEST) $(TOOLDIR)
|
|
$(MKDIR_P) $(DATADIR)/why3/images
|
|
for i in share/images/*.rc; do \
|
|
d=`basename $$i .rc`; \
|
|
$(INSTALL_DATA) $$i $(DATADIR)/why3/images; \
|
|
$(MKDIR_P) $(DATADIR)/why3/images/$$d; \
|
|
$(INSTALL_DATA) share/images/$$d/* $(DATADIR)/why3/images/$$d; \
|
|
done
|
|
$(INSTALL_DATA) share/images/*.png $(DATADIR)/why3/images
|
|
|
|
install:: install-ide
|
|
|
|
install_local:: bin/why3ide.$(SHAREDBEST)
|
|
|
|
endif
|
|
|
|
###############
|
|
# WEBSERV
|
|
###############
|
|
|
|
WEBSERV_FILES = wserver why3web
|
|
|
|
WEBSERVMODULES = $(addprefix src/ide/, $(WEBSERV_FILES))
|
|
|
|
WEBSERVDEP = $(addsuffix .dep, $(WEBSERVMODULES))
|
|
WEBSERVCMO = $(addsuffix .cmo, $(WEBSERVMODULES))
|
|
WEBSERVCMX = $(addsuffix .cmx, $(WEBSERVMODULES))
|
|
|
|
$(WEBSERVDEP) $(WEBSERVCMO) $(WEBSERVCMX): INCLUDES += -I src/ide
|
|
|
|
# build targets
|
|
|
|
byte: bin/why3webserver.cma
|
|
opt: bin/why3webserver.cmxs
|
|
|
|
bin/why3webserver.cmxs: $(WEBSERVCMX)
|
|
bin/why3webserver.cma: $(WEBSERVCMO)
|
|
|
|
# depend and clean targets
|
|
|
|
MAKEINC += $(WEBSERVDEP)
|
|
|
|
CLEANDIRS += src/ide
|
|
|
|
uninstall-bin::
|
|
rm -f $(TOOLDIR)/why3webserver.$(SHAREDBEST)
|
|
|
|
install-bin::
|
|
$(MKDIR_P) $(TOOLDIR)
|
|
$(INSTALL_DATA) bin/why3webserver.$(SHAREDBEST) $(TOOLDIR)
|
|
|
|
install_local:: bin/why3webserver.$(SHAREDBEST)
|
|
|
|
|
|
###############
|
|
# Session
|
|
###############
|
|
|
|
SESSION_FILES = why3session_lib why3session_info \
|
|
why3session_html why3session_latex why3session_update \
|
|
why3session_output why3session_create why3session_main
|
|
# TODO: why3session_copy why3session_rm why3session_csv why3session_run
|
|
# why3session_output
|
|
|
|
SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
|
|
|
|
SESSIONDEP = $(addsuffix .dep, $(GNATASTMODULES) $(SESSIONMODULES))
|
|
SESSIONCMO = $(addsuffix .cmo, $(GNATASTMODULES) $(SESSIONMODULES))
|
|
SESSIONCMX = $(addsuffix .cmx, $(GNATASTMODULES) $(SESSIONMODULES))
|
|
|
|
$(SESSIONDEP) $(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session
|
|
|
|
# build targets
|
|
|
|
byte: bin/why3session.cma
|
|
opt: bin/why3session.cmxs
|
|
|
|
bin/why3session.cmxs: $(SESSIONCMX)
|
|
bin/why3session.cma: $(SESSIONCMO)
|
|
|
|
# depend and clean targets
|
|
|
|
MAKEINC += $(SESSIONDEP)
|
|
|
|
CLEANDIRS += src/why3session
|
|
|
|
uninstall-bin::
|
|
rm -f $(TOOLDIR)/why3session.$(SHAREDBEST)
|
|
|
|
install-bin::
|
|
$(MKDIR_P) $(TOOLDIR)
|
|
$(INSTALL_DATA) bin/why3session.$(SHAREDBEST) $(TOOLDIR)
|
|
|
|
install_local:: bin/why3session.$(SHAREDBEST)
|
|
|
|
###############
|
|
# Why3 Shell
|
|
###############
|
|
|
|
SHELL_FILES = why3shell
|
|
|
|
SHELLMODULES = $(addprefix src/tools/, $(SHELL_FILES))
|
|
|
|
SHELLDEP = $(addsuffix .dep, $(SHELLMODULES))
|
|
SHELLCMO = $(addsuffix .cmo, $(SHELLMODULES))
|
|
SHELLCMX = $(addsuffix .cmx, $(SHELLMODULES))
|
|
|
|
$(SHELLDEP) $(SHELLCMO) $(SHELLCMX): INCLUDES += -I src/tools
|
|
|
|
# build targets
|
|
|
|
byte: bin/why3shell.cma
|
|
opt: bin/why3shell.cmxs
|
|
|
|
bin/why3shell.cmxs: $(SHELLCMX)
|
|
bin/why3shell.cma: $(SHELLCMO)
|
|
|
|
# depend and clean targets
|
|
|
|
MAKEINC += $(SHELLDEP)
|
|
|
|
uninstall-bin::
|
|
rm -f $(TOOLDIR)/why3shell.$(SHAREDBEST)
|
|
|
|
install-bin::
|
|
$(MKDIR_P) $(TOOLDIR)
|
|
$(INSTALL_DATA) bin/why3shell.$(SHAREDBEST) $(TOOLDIR)
|
|
|
|
install_local:: bin/why3shell.$(SHAREDBEST)
|
|
|
|
####################
|
|
# Coq realizations
|
|
####################
|
|
|
|
COQVERSIONSPECIFIC=
|
|
|
|
COQVERSIONSPECIFICTARGETS=$(addprefix lib/coq/, $(COQVERSIONSPECIFIC))
|
|
|
|
$(COQVERSIONSPECIFICTARGETS): %: %.@coq_compat_version@
|
|
$(CMP_CP)
|
|
|
|
clean-coq::
|
|
rm -f $(COQVERSIONSPECIFICTARGETS)
|
|
|
|
COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power NumOf
|
|
COQLIBS_INT_ALL_FILES = Exponentiation $(COQLIBS_INT_FILES)
|
|
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES))
|
|
|
|
COQLIBS_BOOL_FILES = Bool
|
|
COQLIBS_BOOL = $(addprefix lib/coq/bool/, $(COQLIBS_BOOL_FILES))
|
|
|
|
ifeq (@enable_coq_fp_libs@,yes)
|
|
COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt PowerReal Real RealInfix Square Trigonometry Truncate
|
|
else
|
|
COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt PowerReal Real RealInfix Square Trigonometry
|
|
endif
|
|
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
|
|
|
|
COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
|
|
COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
|
|
|
|
COQLIBS_SET_FILES = Set Cardinal Fset FsetInduction FsetInt FsetSum SetApp SetAppInt SetImp SetImpInt
|
|
COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
|
|
|
|
COQLIBS_MAP_FILES = Map Const MapExt Occ MapPermut MapInjection
|
|
COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES))
|
|
|
|
COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt NthNoOpt RevAppend Combine Distinct NumOcc Permut
|
|
COQLIBS_LIST = $(addprefix lib/coq/list/, $(COQLIBS_LIST_FILES))
|
|
|
|
COQLIBS_OPTION_FILES = Option
|
|
COQLIBS_OPTION = $(addprefix lib/coq/option/, $(COQLIBS_OPTION_FILES))
|
|
|
|
COQLIBS_BV_FILES = Pow2int BV_Gen
|
|
COQLIBS_BV = $(addprefix lib/coq/bv/, $(COQLIBS_BV_FILES))
|
|
|
|
ifeq (@enable_coq_fp_libs@,yes)
|
|
COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
|
|
COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
|
|
COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
|
|
|
|
COQLIBS_IEEEFLOAT_FILES = RoundingMode GenericFloat Float32 Float64
|
|
COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES))
|
|
endif
|
|
|
|
COQLIBS_FOR_DRIVERS_FILES = ComputerOfEuclideanDivision
|
|
COQLIBS_FOR_DRIVERS = $(addprefix lib/coq/for_drivers/, $(COQLIBS_FOR_DRIVERS_FILES))
|
|
|
|
COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd lib/coq/WellFounded $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_FP) $(COQLIBS_BV) $(COQLIBS_IEEEFLOAT) $(COQLIBS_FOR_DRIVERS)
|
|
|
|
%.vo: %.v
|
|
$(SHOW) 'Coqc $<'
|
|
$(HIDE)$(COQC) $(COQFLAGS) -R lib/coq Why3 $<
|
|
|
|
%.vd: %.v
|
|
$(SHOW) 'Coqdep $<'
|
|
$(HIDE)$(COQDEP) -R lib/coq Why3 $< $(TOTARGET)
|
|
|
|
COQV = $(addsuffix .v, $(COQLIBS_FILES))
|
|
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
|
|
COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
|
|
|
|
coq: $(COQVO) drivers/coq-realizations.aux lib/coq/version
|
|
|
|
clean-coq::
|
|
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES)) lib/coq/version \
|
|
$(foreach f,$(COQLIBS_FILES),$(dir $f).$(notdir $f).aux)
|
|
|
|
drivers/coq-realizations.aux: Makefile
|
|
$(SHOW) 'Generate $@'
|
|
$(HIDE)(echo "(* generated automatically at compilation time *)"; \
|
|
echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \
|
|
echo 'theory HighOrd meta "realized_theory" "HighOrd", "" end'; \
|
|
echo 'theory WellFounded meta "realized_theory" "WellFounded", "" end'; \
|
|
for f in $(COQLIBS_INT_FILES); do \
|
|
echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
|
|
for f in $(COQLIBS_BOOL_FILES); do \
|
|
echo 'theory bool.'"$$f"' meta "realized_theory" "bool.'"$$f"'", "" end'; done; \
|
|
for f in $(COQLIBS_REAL_FILES); do \
|
|
echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
|
|
for f in $(COQLIBS_NUMBER_FILES); do \
|
|
echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
|
|
for f in $(COQLIBS_SET_FILES); do \
|
|
echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
|
|
for f in $(COQLIBS_MAP_FILES); do \
|
|
echo 'theory map.'"$$f"' meta "realized_theory" "map.'"$$f"'", "" end'; done; \
|
|
for f in $(COQLIBS_LIST_FILES); do \
|
|
echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
|
|
for f in $(COQLIBS_OPTION_FILES); do \
|
|
echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
|
|
for f in $(COQLIBS_BV_FILES); do \
|
|
echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \
|
|
for f in $(COQLIBS_IEEEFLOAT_FILES); do \
|
|
echo 'theory ieee_float.'"$$f"' meta "realized_theory" "ieee_float.'"$$f"'", "" end'; done; \
|
|
for f in $(COQLIBS_FP_FILES); do \
|
|
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
|
|
for f in $(COQLIBS_FOR_DRIVERS_FILES); do \
|
|
echo 'theory for_drivers.'"$$f"' meta "realized_theory" "for_drivers.'"$$f"'", "" end'; done; \
|
|
) > $@
|
|
|
|
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-bv update-coq-ieee_float update-coq-for-drivers
|
|
|
|
LOCAL_STDLIB=-L stdlib --no-stdlib --no-load-default-plugins
|
|
|
|
update-coq-int: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/int.mlw
|
|
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T int.$$f -o $(GENERATED_PREFIX_COQ)/int/; done
|
|
|
|
update-coq-bool: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/bool.mlw
|
|
for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T bool.$$f -o $(GENERATED_PREFIX_COQ)/bool/; done
|
|
|
|
update-coq-real: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/real.mlw
|
|
for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T real.$$f -o $(GENERATED_PREFIX_COQ)/real/; done
|
|
|
|
update-coq-number: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/number.mlw
|
|
for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T number.$$f -o $(GENERATED_PREFIX_COQ)/number/; done
|
|
|
|
update-coq-set: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/set.mlw
|
|
for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T set.$$f -o $(GENERATED_PREFIX_COQ)/set/; done
|
|
|
|
update-coq-map: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/map.mlw
|
|
for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T map.$$f -o $(GENERATED_PREFIX_COQ)/map/; done
|
|
|
|
update-coq-list: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/list.mlw
|
|
for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T list.$$f -o $(GENERATED_PREFIX_COQ)/list/; done
|
|
|
|
update-coq-option: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/option.mlw
|
|
for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T option.$$f -o $(GENERATED_PREFIX_COQ)/option/; done
|
|
|
|
update-coq-bv: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/bv.mlw
|
|
for f in $(COQLIBS_BV_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T bv.$$f -o $(GENERATED_PREFIX_COQ)/bv/; done
|
|
|
|
update-coq-for-drivers: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/for_drivers.mlw
|
|
for f in $(COQLIBS_FOR_DRIVERS_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T for_drivers.$$f -o $(GENERATED_PREFIX_COQ)/for_drivers/; done
|
|
|
|
update-coq-ieee_float: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/ieee_float.mlw
|
|
for f in $(COQLIBS_IEEEFLOAT_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T ieee_float.$$f -o $(GENERATED_PREFIX_COQ)/ieee_float/; done
|
|
|
|
update-coq-fp: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/coq-realizations.aux stdlib/floating_point.mlw
|
|
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D coq-realize -T floating_point.$$f -o $(GENERATED_PREFIX_COQ)/floating_point/; done
|
|
|
|
ifeq (@enable_coq_libs@,yes)
|
|
|
|
uninstall-coq:
|
|
rm -rf $(LIBDIR)/why3/coq
|
|
|
|
install-coq:
|
|
$(MKDIR_P) $(LIBDIR)/why3/coq
|
|
$(INSTALL_DATA) lib/coq/version $(LIBDIR)/why3/coq/
|
|
$(INSTALL_DATA) lib/coq/BuiltIn.vo lib/coq/HighOrd.vo lib/coq/WellFounded.vo $(LIBDIR)/why3/coq/
|
|
$(MKDIR_P) $(LIBDIR)/why3/coq/int
|
|
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/
|
|
$(MKDIR_P) $(LIBDIR)/why3/coq/bool
|
|
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_BOOL)) $(LIBDIR)/why3/coq/bool/
|
|
$(MKDIR_P) $(LIBDIR)/why3/coq/real
|
|
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
|
|
$(MKDIR_P) $(LIBDIR)/why3/coq/number
|
|
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_NUMBER)) $(LIBDIR)/why3/coq/number/
|
|
$(MKDIR_P) $(LIBDIR)/why3/coq/set
|
|
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_SET)) $(LIBDIR)/why3/coq/set/
|
|
$(MKDIR_P) $(LIBDIR)/why3/coq/map
|
|
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_MAP)) $(LIBDIR)/why3/coq/map/
|
|
$(MKDIR_P) $(LIBDIR)/why3/coq/list
|
|
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_LIST)) $(LIBDIR)/why3/coq/list/
|
|
$(MKDIR_P) $(LIBDIR)/why3/coq/option
|
|
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_OPTION)) $(LIBDIR)/why3/coq/option/
|
|
$(MKDIR_P) $(LIBDIR)/why3/coq/bv
|
|
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_BV)) $(LIBDIR)/why3/coq/bv/
|
|
ifeq (@enable_coq_fp_libs@,yes)
|
|
$(MKDIR_P) $(LIBDIR)/why3/coq/floating_point
|
|
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
|
|
$(MKDIR_P) $(LIBDIR)/why3/coq/ieee_float
|
|
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_IEEEFLOAT)) $(LIBDIR)/why3/coq/ieee_float/
|
|
endif
|
|
$(MKDIR_P) $(LIBDIR)/why3/coq/for_drivers
|
|
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_FOR_DRIVERS)) $(LIBDIR)/why3/coq/for_drivers/
|
|
$(MKDIR_P) $(DATADIR)/why3/drivers
|
|
$(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
|
|
|
|
install:: install-coq
|
|
|
|
all: coq
|
|
|
|
ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq"
|
|
MAKEINC += $(COQVD)
|
|
endif
|
|
|
|
endif
|
|
|
|
install-data::
|
|
$(MKDIR_P) $(DATADIR)/why3/drivers
|
|
$(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
|
|
|
|
all: drivers/coq-realizations.aux
|
|
|
|
clean:: clean-coq
|
|
rm -f drivers/coq-realizations.aux
|
|
|
|
####################
|
|
# PVS realizations
|
|
####################
|
|
|
|
PVSLIBS_INT_FILES = Int Abs MinMax ComputerDivision EuclideanDivision
|
|
PVSLIBS_INT = $(addprefix lib/pvs/int/, $(PVSLIBS_INT_FILES))
|
|
|
|
PVSLIBS_REAL_FILES = Abs FromInt MinMax Real Square ExpLog Trigonometry \
|
|
PowerInt
|
|
# RealInfix
|
|
PVSLIBS_REAL = $(addprefix lib/pvs/real/, $(PVSLIBS_REAL_FILES))
|
|
|
|
PVSLIBS_LIST_FILES =
|
|
# Nth
|
|
PVSLIBS_LIST = $(addprefix lib/pvs/int/, $(PVSLIBS_LIST_FILES))
|
|
|
|
PVSLIBS_NUMBER_FILES = # Divisibility Gcd Parity Prime
|
|
PVSLIBS_NUMBER = $(addprefix lib/pvs/number/, $(PVSLIBS_NUMBER_FILES))
|
|
|
|
PVSLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
|
|
PVSLIBS_FP_ALL_FILES = $(PVSLIBS_FP_FILES)
|
|
PVSLIBS_FP = $(addprefix lib/pvs/floating_point/, $(PVSLIBS_FP_ALL_FILES))
|
|
|
|
PVSLIBS_FILES = $(PVSLIBS_INT) $(PVSLIBS_REAL) $(PVSLIBS_LIST) \
|
|
$(PVSLIBS_NUMBER) $(PVSLIBS_FP)
|
|
|
|
update-pvs: bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/pvs-realizations.aux
|
|
for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D pvs-realize -T int.$$f -o lib/pvs/int/; done
|
|
for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D pvs-realize -T real.$$f -o lib/pvs/real/; done
|
|
for f in $(PVSLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D pvs-realize -T list.$$f -o lib/pvs/list/; done
|
|
for f in $(PVSLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D pvs-realize -T number.$$f -o lib/pvs/number/; done
|
|
for f in $(PVSLIBS_FP_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D pvs-realize -T floating_point.$$f -o lib/pvs/floating_point/; done
|
|
|
|
drivers/pvs-realizations.aux: Makefile
|
|
$(SHOW) 'Generate $@'
|
|
$(HIDE)(echo "(* generated automatically at compilation time *)"; \
|
|
for f in $(PVSLIBS_INT_FILES); do \
|
|
echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
|
|
for f in $(PVSLIBS_REAL_FILES); do \
|
|
echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
|
|
for f in $(PVSLIBS_LIST_FILES); do \
|
|
echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
|
|
for f in $(PVSLIBS_NUMBER_FILES); do \
|
|
echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
|
|
for f in $(PVSLIBS_FP_FILES); do \
|
|
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
|
|
) > $@
|
|
|
|
pvs: lib/pvs/version
|
|
|
|
clean-pvs:
|
|
rm -f lib/pvs/version
|
|
|
|
ifeq (@enable_pvs_libs@,yes)
|
|
|
|
uninstall-pvs:
|
|
rm -rf $(LIBDIR)/why3/pvs
|
|
|
|
install-pvs:
|
|
$(MKDIR_P) $(LIBDIR)/why3/pvs
|
|
$(INSTALL_DATA) lib/pvs/version $(LIBDIR)/why3/pvs/
|
|
$(MKDIR_P) $(LIBDIR)/why3/pvs/int
|
|
$(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_INT)) $(LIBDIR)/why3/pvs/int/
|
|
$(INSTALL_DATA) $(addsuffix .prf, $(PVSLIBS_INT)) $(LIBDIR)/why3/pvs/int/
|
|
$(MKDIR_P) $(LIBDIR)/why3/pvs/real
|
|
$(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_REAL)) $(LIBDIR)/why3/pvs/real/
|
|
$(INSTALL_DATA) $(addsuffix .prf, $(PVSLIBS_REAL)) $(LIBDIR)/why3/pvs/real/
|
|
$(MKDIR_P) $(LIBDIR)/why3/pvs/floating_point/
|
|
$(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_FP)) $(LIBDIR)/why3/pvs/floating_point/
|
|
$(MKDIR_P) $(DATADIR)/why3/drivers/
|
|
$(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
|
|
|
|
install:: install-pvs
|
|
|
|
all: pvs
|
|
|
|
endif
|
|
|
|
install-data::
|
|
$(MKDIR_P) $(DATADIR)/why3/drivers/
|
|
$(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
|
|
|
|
all: drivers/pvs-realizations.aux
|
|
|
|
clean:: clean-pvs
|
|
rm -f drivers/pvs-realizations.aux
|
|
|
|
#######################
|
|
# Isabelle realizations
|
|
#######################
|
|
|
|
|
|
ISABELLEVERSIONSPECIFIC=ROOT why3.ML Why3_BV.thy Why3_Map.thy
|
|
|
|
ISABELLEVERSIONSPECIFICTARGETS=$(addprefix lib/isabelle/, $(ISABELLEVERSIONSPECIFIC))
|
|
|
|
ISABELLEREALIZEDRV=isabelle-realize
|
|
ISABELLEREALIZEDRVPATH=drivers/$(ISABELLEREALIZEDRV).drv
|
|
|
|
$(ISABELLEVERSIONSPECIFICTARGETS): %: %.@ISABELLEVERSION@
|
|
$(CMP_CP)
|
|
|
|
clean-isabelle::
|
|
rm -f $(ISABELLEVERSIONSPECIFICTARGETS)
|
|
|
|
ISABELLELIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
|
|
ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/int/, $(ISABELLELIBS_INT_FILES)))
|
|
|
|
ISABELLELIBS_BOOL_FILES = Bool
|
|
ISABELLELIBS_BOOL = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/bool/, $(ISABELLELIBS_BOOL_FILES)))
|
|
|
|
ISABELLELIBS_REAL_FILES = Real RealInfix Abs MinMax FromInt Truncate Square ExpLog Trigonometry PowerInt # not yet realized : PowerReal Hyperbolic Polar
|
|
ISABELLELIBS_REAL = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/real/, $(ISABELLELIBS_REAL_FILES)))
|
|
|
|
ISABELLELIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
|
|
ISABELLELIBS_NUMBER = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/number/, $(ISABELLELIBS_NUMBER_FILES)))
|
|
|
|
ISABELLELIBS_SET_FILES = Set Fset
|
|
ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/set/, $(ISABELLELIBS_SET_FILES)))
|
|
|
|
ISABELLELIBS_MAP_FILES = Map Const Occ MapPermut MapInjection
|
|
ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/map/, $(ISABELLELIBS_MAP_FILES)))
|
|
|
|
ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt RevAppend Combine Distinct NumOcc Permut
|
|
ISABELLELIBS_LIST = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/list/, $(ISABELLELIBS_LIST_FILES)))
|
|
|
|
ISABELLELIBS_BV_FILES = Pow2int
|
|
# BV8 BV16 BV32 BV64 BVConverter_32_64 BVConverter_16_64 BVConverter_8_64 BVConverter_16_32 BVConverter_8_32 BVConverter_8_16
|
|
ISABELLELIBS_BV = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/bv/, $(ISABELLELIBS_BV_FILES)))
|
|
|
|
ISABELLELIBS = $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
|
|
|
|
drivers/isabelle-realizations.aux: Makefile
|
|
$(SHOW) 'Generate $@'
|
|
$(HIDE)(echo "(* generated automatically at compilation time *)"; \
|
|
echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \
|
|
for f in $(ISABELLELIBS_INT_FILES); do \
|
|
echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
|
|
for f in $(ISABELLELIBS_BOOL_FILES); do \
|
|
echo 'theory bool.'"$$f"' meta "realized_theory" "bool.'"$$f"'", "" end'; done; \
|
|
for f in $(ISABELLELIBS_REAL_FILES); do \
|
|
echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
|
|
for f in $(ISABELLELIBS_NUMBER_FILES); do \
|
|
echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
|
|
for f in $(ISABELLELIBS_SET_FILES); do \
|
|
echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
|
|
for f in $(ISABELLELIBS_MAP_FILES); do \
|
|
echo 'theory map.'"$$f"' meta "realized_theory" "map.'"$$f"'", "" end'; done; \
|
|
for f in $(ISABELLELIBS_LIST_FILES); do \
|
|
echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
|
|
for f in $(ISABELLELIBS_OPTION_FILES); do \
|
|
echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
|
|
for f in $(ISABELLELIBS_BV_FILES); do \
|
|
echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \
|
|
) > $@
|
|
|
|
ifeq (@enable_local@,yes)
|
|
ISABELLE_TARGET_DIR=`pwd`/lib/isabelle
|
|
else
|
|
ISABELLE_TARGET_DIR=$(LIBDIR)/why3/isabelle
|
|
endif
|
|
|
|
$(GENERATED_PREFIX_ISABELLE)/realizations: $(ISABELLELIBS)
|
|
$(HIDE)sha1sum $^ | sed -e "s,$(GENERATED_PREFIX_ISABELLE)/,," > $@
|
|
|
|
update-isabelle: $(GENERATED_PREFIX_ISABELLE)/realizations
|
|
|
|
$(ISABELLELIBS_INT): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
|
|
$(ISABELLEREALIZEDRVPATH) 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/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/int/
|
|
|
|
$(ISABELLELIBS_BOOL): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
|
|
$(ISABELLEREALIZEDRVPATH) 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/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bool/
|
|
|
|
$(ISABELLELIBS_REAL): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
|
|
$(ISABELLEREALIZEDRVPATH) 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/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/real/
|
|
|
|
$(ISABELLELIBS_NUMBER): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
|
|
$(ISABELLEREALIZEDRVPATH) 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/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/number/
|
|
|
|
$(ISABELLELIBS_SET): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
|
|
$(ISABELLEREALIZEDRVPATH) 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/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/set/
|
|
|
|
$(ISABELLELIBS_MAP): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
|
|
$(ISABELLEREALIZEDRVPATH) 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/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/map/
|
|
|
|
$(ISABELLELIBS_LIST): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
|
|
$(ISABELLEREALIZEDRVPATH) 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/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/list/
|
|
|
|
$(ISABELLELIBS_OPTION): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
|
|
$(ISABELLEREALIZEDRVPATH) 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/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/option/
|
|
|
|
$(ISABELLELIBS_BV): bin/why3.@OCAMLBEST@ bin/why3realize.$(SHAREDBEST) drivers/isabelle-realizations.aux \
|
|
$(ISABELLEREALIZEDRVPATH) 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/why3.@OCAMLBEST@ realize $(LOCAL_STDLIB) -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bv/
|
|
|
|
ifeq (@enable_isabelle_libs@,yes)
|
|
|
|
$(GENERATED_PREFIX_ISABELLE)/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(ISABELLELIBS)
|
|
ifneq (@enable_local@,yes)
|
|
cp -r $(GENERATED_PREFIX_ISABELLE) "$(LIBDIR)/why3"
|
|
endif
|
|
@(if isabelle components -l | grep -q "$(ISABELLE_TARGET_DIR)$$"; then \
|
|
echo "Building the Why3 heap for Isabelle/HOL:"; \
|
|
isabelle build -bc Why3; \
|
|
touch $@; \
|
|
else \
|
|
echo "[Warning] Cannot pre-build the Isabelle heap because"; \
|
|
echo " the Isabelle component configuration does not contain"; \
|
|
echo " [$(ISABELLE_TARGET_DIR)]"; \
|
|
fi)
|
|
|
|
install-isabelle: $(GENERATED_PREFIX_ISABELLE)/last_build
|
|
|
|
install_local:: install-isabelle
|
|
install:: install-isabelle
|
|
|
|
endif
|
|
|
|
all: drivers/isabelle-realizations.aux
|
|
|
|
install-data::
|
|
$(INSTALL_DATA) drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/
|
|
|
|
clean-isabelle::
|
|
rm -f $(GENERATED_PREFIX_ISABELLE)/*/*.xml
|
|
|
|
clean:: clean-isabelle
|
|
rm -f drivers/isabelle-realizations.aux
|
|
|
|
#######################
|
|
# Isabelle client
|
|
#######################
|
|
|
|
ISABELLEC_FILES := isabelle_client_main
|
|
|
|
ISABELLECMODULES := $(addprefix src/isabelle-client/, $(ISABELLEC_FILES))
|
|
ISABELLECDEP = $(addsuffix .dep, $(ISABELLECMODULES))
|
|
ISABELLECCMO = $(addsuffix .cmo, $(ISABELLECMODULES))
|
|
ISABELLECCMX = $(addsuffix .cmx, $(ISABELLECMODULES))
|
|
|
|
$(ISABELLECDEP) $(ISABELLECCMO) $(ISABELLECCMX): INCLUDES += -I src/isabelle-client -I src/util
|
|
|
|
depend: $(ISABELLECDEP)
|
|
CLEANDIRS += src/isabelle-client
|
|
|
|
# build targets
|
|
|
|
byte: bin/isabelle_client.byte
|
|
opt: bin/isabelle_client.opt
|
|
|
|
bin/isabelle_client.opt: lib/why3/why3.cmxa $(ISABELLECCMX)
|
|
|
|
bin/isabelle_client.byte: lib/why3/why3.cma $(ISABELLECCMO)
|
|
|
|
# install-bin::
|
|
# cp -f bin/isabelle_client.@OCAMLBEST@ $(BINDIR)/isabelle_client$(EXE)
|
|
|
|
# uninstall-bin::
|
|
# rm -f $(BINDIR)/isabelle_client$(EXE)
|
|
|
|
MAKEINC += $(ISABELLECDEP)
|
|
|
|
clean::
|
|
rm -f bin/isabelle_client.byte bin/isabelle_client.opt bin/isabelle_client
|
|
|
|
################
|
|
# Jessie3 plugin
|
|
################
|
|
|
|
ifeq (@enable_frama_c@,yes)
|
|
|
|
nobyte: jessie.byte
|
|
noopt: jessie.opt
|
|
|
|
jessie.byte: src/jessie/Makefile $(WHY3CMA)
|
|
@$(MAKE) -C src/jessie Jessie3.cma
|
|
|
|
jessie.opt: src/jessie/Makefile $(WHY3CMXA)
|
|
@$(MAKE) -C src/jessie Jessie3.cmxs
|
|
|
|
uninstall-framac:
|
|
rm -f $(FRAMAC_LIBDIR)/plugins/Jessie3.*
|
|
|
|
uninstall:: uninstall-framac
|
|
|
|
install-framac:
|
|
$(MKDIR_P) $(FRAMAC_LIBDIR)/plugins/
|
|
$(INSTALL_DATA) $(wildcard $(addprefix src/jessie/Jessie3., $(INSTALLED_LIB_EXTS))) \
|
|
$(FRAMAC_LIBDIR)/plugins/
|
|
|
|
install:: install-framac
|
|
|
|
clean::
|
|
$(MAKE) -C src/jessie clean
|
|
|
|
endif
|
|
|
|
###############
|
|
# Why3 pp
|
|
###############
|
|
|
|
PRETTYPRINT_FILES = why3pp
|
|
|
|
PRETTYPRINTMODULES = $(addprefix src/tools/, $(PRETTYPRINT_FILES))
|
|
|
|
PRETTYPRINTDEP = $(addsuffix .dep, $(PRETTYPRINTMODULES))
|
|
PRETTYPRINTCMO = $(addsuffix .cmo, $(PRETTYPRINTMODULES))
|
|
PRETTYPRINTCMX = $(addsuffix .cmx, $(PRETTYPRINTMODULES))
|
|
|
|
$(PRETTYPRINTDEP) $(PRETTYPRINTCMO) $(PRETTYPRINTCMX): INCLUDES += -I src/tools
|
|
|
|
# build targets
|
|
|
|
byte: bin/why3pp.cma
|
|
opt: bin/why3pp.cmxs
|
|
|
|
bin/why3pp.cmxs: $(PRETTYPRINTCMX)
|
|
bin/why3pp.cma: $(PRETTYPRINTCMO)
|
|
|
|
# depend and clean targets
|
|
|
|
MAKEINC += $(PRETTYPRINTDEP)
|
|
|
|
uninstall-bin::
|
|
rm -f $(TOOLDIR)/why3pp.$(SHAREDBEST)
|
|
|
|
install-bin::
|
|
$(MKDIR_P) $(TOOLDIR)
|
|
$(INSTALL_DATA) bin/why3pp.$(SHAREDBEST) $(TOOLDIR)
|
|
|
|
install_local:: bin/why3pp.$(SHAREDBEST)
|
|
|
|
#########
|
|
# why3doc
|
|
#########
|
|
|
|
WHY3DOCGENERATED = src/why3doc/doc_lexer.ml
|
|
|
|
WHY3DOC_FILES = doc_html doc_def doc_lexer doc_main
|
|
|
|
WHY3DOCMODULES = $(addprefix src/why3doc/, $(WHY3DOC_FILES))
|
|
|
|
WHY3DOCDEP = $(addsuffix .dep, $(WHY3DOCMODULES))
|
|
WHY3DOCCMO = $(addsuffix .cmo, $(WHY3DOCMODULES))
|
|
WHY3DOCCMX = $(addsuffix .cmx, $(WHY3DOCMODULES))
|
|
|
|
$(WHY3DOCDEP) $(WHY3DOCCMO) $(WHY3DOCCMX): INCLUDES += -I src/why3doc
|
|
|
|
$(WHY3DOCDEP): $(WHY3DOCGENERATED)
|
|
|
|
# build targets
|
|
|
|
byte: bin/why3doc.cma
|
|
opt: bin/why3doc.cmxs
|
|
|
|
bin/why3doc.cmxs: $(WHY3DOCCMX)
|
|
bin/why3doc.cma: $(WHY3DOCCMO)
|
|
|
|
# depend and clean targets
|
|
|
|
MAKEINC += $(WHY3DOCDEP)
|
|
|
|
CLEANDIRS += src/why3doc
|
|
GENERATED += $(WHY3DOCGENERATED)
|
|
|
|
uninstall-bin::
|
|
rm -f $(TOOLDIR)/why3doc.$(SHAREDBEST)
|
|
|
|
install-bin::
|
|
$(MKDIR_P) $(TOOLDIR)
|
|
$(INSTALL_DATA) bin/why3doc.$(SHAREDBEST) $(TOOLDIR)
|
|
|
|
install_local:: bin/why3doc.$(SHAREDBEST)
|
|
|
|
#########
|
|
# trywhy3
|
|
#########
|
|
|
|
ifeq ($(DEBUGJS),yes)
|
|
JSOO_DEBUG=--pretty --debug-info --source-map
|
|
JS_MAPS=trywhy3.map why3_worker.map
|
|
else
|
|
JSOO_DEBUG=
|
|
JS_MAPS=
|
|
endif
|
|
|
|
TRYWHY3_FILES = json_base json_parser json_lexer bindings shortener trywhy3 why3_worker worker_proto
|
|
|
|
TRYWHY3MODULES = $(addprefix src/trywhy3/, $(TRYWHY3_FILES))
|
|
|
|
TRYWHY3DEP = $(addsuffix .dep, $(TRYWHY3MODULES))
|
|
TRYWHY3CMO = $(addsuffix .cmo, $(TRYWHY3MODULES))
|
|
TRYWHY3CMI = $(addsuffix .cmi, $(TRYWHY3MODULES))
|
|
|
|
$(TRYWHY3DEP) $(TRYWHY3CMO) $(TRYWHY3CMI): INCLUDES += -I src/trywhy3
|
|
|
|
TRYWHY3_COMMON_PACK = \
|
|
trywhy3.js trywhy3.html trywhy3.css trywhy3_custom.css \
|
|
help_whyml.html help_python.html help_micro-C.html \
|
|
why3_worker.js \
|
|
examples/ \
|
|
$(JS_MAPS)
|
|
|
|
TRYWHY3_SMALL_PACK = \
|
|
$(TRYWHY3_COMMON_PACK) \
|
|
mode-why3.js
|
|
|
|
TRYWHY3_FULL_PACK = \
|
|
$(TRYWHY3_COMMON_PACK) \
|
|
alt-ergo-worker.js \
|
|
ace-builds/src-min-noconflict/ace.js \
|
|
ace-builds/src-min-noconflict/mode-why3.js \
|
|
ace-builds/src-min-noconflict/mode-python.js \
|
|
ace-builds/src-min-noconflict/mode-c_cpp.js \
|
|
ace-builds/src-min-noconflict/theme-chrome.js
|
|
|
|
trywhy3.tar.gz: $(addprefix src/trywhy3/, $(TRYWHY3_SMALL_PACK))
|
|
tar czf $@ -C src $(addprefix trywhy3/, $(TRYWHY3_SMALL_PACK))
|
|
|
|
trywhy3-full.tar.gz: $(addprefix src/trywhy3/, $(TRYWHY3_FULL_PACK))
|
|
tar czf $@ -C src $(addprefix trywhy3/, $(TRYWHY3_FULL_PACK))
|
|
|
|
trywhy3: src/trywhy3/trywhy3.js src/trywhy3/why3_worker.js
|
|
|
|
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
|
|
$(SHOW) 'Js_of_ocaml $<'
|
|
$(HIDE)js_of_ocaml $(JSOO_DEBUG) --Werror $<
|
|
|
|
src/trywhy3/trywhy3.byte: $(addprefix src/trywhy3/, json_base.cmo json_parser.cmo json_lexer.cmo bindings.cmo worker_proto.cmo shortener.cmo trywhy3.cmo)
|
|
$(SHOW) 'Linking $@'
|
|
$(HIDE)$(OCAMLFIND) ocamlc -o $@ -package js_of_ocaml -package menhirLib -linkpkg $^
|
|
|
|
src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte src/trywhy3/trywhy3.conf src/trywhy3/try_alt_ergo.drv
|
|
$(SHOW) 'Js_of_ocaml $<'
|
|
$(HIDE)js_of_ocaml $(JSOO_DEBUG) --Werror -I . -I src/trywhy3 \
|
|
--extern-fs --file=trywhy3.conf:/ --file=try_alt_ergo.drv:/ \
|
|
`find stdlib -name "*.mlw" -exec printf " --file=%s:/%s" {} {} ";"` \
|
|
+dynlink.js +toplevel.js +zarith_stubs_js/biginteger.js +zarith_stubs_js/runtime.js $<
|
|
|
|
src/trywhy3/why3_worker.byte: $(WHY3CMA) $(PYTHONCMO) $(MICROCCMO) \
|
|
$(addprefix src/trywhy3/, bindings.cmo worker_proto.cmo why3_worker.cmo)
|
|
$(SHOW) 'Linking $@'
|
|
$(HIDE)$(OCAMLFIND) ocamlc $(filter-out -thread,$(BFLAGS)) -package js_of_ocaml -o $@ -linkpkg $^
|
|
|
|
$(addprefix src/trywhy3/, worker_proto.cmo why3_worker.cmo): BFLAGS += -package js_of_ocaml
|
|
|
|
$(addprefix src/trywhy3/, bindings.cmo trywhy3.cmo): BFLAGS += -package js_of_ocaml -package js_of_ocaml-ppx
|
|
|
|
TRYWHY3JSON_FILES = json_base json_parser json_lexer
|
|
TRYWHY3JSON = $(TRYWHY3JSON_FILES:%=src/trywhy3/%.ml) $(TRYWHY3JSON_FILES:%=src/trywhy3/%.mli)
|
|
|
|
$(TRYWHY3JSON): src/trywhy3/%: src/util/%
|
|
cp $< $@
|
|
|
|
GENERATED += $(TRYWHY3JSON)
|
|
|
|
$(TRYWHY3DEP): $(TRYWHY3JSON)
|
|
|
|
MAKEINC += $(TRYWHY3DEP)
|
|
|
|
clean-trywhy3:
|
|
rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte \
|
|
src/trywhy3/why3_worker.js src/trywhy3/why3_worker.byte \
|
|
trywhy3.tar.gz
|
|
|
|
clean:: clean-trywhy3
|
|
|
|
CLEANDIRS += src/trywhy3
|
|
|
|
|
|
#########
|
|
# why3webserver and full web/js interface
|
|
#########
|
|
|
|
ifeq (@enable_web_ide@,yes)
|
|
|
|
src/ide/why3_js.cmo: BFLAGS += -package js_of_ocaml -package js_of_ocaml-ppx
|
|
|
|
src/ide/why3_js.byte: lib/why3/why3.cma src/ide/why3_js.cmo
|
|
$(SHOW) 'Linking $@'
|
|
$(HIDE)$(OCAMLFIND) ocamlc -package js_of_ocaml \
|
|
$(filter-out -thread,$(BFLAGS)) -o $@ -linkpkg $(BLINKFLAGS) $^
|
|
|
|
src/ide/why3_js.js: src/ide/why3_js.byte
|
|
$(SHOW) 'Js_of_ocaml $<'
|
|
$(HIDE)js_of_ocaml --Werror +dynlink.js +toplevel.js +zarith_stubs_js/biginteger.js +zarith_stubs_js/runtime.js $<
|
|
|
|
web_ide: src/ide/why3_js.js
|
|
|
|
opt: bin/why3webserver.cmxs
|
|
byte: bin/why3webserver.cma src/ide/why3_js.cmo
|
|
|
|
endif
|
|
|
|
########
|
|
# bench
|
|
########
|
|
|
|
.PHONY: bench test
|
|
|
|
bench:: bin/why3.@OCAMLBEST@ bin/why3config.$(SHAREDBEST) plugins $(TOOLS) \
|
|
share/Makefile.config bin/why3extract.$(SHAREDBEST)
|
|
bin/why3.@OCAMLBEST@ config list-provers | grep -q Alt-Ergo || \
|
|
bin/why3.@OCAMLBEST@ config detect
|
|
@echo "=== Check API examples ==="
|
|
$(MAKE) bench-api
|
|
@echo "=== Check examples ==="
|
|
bash bench/bench -suffix ".@OCAMLBEST@"
|
|
@echo "=== Check parsing messages ==="
|
|
bench/parsing-bench
|
|
|
|
APITESTS = \
|
|
clone \
|
|
counterexample \
|
|
create_session \
|
|
logic \
|
|
mlw_expr \
|
|
mlw_tree \
|
|
transform
|
|
|
|
ifeq (@enable_infer@,yes)
|
|
APITESTS += mlw_tree_infer_invs
|
|
endif
|
|
|
|
ifeq (@enable_infer@,yes)
|
|
APITESTS += mlw_tree_bddinfer_invs
|
|
endif
|
|
|
|
ifeq (@enable_sexp@,yes)
|
|
APITESTS += epsilon
|
|
endif
|
|
|
|
bench-api: $(addprefix test-api-, $(APITESTS))
|
|
|
|
clean::
|
|
rm -rf bench/infer/*.out
|
|
rm -rf bench/bddinfer/*.out
|
|
rm -rf bench/check-ce/*.out
|
|
|
|
###############
|
|
# test targets
|
|
###############
|
|
|
|
test-itp.opt: src/printer/itp.ml lib/why3/why3.cmxa
|
|
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
|
|
$(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(OLINKFLAGS) lib/why3/why3.cmxa $<
|
|
|
|
test-api-%.byte: examples/use_api/%.ml lib/why3/why3.cma
|
|
$(SHOW) 'Ocaml $<'
|
|
$(HIDE)($(OCAMLC) -o $@ -I lib/why3 $(BFLAGS) $(BLINKFLAGS) lib/why3/why3.cma $<) \
|
|
|| (printf "Compilation failed for API test $@. Please fix it.\n"; exit 2)
|
|
|
|
test-api-%.opt: examples/use_api/%.ml lib/why3/why3.cmxa
|
|
$(SHOW) 'Ocamlopt $<'
|
|
$(HIDE)($(OCAMLOPT) -o $@ -I lib/why3 $(OFLAGS) $(OLINKFLAGS) lib/why3/why3.cmxa $<) \
|
|
|| (printf "Compilation failed for API test $@. Please fix it.\n"; exit 2)
|
|
|
|
test-api-%: test-api-%.@OCAMLBEST@
|
|
$(HIDE)mkdir -p examples/use_api/results
|
|
$(HIDE)(./$< | sed -e 's/^\(Versions of Alt-Ergo found: \).*$$/\1<hidden>/' \
|
|
-e 's/0\.0[0-9]/<hidden>/g;s/[0-9]\+ steps/<hidden> steps/' \
|
|
> examples/use_api/results/$@.stdout ) \
|
|
|| (printf "Execution failed for API test $<. Please fix it.\n"; exit 2)
|
|
$(HIDE)(diff -u examples/use_api/oracles/$@.stdout examples/use_api/results/$@.stdout) \
|
|
|| (printf "Oracle updated for API test $<. Please review it.\n"; cp examples/use_api/results/$@.stdout examples/use_api/oracles/$@.stdout )
|
|
$(HIDE)rm -f $< why3session.xml why3shapes why3shapes.gz
|
|
|
|
|
|
#test-shape: lib/why3/why3.cma
|
|
# ocaml -I lib/why3 $(INCLUDES) $(BLINKFLAGS) $? examples/test_shape.ml
|
|
|
|
|
|
################
|
|
# documentation
|
|
################
|
|
|
|
.PHONY: doc predoc update-doc-png clean-doc
|
|
|
|
doc/generated/drivers-all.dot: drivers/*.drv drivers/*.gen
|
|
doc/drv_depgraph $^ > $@
|
|
|
|
doc/generated/drivers-%.dot: doc/generated/drivers-all.dot
|
|
ccomps -X $(NODE) $< > $@
|
|
|
|
doc/generated/drivers-smt.dot: NODE = smt-libv2.gen
|
|
doc/generated/drivers-tptp.dot: NODE = tptp.gen
|
|
doc/generated/drivers-coq.dot: NODE = coq-common.gen
|
|
doc/generated/drivers-isabelle.dot: NODE = isabelle-common.gen
|
|
doc/generated/drivers-pvs.dot: NODE = pvs-common.gen
|
|
|
|
DRVDOT = $(patsubst %,doc/generated/drivers-%.dot, smt tptp coq isabelle pvs)
|
|
|
|
DOC = index zebibliography genindex \
|
|
foreword starting whyml api install manpages syntaxref vcgen \
|
|
input_formats exec itp technical changes
|
|
|
|
DOCRST = $(DOC:%=doc/%.rst) doc/whyml2java.inc doc/manual.bib
|
|
|
|
LIBDOT = $(patsubst %,doc/generated/library-%.dot, int array)
|
|
|
|
doc/generated/library-%.dot: stdlib/%.mlw
|
|
bin/why3 pp --output=dep $< | tred > $@
|
|
|
|
predoc: $(DRVDOT) $(LIBDOT) java-examples
|
|
|
|
java-examples:
|
|
${MAKE} -C doc/javaexamples all
|
|
|
|
clean-java-examples:
|
|
${MAKE} -C doc/javaexamples clean
|
|
|
|
update-doc-png:
|
|
export UBUNTU_MENUPROXY=0; \
|
|
export WHY3CONFIG=doc/why3ide-doc.conf; \
|
|
export WHY3LOADPATH=stdlib; \
|
|
export GTK_THEME=Adwaita; \
|
|
export WAYLAND_DISPLAY=; \
|
|
sed -n -e 's/^.. %EXECUTE \(.*\)/\1/p' $(DOCRST) | $(SHELL) -e
|
|
|
|
ifeq (@enable_doc@,yes)
|
|
|
|
doc: doc/html/index.html
|
|
|
|
TESTSAPIDOC = $(addsuffix .ml, $(addprefix examples/use_api/, $(APITESTS)))
|
|
|
|
doc/html/index.html: $(DOCRST) $(DRVDOT) $(LIBDOT) $(TESTSAPIDOC) java-examples doc/conf.py
|
|
$(SPHINX) -b html -d doc/.doctrees doc doc/html
|
|
|
|
doc/latex/manual.tex: $(DOCRST) $(DRVDOT) $(LIBDOT) $(TESTSAPIDOC) java-examples doc/conf.py
|
|
$(SPHINX) -b latex -d doc/.doctrees doc doc/latex
|
|
|
|
ifeq (@enable_pdf_doc@,yes)
|
|
|
|
doc: doc/latex/manual.pdf
|
|
|
|
doc/latex/manual.pdf: doc/latex/manual.tex
|
|
@echo "running LaTeX compilation..."
|
|
cd doc/latex; $(LATEXCOMP) manual.tex >/dev/null
|
|
ifeq (@LATEX@,pdflatex)
|
|
@cd doc/latex; if grep 'may have changed. Rerun to get' manual.log; then \
|
|
makeindex manual; \
|
|
echo "running LaTeX again to try to fix references..."; \
|
|
pdflatex manual >/dev/null; \
|
|
fi
|
|
@cd doc/latex; if grep 'may have changed. Rerun to get' manual.log; then \
|
|
echo "running LaTeX again to try to fix references..."; \
|
|
pdflatex manual >/dev/null; \
|
|
fi
|
|
endif
|
|
|
|
endif
|
|
|
|
else
|
|
|
|
doc:
|
|
|
|
endif
|
|
|
|
clean-doc: clean-java-examples
|
|
rm -rf doc/html doc/latex
|
|
rm -rf doc/generated/*.dot
|
|
|
|
clean:: clean-doc
|
|
|
|
##########
|
|
# API DOC
|
|
##########
|
|
|
|
.PHONY: apidoc apidot
|
|
|
|
MODULESTODOC = \
|
|
util/util util/opt util/lists util/strings util/getopt \
|
|
util/extmap util/extset util/exthtbl \
|
|
util/weakhtbl util/wstdlib util/rc util/debug \
|
|
util/loc util/pp util/bigInt util/number \
|
|
util/mlmpfr_wrapper \
|
|
core/ident core/ty core/term core/decl core/coercion core/theory \
|
|
core/env core/task core/trans core/pretty core/printer \
|
|
core/model_parser \
|
|
parser/ptree.ml \
|
|
parser/ptree_helpers parser/typing parser/mlw_printer \
|
|
driver/whyconf driver/call_provers driver/driver \
|
|
transform/args_wrapper \
|
|
mlw/ity mlw/expr mlw/pdecl mlw/pmodule mlw/vc \
|
|
mlw/pinterp_core mlw/rac mlw/pinterp mlw/check_ce \
|
|
session/session_itp session/controller_itp \
|
|
session/itp_communication session/itp_server \
|
|
session/strategy
|
|
|
|
ifeq (@enable_bddinfer@,yes)
|
|
MODULESTODOC += bddinfer/why3infer
|
|
endif
|
|
|
|
FILESTODOC = $(subst .ml.mli,.ml,$(MODULESTODOC:%=src/%.mli))
|
|
|
|
DOCFLAGS = -sort $(INCLUDES) $(LIBINCLUDES)
|
|
|
|
ifeq (@enable_ocamlfind@,yes)
|
|
DOCFLAGS += $(addprefix -package ,$(EXTPKGS))
|
|
else
|
|
DOCFLAGS += $(EXTINCLUDES)
|
|
endif
|
|
|
|
doc/apidoc:
|
|
mkdir -p doc/apidoc
|
|
|
|
apidoc: doc/apidoc $(FILESTODOC)
|
|
$(OCAMLDOC) $(DOCFLAGS) -d doc/apidoc -charset utf-8 -html \
|
|
-t "Why3 API documentation" -keep-code $(FILESTODOC)
|
|
|
|
# could we include also the dependency graph ? -- someone
|
|
# At least we can give a way to create it -- francois
|
|
|
|
apidot: doc/apidoc/dg.svg doc/apidoc/dg.png
|
|
|
|
#The sed remove configuration for dot that gives bad result
|
|
doc/apidoc/dg.dot: doc/apidoc $(FILESTODOC)
|
|
$(OCAMLDOC) $(DOCFLAGS) -o doc/apidoc/dg.dot.tmp -dot $(FILESTODOC)
|
|
sed -e "s/ \(size\|ratio\|rotate\|fontsize\).*$$//" doc/apidoc/dg.dot.tmp \
|
|
| tred > doc/apidoc/dg.dot
|
|
rm -f doc/apidoc/dg.dot.tmp
|
|
|
|
doc/apidoc/dg.svg: doc/apidoc/dg.dot
|
|
dot -T svg $< > $@
|
|
|
|
doc/apidoc/dg.png: doc/apidoc/dg.dot
|
|
dot -T png $< > $@
|
|
|
|
doc/apidoc.tex: $(FILESTODOC)
|
|
$(OCAMLDOC) $(DOCFLAGS) -o doc/apidoc.tex -latex -noheader -notrailer $(FILESTODOC)
|
|
|
|
clean::
|
|
rm -f doc/apidoc/*
|
|
|
|
##########
|
|
# Install rules for bash completions
|
|
##########
|
|
|
|
uninstall-bash:
|
|
if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then \
|
|
rm -f /etc/bash_completion.d/why3; \
|
|
fi
|
|
|
|
uninstall:: uninstall-bash
|
|
|
|
install-bash::
|
|
if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then \
|
|
$(INSTALL) share/bash/why3 /etc/bash_completion.d; \
|
|
fi
|
|
|
|
install:: install-bash
|
|
|
|
##########
|
|
# Stdlib formatted with why3doc
|
|
##########
|
|
|
|
.PHONY: stdlibdoc
|
|
|
|
STDMACHLIBS = \
|
|
array bv c float fxp int matrix onetime peano tagset \
|
|
java/lang java/util
|
|
|
|
STDLIBS = \
|
|
algebra array \
|
|
bag bintree bool bv \
|
|
cursor \
|
|
exn \
|
|
floating_point fmap function \
|
|
graph hashtbl \
|
|
ieee_float int io \
|
|
list \
|
|
map matrix \
|
|
number \
|
|
ocaml option \
|
|
pigeon pqueue \
|
|
queue \
|
|
random real ref regexp relations \
|
|
seq set stack string \
|
|
tree \
|
|
ufloat \
|
|
witness \
|
|
$(addprefix mach/, $(STDMACHLIBS))
|
|
|
|
# NO NEED DOC:
|
|
# debug: too basic, needs large improvement
|
|
# tptp: for TPTP provers ?
|
|
# for_drivers: used only in drivers
|
|
|
|
STDLIBFILES = $(patsubst %,stdlib/%.mlw, $(STDLIBS))
|
|
|
|
# TODO: remove the hack about int.mlw once it has become builtin
|
|
stdlibdoc: $(STDLIBFILES) bin/why3.@OCAMLBEST@ bin/why3doc.$(SHAREDBEST)
|
|
mkdir -p doc/stdlibdoc
|
|
sed -e "s/use Int/use int.Int/" stdlib/int.mlw > int.mlw
|
|
rm -f doc/stdlibdoc/style.css
|
|
WHY3CONFIG="" bin/why3.@OCAMLBEST@ doc $(LOCAL_STDLIB) \
|
|
-o doc/stdlibdoc --title="Why3 Standard Library" \
|
|
$(subst stdlib/int.mlw,int.mlw,$(STDLIBFILES))
|
|
rm int.mlw
|
|
cd doc/stdlibdoc; \
|
|
for f in stdlib.*.html; \
|
|
do mv "$$f" "$${f#stdlib.}"; done
|
|
sed -i -e "s#stdlib.##g" doc/stdlibdoc/index.html
|
|
sed -i -e "s#int\.\(<a href=\"\)int\.html#\1#g" doc/stdlibdoc/int.html
|
|
|
|
clean::
|
|
rm -f doc/stdlibdoc/*
|
|
|
|
################
|
|
# generic rules
|
|
################
|
|
|
|
%.cmi: %.mli
|
|
$(SHOW) 'Ocamlc $<'
|
|
$(HIDE)$(OCAMLC) -c $(BFLAGS) $<
|
|
|
|
# suppress "unused rec" warning for Menhir-produced files
|
|
%.cmo: %.ml %.mly
|
|
$(SHOW) 'Ocamlc $<'
|
|
$(HIDE)$(OCAMLC) -c $(BFLAGS) -w -39 $<
|
|
|
|
# suppress "unused rec" warning for Menhir-produced files
|
|
%.cmx: %.ml %.mly
|
|
$(SHOW) 'Ocamlopt $<'
|
|
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) -w -39 $(CMIHACK) $<
|
|
|
|
%.cmo: %.ml
|
|
$(SHOW) 'Ocamlc $<'
|
|
$(HIDE)$(OCAMLC) -c $(BFLAGS) $<
|
|
|
|
%.cmx: %.ml %.mli
|
|
$(SHOW) 'Ocamlopt $<'
|
|
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) $<
|
|
|
|
%.cmx: %.ml
|
|
$(SHOW) 'Ocamlopt $<'
|
|
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) $(CMIHACK) $<
|
|
|
|
%.cma:
|
|
$(SHOW) 'Linking $@'
|
|
$(HIDE)$(OCAMLC) -a $(BFLAGS) -o $@ $^
|
|
|
|
%.cmxa:
|
|
$(SHOW) 'Linking $@'
|
|
$(HIDE)$(OCAMLOPT) -a $(OFLAGS) -o $@ $^
|
|
|
|
%.cmxs:
|
|
$(SHOW) 'Linking $@'
|
|
$(HIDE)$(OCAMLOPT) -shared $(OFLAGS) -o $@ $^
|
|
|
|
%.ml: %.mll
|
|
$(SHOW) 'Ocamllex $<'
|
|
$(HIDE)$(OCAMLLEX) $<
|
|
|
|
# the % below are not a typo; they are a way to force Make to consider all the targets at once
|
|
src/c%re/parser_tokens.ml src/c%re/parser_tokens.mli: src/parser/parser_common.mly
|
|
$(SHOW) 'Menhir $^'
|
|
$(HIDE)$(MENHIR) --base src/core/parser_tokens --only-tokens $^
|
|
|
|
src/p%rser/parser.ml src/p%rser/parser.mli: $(PARSERS)
|
|
$(SHOW) 'Menhir $^'
|
|
$(HIDE)$(MENHIR) --table --explain --strict --base src/parser/parser \
|
|
--external-tokens Parser_tokens $^
|
|
|
|
pl%gins/cfg/cfg_parser.ml pl%gins/cfg/cfg_parser.mli: src/parser/parser_common.mly plugins/cfg/cfg_parser.mly
|
|
$(SHOW) 'Menhir $^'
|
|
$(HIDE)$(MENHIR) --table --explain --strict --base plugins/cfg/cfg_parser $^
|
|
$(HIDE)for f in plugins/cfg/cfg_parser.mli plugins/cfg/cfg_parser.ml; do (echo "open Why3"; cat $$f) > $$f.new && mv $$f.new $$f; done
|
|
|
|
pl%gins/coma/coma_parser.ml pl%gins/coma/coma_parser.mli: src/parser/parser_common.mly plugins/coma/coma_parser.mly
|
|
$(SHOW) 'Menhir $^'
|
|
$(HIDE)$(MENHIR) --table --explain --strict --base plugins/coma/coma_parser $^
|
|
$(HIDE)for f in plugins/coma/coma_parser.mli plugins/coma/coma_parser.ml; do (echo "open Why3"; cat $$f) > $$f.new && mv $$f.new $$f; done
|
|
|
|
%.ml %.mli: %.mly
|
|
$(SHOW) 'Menhir $<'
|
|
$(HIDE)$(MENHIR) --table --explain --strict $<
|
|
|
|
%.dep: %.ml %.mli
|
|
$(SHOW) 'Ocamldep $<'
|
|
$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(INCLUDES) $< $<i $(TOTARGET)
|
|
|
|
%.dep: %.ml
|
|
$(SHOW) 'Ocamldep $<'
|
|
$(HIDE)($(OCAMLDEP) $(DEPFLAGS) $(INCLUDES) $<; \
|
|
echo '$*.cmx : $*.cmi'; \
|
|
echo '$*.cmi : $*.cmo') $(TOTARGET)
|
|
|
|
%.dep: %.mli
|
|
$(SHOW) 'Ocamldep $<'
|
|
$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(INCLUDES) $< $(TOTARGET)
|
|
|
|
bin/%.opt:
|
|
$(SHOW) 'Linking $@'
|
|
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
|
|
|
|
bin/%.byte:
|
|
$(SHOW) 'Linking $@'
|
|
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
|
|
|
|
# .ml4.ml:
|
|
# $(CAMLP4) pr_o.cmo -impl $< > $@
|
|
|
|
# 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-ocaml=/let[ \t]+\([^ \t]+\)/\1/" \
|
|
"--regex-ocaml=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
|
|
"--regex-ocaml=/and[ \t]+\([^ \t]+\)/\1/" \
|
|
"--regex-ocaml=/type[ \t]+\([^ \t]+\)/\1/" \
|
|
"--regex-ocaml=/exception[ \t]+\([^ \t]+\)/\1/" \
|
|
"--regex-ocaml=/val[ \t]+\([^ \t]+\)/\1/" \
|
|
"--regex-ocaml=/module[ \t]+\([^ \t]+\)/\1/"
|
|
|
|
otags:
|
|
find \( -name '*.ml' -or -name '*.mli' \) -print0 | xargs -0 otags
|
|
# otags src/*.mli src/*.ml c/*.mli c/*.ml intf/*.mli intf/*.ml
|
|
|
|
# the previous seems broken. This one is intented for vi(m) users, but could
|
|
# be adapted for emacs (remove the -vi option ?)
|
|
otags-vi:
|
|
find \( -name '*.ml' -or -name '*.mli' \) -print0 | xargs -0 otags -vi
|
|
|
|
wc:
|
|
ocamlwc -p src/*.ml* src/*/*.ml*
|
|
|
|
#dep: depend
|
|
# cat .depend* | ocamldot | dot -Tpdf > dep.pdf
|
|
# $(PDFVIEWER) dep.pdf
|
|
|
|
# distrib
|
|
#########
|
|
|
|
NAME = why3-@VERSION@
|
|
# see .gitattributes for the list of files that are not distributed
|
|
MORE_DIST = configure
|
|
|
|
dist: $(MORE_DIST)
|
|
rm -f distrib/$(NAME).tar.gz
|
|
mkdir -p distrib/
|
|
git archive --format=tar --prefix=$(NAME)/ -o distrib/$(NAME).tar HEAD
|
|
tar rf distrib/$(NAME).tar --transform="s,^,$(NAME)/," --mtime="$$(date -Iseconds -d "`git show -s --format=%ci` +1 second")" --owner=0 --group=0 $(MORE_DIST)
|
|
gzip -n -f --best distrib/$(NAME).tar
|
|
|
|
|
|
###############
|
|
# file headers
|
|
###############
|
|
|
|
headers:
|
|
headache -c misc/headache_config.txt -h misc/header.txt \
|
|
Makefile.in configure.in \
|
|
src/*/*.ml src/*/*.ml[ily] \
|
|
plugins/*/*.ml plugins/*/*.ml[ily] \
|
|
lib/coq/*.v lib/coq/*/*.v \
|
|
src/server/*.[ch] \
|
|
examples/use_api/*.ml
|
|
|
|
#########
|
|
# myself
|
|
#########
|
|
|
|
AUTOCONF_FILES = \
|
|
Makefile \
|
|
src/jessie/Makefile \
|
|
src/config.sh \
|
|
.merlin \
|
|
src/jessie/.merlin \
|
|
lib/why3/META \
|
|
lib/coq/version \
|
|
lib/pvs/version
|
|
|
|
$(AUTOCONF_FILES): %: %.in config.status
|
|
./config.status chmod --file $@
|
|
|
|
src/util/config.ml share/Makefile.config: src/config.sh
|
|
$(SHOW) 'Generate $@'
|
|
$(HIDE)BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
|
|
|
|
clean::
|
|
rm -f share/Makefile.config
|
|
|
|
config.status: configure
|
|
./config.status --recheck
|
|
|
|
configure: configure.in
|
|
autoconf -f
|
|
|
|
###################
|
|
# clean and depend
|
|
###################
|
|
|
|
.PHONY: distclean
|
|
|
|
distclean: clean
|
|
rm -f config.status config.cache config.log \
|
|
src/util/config.ml $(AUTOCONF_FILES)
|
|
|
|
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
|
|
ifneq "$(MAKECMDGOALS)" "depend"
|
|
-include $(MAKEINC)
|
|
endif
|
|
endif
|
|
|
|
depend: $(MAKEINC)
|
|
|
|
clean::
|
|
rm -f $(GENERATED)
|
|
$(foreach d,$(CLEANDIRS),rm -f $(addprefix $(d)/*.,$(COMPILED_LIB_EXTS));)
|
|
$(foreach p,$(CLEANLIBS),rm -f $(addprefix $(p).,$(COMPILED_LIB_EXTS));)
|
|
|
|
detect-unused:
|
|
@L1=$$(mktemp); \
|
|
L2=$$(mktemp); \
|
|
for d in `find examples/ -name 'why3session.xml' -printf '%h\n'`; do \
|
|
sed -n -e 's/.*proof.*name="\([^"]*\)".*/\1/p' $$d/why3session.xml | sort > $$L1; \
|
|
(cd $$d; git ls-files) | grep -v -e '^why3session.xml' -e '^why3shapes' -e '^[.]gitignore' -e '^Makefile' -e '[.]ml$$' -e '[.]html$$' | sed -e 's/[.]prf$$/.pvs/;s/[.]thy$$/.xml/' | sort -u > $$L2; \
|
|
diff -u --label="$$d/why3session.xml" --label="$$d/" $$L1 $$L2 || echo; \
|
|
done; \
|
|
rm $$L1 $$L2
|
|
|
|
##################################################################
|
|
# Building the Why3 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.
|