no more why3ml executable

parent e8374d94
......@@ -47,9 +47,6 @@ why3.conf
/bin/why3.byte
/bin/why3.opt
/bin/why3
/bin/why3ml.byte
/bin/why3ml.opt
/bin/why3ml
/bin/why3ide.byte
/bin/why3ide.opt
/bin/why3ide
......
* marks an incompatible change
* no more executable why3ml (why3 now handles WhyML files)
o [Provers] support for Z3 4.0
o [Sessions] a small change in the format. Why3 is still able to
read session files in the old format.
......
......@@ -359,35 +359,33 @@ install_no_local::
cp -f lib/plugins/* $(LIBDIR)/why3/plugins
##################
# Why binary
##################
########
# Whyml (old API)
########
byte: bin/why3.byte
opt: bin/why3.opt
PGM_FILES = pgm_ttree pgm_types pgm_pretty \
pgm_module pgm_wp pgm_typing pgm_ocaml pgm_main
bin/why3.opt: src/why3.cmxa src/main.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
bin/why3.byte: src/why3.cma src/main.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
PGMDEP = $(addsuffix .dep, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))
bin/why3: bin/why3.@OCAMLBEST@
ln -sf why3.@OCAMLBEST@ $@
$(PGMDEP): DEPFLAGS += -I src/programs
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
src/main.cmo: src/why3.cma
src/main.cmx: src/why3.cmxa
# depend and clean targets
clean::
rm -f src/main.cm[iox] src/main.annot src/main.o
rm -f bin/why3.byte bin/why3.opt bin/why3
ifneq "$(MAKECMDGOALS)" "clean"
include $(PGMDEP)
endif
install_no_local::
cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
depend: $(PGMDEP)
install_local: bin/why3
clean::
rm -f src/programs/*.cm[iox] src/programs/*.o
rm -f src/programs/*.annot src/programs/*.dep src/programs/*~
########
# Whyml (new API)
......@@ -405,11 +403,6 @@ MLWCMX = $(addsuffix .cmx, $(MLWMODULES))
$(MLWDEP): DEPFLAGS += -I src/whyml
$(MLWCMO) $(MLWCMX): INCLUDES += -I src/whyml
# build targets
byte: $(MLWCMO)
opt: $(MLWCMX)
# depend and clean targets
ifneq "$(MAKECMDGOALS)" "clean"
......@@ -421,60 +414,47 @@ depend: $(MLWDEP)
clean::
rm -f src/whyml/*.cm[iox] src/whyml/*.o
rm -f src/whyml/*.annot src/whyml/*.dep src/whyml/*~
# rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
########
# Whyml
########
PGM_FILES = pgm_ttree pgm_types pgm_pretty \
pgm_module pgm_wp pgm_typing pgm_ocaml pgm_main
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
PGMDEP = $(addsuffix .dep, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))
######
# Why3
######
$(PGMDEP): DEPFLAGS += -I src/programs
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
# build targets
src/main.cmo: src/why3.cma
src/main.cmx: src/why3.cmxa
byte: bin/why3ml.byte
opt: bin/why3ml.opt
byte: bin/why3.byte
opt: bin/why3.opt
bin/why3ml.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) src/main.cmx
bin/why3.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) src/main.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3ml.byte: src/why3.cma $(PGMCMO) $(MLWCMO) src/main.cmo
bin/why3.byte: src/why3.cma $(PGMCMO) $(MLWCMO) src/main.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3ml: bin/why3ml.@OCAMLBEST@
ln -sf why3ml.@OCAMLBEST@ $@
# depend and clean targets
bin/why3: bin/why3.@OCAMLBEST@
ln -sf why3.@OCAMLBEST@ $@
ifneq "$(MAKECMDGOALS)" "clean"
include $(PGMDEP)
endif
install_no_local::
cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
depend: $(PGMDEP)
install_local: bin/why3
clean::
rm -f src/programs/*.cm[iox] src/programs/*.o
rm -f src/programs/*.annot src/programs/*.dep src/programs/*~
rm -f src/main.cm[iox] src/main.annot src/main.o
rm -f bin/why3.byte bin/why3.opt bin/why3
rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
# test target
##############
# test targets
##############
%.gui: %.why bin/why3ide.opt
bin/why3ide.opt $*.why
%: %.mlw bin/why3ml.opt
bin/why3ml.opt $*.mlw
%: %.mlw bin/why3.opt
bin/why3.opt $*.mlw
%: %.why bin/why3.opt
bin/why3.opt $*.why
......@@ -483,12 +463,7 @@ clean::
bin/why3ide.opt $*.mlw
%.type: %.mlw bin/why3ide.opt
bin/why3ml.opt --type-only $*.mlw
install_no_local::
cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml$(EXE)
install_local: bin/why3ml
bin/why3.opt --type-only $*.mlw
##########
# gallery
......@@ -1122,9 +1097,9 @@ install_local: bin/why3doc
.PHONY: bench test
bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
$(MAKE) test-api.@OCAMLBEST@
sh bench/bench "bin/why3.@OCAMLBEST@" "bin/why3ml.@OCAMLBEST@"
sh bench/bench "bin/why3.@OCAMLBEST@"
@if test "@enable_coq_plugin@" = "yes"; then \
echo "=== checking the Coq tactic ==="; \
$(MAKE) test-coq-tactic.@OCAMLBEST@; fi
......@@ -1155,18 +1130,18 @@ test: bin/why3.byte plugins.byte $(TOOLS)
@printf "*** Checking Coq compilation ***\\n"
@for i in output_coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done
testl: bin/why3ml.byte
ocamlrun -bt bin/why3ml.byte tests/test-pgm-jcf.mlw
ocamlrun -bt bin/why3ml.byte -P alt-ergo tests/test-pgm-jcf.mlw
testl: bin/why3.byte
ocamlrun -bt bin/why3.byte tests/test-pgm-jcf.mlw
ocamlrun -bt bin/why3.byte -P alt-ergo tests/test-pgm-jcf.mlw
testl-debug: bin/why3ml.opt
bin/why3ml.opt --debug program_typing tests/test-pgm-jcf.mlw
testl-debug: bin/why3.opt
bin/why3.opt --debug program_typing tests/test-pgm-jcf.mlw
testl-ide: bin/why3ide.opt
bin/why3ide.opt tests/test-pgm-jcf.mlw
testl-type: bin/why3ml.byte
ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
testl-type: bin/why3.byte
ocamlrun -bt bin/why3.byte --type-only tests/test-pgm-jcf.mlw
test-api.byte: examples/use_api.ml src/why3.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \
......
......@@ -133,3 +133,12 @@ tools
Andrei: isn't this done?
- Maybe : make something generic for the dialog box with memory.
provers
-------
- PVS: use a better name for PVS theory when printing a task, e.g.
file_theory_goal. Solution: do that when we have idents with origin
information (necessary for parsing a task).
......@@ -9,7 +9,7 @@
export WHY3LOADPATH=theories
pgm=$1
pgml=$2
pgml=$1
pgml_options=
goods () {
......
......@@ -2,7 +2,7 @@
% \newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
\newcommand{\why}{\textsf{Why3}\xspace}
\newcommand{\whyml}{\textsf{Why3ML}\xspace}
\newcommand{\whyml}{\textsf{WhyML}\xspace}
\newcommand{\eg}{\emph{e.g.}\xspace}
\newcommand{\ie}{\emph{i.e.}\xspace}
......
......@@ -6,10 +6,10 @@ provided by the \why environment. These are as follows:
\begin{description}
\item[\texttt{why3config}] tool for managing the user's configuration,
including the detection of installed provers.
\item[\texttt{why3}] reads \why input files and call provers, on the command-line
\item[\texttt{why3}] reads \why\ and \whyml input files and calls
provers, on the command-line.
\item[\texttt{why3ide}] graphical interface to display goals, run
provers and transformations on them.
\item[\texttt{why3ml}] as \texttt{why3} but reads \whyml programs instead
\item[\texttt{why3replayer}] replay the proofs stored in a session,
for regression test purposes
\item[\texttt{why3bench}] produces benchmarks.
......@@ -103,8 +103,9 @@ can be obtained by the option \verb|--list-prover-ids|.
\label{sec:why3ref}
\why is primarily used to call provers on goals contained in an
input file. By default, such a file must be written in \why language
and have the extension \texttt{.why}. However, a dynamically loaded
input file. By default, such a file must be written either in \why language
(extension \texttt{.why}) or in \whyml language (extension \texttt{.mlw}).
However, a dynamically loaded
plugin can register a parser for some other format of logical problems,
\eg{} TPTP or SMTlib.
......@@ -120,6 +121,8 @@ The \texttt{why3} tool executes the following steps:
the filename extension or the \verb|--format| option to choose
among the available parsers. The \verb|--list-format| option gives
the list of registered parsers.
\whyml modules are turned into
theories containing verification conditions as goals.
\item Extract the selected goals inside each of the selected theories
into tasks. The goals and theories are selected using the options
\verb|-G/--goal| and \verb|-T/--theory|. The option
......@@ -316,22 +319,6 @@ are groups together under several tabs
decision by clicking on it.
\end{description}
\section{The \texttt{why3ml} tool}
The \texttt{why3ml} tool is a layer on top of the \why library for
generating verification conditions from \whyml programs.
The command-line of \texttt{why3ml} is identical to that of
\texttt{why3}, but also accepts files with extension \texttt{.mlw} as
input files containing \whyml modules (see Chapter~\ref{chap:whyml}
and Section~\ref{sec:syntax:whyml}). Modules are turned into
theories containing verification conditions as goals, and then
\texttt{why3ml} behaves exactly as \texttt{why3} for the remaining of
the process.
Note that files with extension \texttt{.mlw} can also be loaded in
\texttt{why3ide}.
For those who want to experiment with \whyml, many examples are provided in
\texttt{examples/programs}.
\section{The \texttt{why3bench} tool}
......
......@@ -166,7 +166,7 @@ A \why input file is a (possibly empty) list of theories.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\clearpage
\section{Why3ML Language}\label{sec:syntax:whyml}
\section{WhyML Language}\label{sec:syntax:whyml}
\subsection{Types}
......
\chapter{The Why3ML Programming Language}
\chapter{The WhyML Programming Language}
\label{chap:whyml}
This chapter describes the \whyml programming language.
......@@ -32,15 +32,14 @@ They also provide extra features:
\end{itemize}
%
Programs are contained in files with suffix \verb|.mlw|.
They are handled by the tool \texttt{why3ml}, which has a command line
similar to \texttt{why3}. For instance
They are handled by \texttt{why3}. For instance
\begin{verbatim}
% why3ml myfile.mlw
% why3 myfile.mlw
\end{verbatim}
will display the verification conditions extracted from modules in
file \texttt{myfile.mlw}, as a set of corresponding theories, and
\begin{verbatim}
% why3ml -P alt-ergo myfile.mlw
% why3 -P alt-ergo myfile.mlw
\end{verbatim}
will run the SMT solver Alt-Ergo on these verification conditions.
Program files are also handled by the GUI tool \texttt{why3ide}.
......@@ -178,7 +177,7 @@ end
\label{fig:MaxAndSum}
\end{figure}
We can now proceed to its verification.
Running \texttt{why3ml}, or better \texttt{why3ide}, on file
Running \texttt{why3}, or better \texttt{why3ide}, on file
\verb|max_sum.mlw| will show a single verification condition with name
\verb|WP_parameter_max_sum|.
Discharging this verification condition with an automated theorem
......
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