Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
120
Issues
120
List
Boards
Labels
Service Desk
Milestones
Merge Requests
17
Merge Requests
17
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
f44ea070
Commit
f44ea070
authored
Jun 16, 2014
by
Guillaume Melquiond
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Change why3replayer into why3replay, so as to match other commands.
parent
0285a2ab
Changes
12
Hide whitespace changes
Inline
Side-by-side
Showing
12 changed files
with
51 additions
and
159 deletions
+51
-159
.gitignore
.gitignore
+3
-3
Makefile.in
Makefile.in
+15
-55
check.sh
check.sh
+1
-1
doc/coq_tactic.tex
doc/coq_tactic.tex
+1
-1
doc/install.tex
doc/install.tex
+3
-5
doc/manpages.tex
doc/manpages.tex
+5
-5
doc/starting.tex
doc/starting.tex
+2
-2
examples/bench.sh
examples/bench.sh
+1
-1
examples/regtests.sh
examples/regtests.sh
+1
-1
examples/vacid_0_binary_heaps/Makefile
examples/vacid_0_binary_heaps/Makefile
+0
-4
share/bash/why3
share/bash/why3
+3
-3
src/tools/why3replay.ml
src/tools/why3replay.ml
+16
-78
No files found.
.gitignore
View file @
f44ea070
...
...
@@ -78,9 +78,9 @@ why3.conf
/bin/why3realize.byte
/bin/why3realize.opt
/bin/why3realize
/bin/why3replay
er
.byte
/bin/why3replay
er
.opt
/bin/why3replay
er
/bin/why3replay.byte
/bin/why3replay.opt
/bin/why3replay
/bin/why3session.opt
/bin/why3session.byte
/bin/why3session
...
...
Makefile.in
View file @
f44ea070
...
...
@@ -481,7 +481,7 @@ clean::
# Why3 commands
###############
TOOLS_BIN
=
why3execute why3extract why3prove why3realize
TOOLS_BIN
=
why3execute why3extract why3prove why3realize
why3replay
TOOLS_FILES
=
args
$(TOOLS_BIN)
TOOLSMODULES
=
$(
addprefix
src/tools/,
$(TOOLS_FILES)
)
...
...
@@ -540,6 +540,17 @@ bin/why3realize.byte: lib/why3/why3.cma src/tools/args.cmo src/tools/why3realize
bin/why3realize
:
bin/why3realize.@OCAMLBEST@
ln
-sf
why3realize.@OCAMLBEST@
$@
bin/why3replay.opt
:
lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3replay.cmx
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLOPT)
$(OFLAGS)
-o
$@
$(OLINKFLAGS)
$^
bin/why3replay.byte
:
lib/why3/why3.cma src/tools/args.cmo src/tools/why3replay.cmo
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLC)
$(BFLAGS)
-o
$@
$(BLINKFLAGS)
$^
bin/why3replay
:
bin/why3replay.@OCAMLBEST@
ln
-sf
why3replay.@OCAMLBEST@
$@
clean_old_install
::
rm
-f
$
(
TOOLS_BIN:%
=
$(TOOLDIR)
/%
$(EXE)
)
...
...
@@ -548,6 +559,7 @@ install_no_local::
cp
-f
bin/why3extract.@OCAMLBEST@
$(TOOLDIR)
/why3extract
$(EXE)
cp
-f
bin/why3prove.@OCAMLBEST@
$(TOOLDIR)
/why3prove
$(EXE)
cp
-f
bin/why3realize.@OCAMLBEST@
$(TOOLDIR)
/why3realize
$(EXE)
cp
-f
bin/why3replay.@OCAMLBEST@
$(TOOLDIR)
/why3replay
$(EXE)
install_local
:
$(addprefix bin/
,
$(TOOLS_BIN))
...
...
@@ -563,10 +575,12 @@ clean::
rm
-f
src/tools/why3extract.cm[iox] src/tools/why3extract.annot src/tools/why3extract.o src/tools/why3extract.dep
rm
-f
src/tools/why3prove.cm[iox] src/tools/why3prove.annot src/tools/why3prove.o src/tools/why3prove.dep
rm
-f
src/tools/why3realize.cm[iox] src/tools/why3realize.annot src/tools/why3realize.o src/tools/why3realize.dep
rm
-f
src/tools/why3replay.cm[iox] src/tools/why3replay.annot src/tools/why3replay.o src/tools/why3replay.dep
rm
-f
bin/why3execute.byte bin/why3execute.opt bin/why3execute
rm
-f
bin/why3extract.byte bin/why3extract.opt bin/why3extract
rm
-f
bin/why3prove.byte bin/why3prove.opt bin/why3prove
rm
-f
bin/why3realize.byte bin/why3realize.opt bin/why3realize
rm
-f
bin/why3replay.byte bin/why3replay.opt bin/why3replay
##############
# test targets
...
...
@@ -758,60 +772,6 @@ install_local: bin/why3ide
endif
###############
# Replayer
###############
REPLAYER_FILES
=
replay
REPLAYERMODULES
=
$(
addprefix
src/why3replayer/,
$(REPLAYER_FILES)
)
REPLAYERDEP
=
$(
addsuffix
.dep,
$(REPLAYERMODULES)
)
REPLAYERCMO
=
$(
addsuffix
.cmo,
$(REPLAYERMODULES)
)
REPLAYERCMX
=
$(
addsuffix
.cmx,
$(REPLAYERMODULES)
)
$(REPLAYERDEP)
:
DEPFLAGS += -I src/why3replayer
$(REPLAYERCMO) $(REPLAYERCMX)
:
INCLUDES += -I src/why3replayer
# build targets
byte
:
bin/why3replayer.byte
opt
:
bin/why3replayer.opt
bin/why3replayer.opt
:
lib/why3/why3.cmxa $(REPLAYERCMX)
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLOPT)
$(OFLAGS)
-o
$@
$(OLINKFLAGS)
$^
bin/why3replayer.byte
:
lib/why3/why3.cma $(REPLAYERCMO)
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
\
$(OCAMLC)
$(BFLAGS)
-o
$@
$(BLINKFLAGS)
$^
bin/why3replayer
:
bin/why3replayer.@OCAMLBEST@
ln
-sf
why3replayer.@OCAMLBEST@
$@
# depend and clean targets
ifneq
"$(MAKECMDGOALS)" "clean"
include
$(REPLAYERDEP)
endif
depend
:
$(REPLAYERDEP)
clean
::
rm
-f
src/why3replayer/
*
.cm[iox] src/why3replayer/
*
.o
rm
-f
src/why3replayer/
*
.annot src/why3replayer/
*
.dep src/why3replayer/
*
~
rm
-f
bin/why3replayer.byte bin/why3replayer.opt bin/why3replayer
clean_old_install
::
rm
-f
$(BINDIR)
/why3replayer
$(EXE)
install_no_local
::
cp
-f
bin/why3replayer.@OCAMLBEST@
$(TOOLDIR)
/why3replayer
$(EXE)
install_local
:
bin/why3replayer
###############
# Session
###############
...
...
check.sh
View file @
f44ea070
# useful script for git bisect
make
||
exit
125
;
bin/why3config
--detect
&&
bin/why3replay
er examples/bellman_ford.mlw
make
||
exit
125
;
bin/why3config
--detect
&&
bin/why3replay
examples/bellman_ford.mlw
doc/coq_tactic.tex
View file @
f44ea070
...
...
@@ -14,7 +14,7 @@ The Coq tactic is installed in
where
\textit
{
why3-lib-dir
}
is
\why
's library directory, as reported
by
\verb
+
why3 --print-libdir
+
. This directory
is automatically added to Coq's load path if you are
calling Coq via
\why
(from
\texttt
{
why3ide
}
,
\texttt
{
why3replay
er
}
,
calling Coq via
\why
(from
\texttt
{
why3ide
}
,
\texttt
{
why3replay
}
,
etc.). If you are calling Coq by yourself, you need to add
this directory to Coq's load path, either using Coq's command line
option
\texttt
{
-I
}
or by adding
...
...
doc/install.tex
View file @
f44ea070
...
...
@@ -78,14 +78,12 @@ Installation can be tested as follows:
obtain the following:
\begin{verbatim}
$
cd examples
$
why3replayer scottish-private-club
Info: found directory 'scottish-private-club' for the project
$
why3 replay logic/scottish-private-club
Opening session... done
Progress: 4/4
1/1
Everything OK.
$
why
3
replayer programs
/
same
_
fringe
Info: found directory 'programs
/
same
_
fringe' for the project
$
why
3
replay programs
/
same
_
fringe
Opening session... done
Progress:
12
/
12
3
/
3
...
...
@@ -177,7 +175,7 @@ each prover, in the \why configuration file. Within the GUI, you can
discard these choices via the
\textsf
{
Preferences
}
dialog.
Outside the GUI, the prover upgrades are handled as follows. The
\texttt
{
replay
er
}
command will just ignore proof attempts marked as
\texttt
{
replay
}
command will just ignore proof attempts marked as
archived
\index
{
archived
}
.
Conversely, a non
-
archived proof attempt with a non
-
existent
prover will be reported as a replay failure. The
...
...
doc/manpages.tex
View file @
f44ea070
...
...
@@ -449,7 +449,7 @@ each component to compare. Various formats can be used as outputs:
represented in an array; the rows correspond to the
compared components, the columns correspond to the result
(Valid, Unknown, Timeout, Failure, Invalid) and the CPU time taken in seconds.
\item
average:
summarizes the number of the five different answers
\item
[\texttt{average}]
it
summarizes the number of the five different answers
for each component. It also gives the average time taken.
\item
[\texttt{timeline}]
for each component, it gives the number of valid goals
along the time (10 slices between 0 and the longest time a component
...
...
@@ -513,19 +513,19 @@ One can run all the bench given in one bench configuration file with
why3 bench -B path
_
to
_
my
_
bench.rc
\end{verbatim}
\section
{
The
\texttt
{
replay
er
}
Command
}
\section
{
The
\texttt
{
replay
}
Command
}
\label
{
sec:why3replayer
}
The
\texttt
{
replay
er
}
command is meant to execute the proofs
The
\texttt
{
replay
}
command is meant to execute the proofs
stored in a
\why
session file, as produced by the IDE. Its
main purpose is to play non-regression tests. For instance,
\texttt
{
examples/regtests.sh
}
is a script that runs regression tests on
all the examples.
\index
{
replay
er@
\texttt
{
replayer
}}
\index
{
replay
@
\texttt
{
replay
}}
The tool is invoked in a terminal or a script using
\begin{flushleft}
\ttfamily
why3 replay
er
\textsl
{
[options] <project directory>
}
why3 replay
\textsl
{
[options] <project directory>
}
\end{flushleft}
The session file
\texttt
{
why3session.xml
}
stored in the given
directory is loaded and all the proofs it contains are rerun. Then,
...
...
doc/starting.tex
View file @
f44ea070
...
...
@@ -190,12 +190,12 @@ you must select the context \textsf{all goals} at the top of the left
tool bar.
Notice that replaying can be done in batch mode, using the
\texttt
{
replay
er
}
command (see Section~
\ref
{
sec:why3replayer
}
) For
\texttt
{
replay
}
command (see Section~
\ref
{
sec:why3replayer
}
) For
example, running the replayer on the
\texttt
{
hello
\_
proof
}
example is
as follows (assuming
$
G
_
2
$
still is
\lstinline
|(true -> false) /
\
(true
\/
false)|).
\begin{verbatim}
$
why
3
replay
er
hello
_
proof
$
why
3
replay hello
_
proof
Info: found directory 'hello
_
proof' for the project
Opening session...
[
Xml warning
]
prolog ignored
[
Reload
]
file '..
/
hello
_
proof.why'
...
...
examples/bench.sh
View file @
f44ea070
...
...
@@ -23,7 +23,7 @@ run_dir () {
d
=
`
dirname
$f
`
b
=
`
basename
$d
`
echo
-n
"Benchmarking
$d
... "
../bin/why3replay
er
.opt
-bench
$REPLAYOPT
$2
$d
2>
$TMPERR
>
$TMP
../bin/why3replay.opt
-bench
$REPLAYOPT
$2
$d
2>
$TMPERR
>
$TMP
ret
=
$?
if
test
"
$ret
"
!=
"0"
;
then
echo
-n
"FAILED (ret code=
$ret
):"
...
...
examples/regtests.sh
View file @
f44ea070
...
...
@@ -38,7 +38,7 @@ run_dir () {
for
f
in
`
ls
$1
/
*
/why3session.xml
`
;
do
d
=
`
dirname
$f
`
echo
-n
"Replaying
$d
... "
../bin/why3replay
er
.opt
-q
$REPLAYOPT
$2
$d
2>
$TMPERR
>
$TMP
../bin/why3replay.opt
-q
$REPLAYOPT
$2
$d
2>
$TMPERR
>
$TMP
ret
=
$?
if
test
"
$ret
"
!=
"0"
;
then
echo
-n
"FAILED (ret code=
$ret
):"
...
...
examples/vacid_0_binary_heaps/Makefile
deleted
100644 → 0
View file @
0285a2ab
replay
:
why3replayer
-I
.
proofs
share/bash/why3
View file @
f44ea070
...
...
@@ -122,9 +122,9 @@ _why3()
esac
} && complete -F _why3 \
why3 why3ml why3ide why3config why3doc why3replay
er
why3session \
why3 why3ml why3ide why3config why3doc why3replay why3session \
why3.opt why3ml.opt why3ide.opt why3config.opt why3doc.opt \
why3replay
er
.opt why3session.opt \
why3replay.opt why3session.opt \
why3.byte why3ml.byte why3ide.byte why3config.byte why3doc.byte \
why3replay
er
.byte why3session.byte
why3replay.byte why3session.byte
src/
why3replayer/
replay.ml
→
src/
tools/why3
replay.ml
View file @
f44ea070
...
...
@@ -35,9 +35,7 @@ let debug = Debug.register_info_flag
let
()
=
Debug
.
set_flag
debug
let
includes
=
ref
[]
let
file
=
ref
None
let
opt_version
=
ref
false
let
opt_file
=
ref
None
let
opt_stats
=
ref
true
let
opt_force
=
ref
false
let
opt_obsolete_only
=
ref
false
...
...
@@ -63,25 +61,11 @@ let set_opt_smoke = function
|
"deep"
->
opt_smoke
:=
SD_Deep
|
_
->
assert
false
let
opt_config
=
ref
None
let
opt_extra
=
ref
[]
let
spec
=
Arg
.
align
[
(
"-L"
,
Arg
.
String
(
fun
s
->
includes
:=
s
::
!
includes
)
,
"<s> add s to loadpath"
)
;
(
"--library"
,
Arg
.
String
(
fun
s
->
includes
:=
s
::
!
includes
)
,
" same as -L"
)
;
(
"-I"
,
Arg
.
String
(
fun
s
->
includes
:=
s
::
!
includes
)
,
" same as -L (obsolete)"
)
;
(
"-C"
,
Arg
.
String
(
fun
s
->
opt_config
:=
Some
s
)
,
"<file> Read configuration from <file>"
)
;
(
"--config"
,
Arg
.
String
(
fun
s
->
opt_config
:=
Some
s
)
,
" same as -C"
)
;
(
"--extra-config"
,
Arg
.
String
(
fun
s
->
opt_extra
:=
!
opt_extra
@
[
s
])
,
"<file> Read additional configuration from <file>"
)
;
let
usage_msg
=
Format
.
sprintf
"Usage: %s [options] [<file.why>|<project directory>]"
(
Filename
.
basename
Sys
.
argv
.
(
0
))
let
option_list
=
[
(
"--force"
,
Arg
.
Set
opt_force
,
" enforce saving the session after replay"
)
;
...
...
@@ -102,45 +86,16 @@ let spec = Arg.align [
" do not print statistics"
)
;
(
"-q"
,
Arg
.
Unit
(
fun
()
->
Debug
.
unset_flag
debug
)
,
" run quietly"
)
;
(
"-v"
,
Arg
.
Unit
(
fun
()
->
Debug
.
set_flag
debug
)
,
" print version information"
)
;
(*
"--convert-unknown-provers", Arg.Set opt_convert_unknown_provers,
" try to find compatible provers for all unknown provers";
*)
Debug
.
Args
.
desc_debug_list
;
Debug
.
Args
.
desc_shortcut
"parse_only"
"--parse-only"
" Stop after parsing"
;
Debug
.
Args
.
desc_shortcut
"type_only"
"--type-only"
" Stop after type checking"
;
Debug
.
Args
.
desc_debug_all
;
Debug
.
Args
.
desc_debug
;
]
" run quietly"
)
]
let
version_msg
=
Format
.
sprintf
"Why3 replayer, version %s (build date: %s)"
Config
.
version
Config
.
builddate
let
usage_str
=
Format
.
sprintf
"Usage: %s [options] [<file.why>|<project directory>]"
(
Filename
.
basename
Sys
.
argv
.
(
0
))
let
set_file
f
=
match
!
file
with
let
add_opt_file
f
=
match
!
opt_file
with
|
Some
_
->
raise
(
Arg
.
Bad
"only one parameter"
)
|
None
->
file
:=
Some
f
opt_
file
:=
Some
f
let
()
=
Arg
.
parse
spec
set_file
usage_str
let
()
=
if
!
opt_version
then
begin
Format
.
printf
"%s@."
version_msg
;
exit
0
end
let
()
=
if
Debug
.
Args
.
option_list
()
then
exit
0
let
(
env
,
config
)
=
Args
.
initialize
option_list
add_opt_file
usage_msg
(* let () = *)
(* if !opt_smoke <> Session.SD_None && !opt_force then begin *)
...
...
@@ -148,27 +103,10 @@ let () = if Debug.Args.option_list () then exit 0
(* exit 1 *)
(* end *)
let
fname
=
match
!
file
with
|
None
->
Arg
.
usage
spec
usage_str
;
exit
1
|
Some
f
->
f
let
config
=
Whyconf
.
read_config
!
opt_config
let
config
=
List
.
fold_left
Whyconf
.
merge_config
config
!
opt_extra
let
loadpath
=
(
Whyconf
.
loadpath
(
Whyconf
.
get_main
config
))
@
List
.
rev
!
includes
let
env
=
Env
.
create_env
loadpath
let
()
=
Whyconf
.
load_plugins
(
Whyconf
.
get_main
config
)
let
()
=
Debug
.
Args
.
set_flags_selected
()
;
if
Debug
.
Args
.
option_list
()
then
exit
0
let
fname
=
match
!
opt_file
with
|
None
->
Arg
.
usage
option_list
usage_msg
;
exit
1
|
Some
f
->
f
let
found_upgraded_prover
=
ref
false
...
...
@@ -490,6 +428,6 @@ let () =
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3replay
er
.byte"
compile-command: "unset LANG; make -C ../.. bin/why3replay.byte"
End:
*)
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment