Commit 916f3ac3 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Provide a why3-coq opam package containing the tactic and the realizations.

parent 1b4bd864
......@@ -163,8 +163,9 @@ endif
.PHONY: install-bash install-emacs install-framac
.PHONY: uninstall-bash uninstall-emacs uninstall-framac
.PHONY: ide install-ide uninstall-ide
.PHONY: coq install-coq-tactic install-coq install-coq-data
.PHONY: pvs install-pvs install-pvs-data
.PHONY: coq install-coq uninstall-coq
.PHONY: coq-tactic install-coq-tactic uninstall-coq-tactic
.PHONY: pvs install-pvs uninstall-pvs
.PHONY: install-isabelle
.PHONY: plugins plugins.byte plugins.opt
......@@ -961,11 +962,11 @@ $(COQPDEP): $(COQPGENERATED)
byte: lib/coq-tactic/why3tac.cma
opt: lib/coq-tactic/why3tac.cmxs
lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmxa, @ZIPLIB@)
lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmx, @MENHIRLIB@)
lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmxa, @ZIPLIB@ @WHY3LIB@)
lib/coq-tactic/why3tac.cma: BFLAGS += $(addsuffix .cma, @ZIPLIB@)
lib/coq-tactic/why3tac.cma: BFLAGS += $(addsuffix .cmo, @MENHIRLIB@)
lib/coq-tactic/why3tac.cma: BFLAGS += $(addsuffix .cma, @ZIPLIB@ @WHY3LIB@)
lib/coq-tactic/why3tac.cmxs: $(WHY3CMXA) $(COQPCMX)
lib/coq-tactic/why3tac.cma: $(WHY3CMA) $(COQPCMO)
......@@ -987,7 +988,9 @@ lib/coq-tactic/Why3.vo: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/
$(SHOW) 'Coqc $<'
$(HIDE)WHY3CONFIG="" $(COQC) $(COQRTAC) $<
all: lib/coq-tactic/Why3.vo
coq-tactic: lib/coq-tactic/Why3.vo
all: coq-tactic
# depend and clean targets
......@@ -1004,6 +1007,9 @@ GENERATED += $(COQPGENERATED)
clean::
rm -f lib/coq-tactic/*.vo lib/coq-tactic/*.glob
uninstall-coq-tactic:
rm -rf $(LIBDIR)/why3/coq-tactic
install-coq-tactic:
$(MKDIR_P) $(LIBDIR)/why3/coq-tactic
$(INSTALL_DATA) lib/coq-tactic/Why3.vo lib/coq-tactic/why3tac.$(COQTACEXT) $(LIBDIR)/why3/coq-tactic
......@@ -1083,6 +1089,25 @@ endif
COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_SEQ) $(COQLIBS_FP) $(COQLIBS_BV) $(COQLIBS_IEEEFLOAT)
%.vo: %.v
$(SHOW) 'Coqc $<'
$(HIDE)$(COQC) -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
clean-coq:
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
clean:: clean-coq
drivers/coq-realizations.aux: Makefile
$(SHOW) 'Generate $@'
$(HIDE)(echo "(* generated automatically at compilation time *)"; \
......@@ -1152,11 +1177,11 @@ update-coq-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux
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
ifeq (@enable_coq_support@,yes)
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/
......@@ -1187,25 +1212,11 @@ ifeq (@enable_coq_fp_libs@,yes)
$(MKDIR_P) $(LIBDIR)/why3/coq/ieee_float
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_IEEEFLOAT)) $(LIBDIR)/why3/coq/ieee_float/
endif
$(MKDIR_P) $(DATADIR)/why3/drivers
$(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
install:: install-coq
endif
COQV = $(addsuffix .v, $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
%.vo: %.v
$(SHOW) 'Coqc $<'
$(HIDE)$(COQC) -R lib/coq Why3 $<
%.vd: %.v
$(SHOW) 'Coqdep $<'
$(HIDE)$(COQDEP) -R lib/coq Why3 $< $(TOTARGET)
coq: $(COQVO)
all: coq
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
......@@ -1216,19 +1227,13 @@ endif
depend: $(COQVD)
clean-coq:
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
clean:: clean-coq
endif
all: drivers/coq-realizations.aux
install-coq-data:
install-data::
$(MKDIR_P) $(DATADIR)/why3/drivers
$(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
install-data:: install-coq-data
all: drivers/coq-realizations.aux
clean::
rm -f drivers/coq-realizations.aux
......@@ -1279,6 +1284,9 @@ drivers/pvs-realizations.aux: Makefile
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
) > $@
uninstall-pvs:
rm -rf $(LIBDIR)/why3/pvs
install-pvs:
$(MKDIR_P) $(LIBDIR)/why3/pvs
$(INSTALL_DATA) lib/pvs/version $(LIBDIR)/why3/pvs/
......@@ -1290,6 +1298,7 @@ install-pvs:
$(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
......@@ -1309,11 +1318,10 @@ drivers/pvs-realizations.aux: Makefile
endif
install-pvs-data:
install-data::
$(MKDIR_P) $(DATADIR)/why3/drivers/
$(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
install-data:: install-pvs-data
all: drivers/pvs-realizations.aux
clean::
......
Why3 environment for deductive program verification.
Why3 provides a rich language for specification and programming, called
WhyML, and relies on external theorem provers, both automated and
interactive, to discharge verification conditions. Why3 comes with a
standard library of logical theories (integer and real arithmetic,
Boolean operations, sets and maps, etc.) and basic programming data
structures (arrays, queues, hash tables, etc.). A user can write WhyML
programs directly and get correct-by-construction OCaml programs
through an automated extraction mechanism. WhyML is also used as an
intermediate language for the verification of C, Java, or Ada
programs.
Why3 is a complete reimplementation of the former Why platform. Among
the new features are: numerous extensions to the input language, a new
architecture for calling external provers, and a well-designed API,
allowing to use Why3 as a software library. An important emphasis is
put on modularity and genericity, giving the end user a possibility to
easily reuse Why3 formalizations or to add support for a new external
prover if wanted.
This package provides the Coq realizations of Why3 theories.
opam-version: "1.2"
maintainer: "guillaume.melquiond@inria.fr"
authors: [
"François Bobot"
"Jean-Christophe Filliâtre"
"Claude Marché"
"Guillaume Melquiond"
"Andrei Paskevich"
]
homepage: "http://why3.lri.fr/"
license: "GNU Lesser General Public License version 2.1"
doc: "http://why3.lri.fr/doc/"
bug-reports: "https://gitlab.inria.fr/why3/why3/issues"
dev-repo: "https://gitlab.inria.fr/why3/why3.git"
tags: [
"deductive"
"program verification"
"formal specification"
"automated theorem prover"
"interactive theorem prover"
]
available: [ ocaml-version >= "4.02.3" ]
build: [
["autoconf"]
["dash" "-c" "automake --add-missing || true"]
["./configure"
"--prefix" prefix
"--disable-why3-lib"
"--disable-frama-c"
"--disable-ide"
"--disable-js-of-ocaml"]
[make "-j%{jobs}%" "coq" "coq-tactic"]
]
install: [make "install-coq" "install-coq-tactic"]
remove: ["rm" "-rf" "%{lib}%/why3/coq"]
flags: [ light-uninstall ]
depends: [
"ocamlfind" {build}
"why3"
"coq"
]
conflicts: [
"coq" {< "8.4"}
"coq" {>= "8.8"}
]
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