Commit eedc2f21 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Give a git-like invocation to why3 tools.

parent 87268cab
...@@ -51,6 +51,9 @@ why3.conf ...@@ -51,6 +51,9 @@ why3.conf
/bin/why3.byte /bin/why3.byte
/bin/why3.opt /bin/why3.opt
/bin/why3 /bin/why3
/bin/why3contraption.byte
/bin/why3contraption.opt
/bin/why3contraption
/bin/why3ide.byte /bin/why3ide.byte
/bin/why3ide.opt /bin/why3ide.opt
/bin/why3ide /bin/why3ide
...@@ -66,12 +69,6 @@ why3.conf ...@@ -66,12 +69,6 @@ why3.conf
/bin/why3replayer.byte /bin/why3replayer.byte
/bin/why3replayer.opt /bin/why3replayer.opt
/bin/why3replayer /bin/why3replayer
/bin/why3html.byte
/bin/why3html.opt
/bin/why3html
/bin/why3stats.byte
/bin/why3stats.opt
/bin/why3stats
/bin/why3session.opt /bin/why3session.opt
/bin/why3session.byte /bin/why3session.byte
/bin/why3session /bin/why3session
......
...@@ -28,6 +28,7 @@ BINDIR = $(DESTDIR)@bindir@ ...@@ -28,6 +28,7 @@ BINDIR = $(DESTDIR)@bindir@
LIBDIR = $(DESTDIR)@libdir@ LIBDIR = $(DESTDIR)@libdir@
DATADIR = $(DESTDIR)@datarootdir@ DATADIR = $(DESTDIR)@datarootdir@
MANDIR = $(DESTDIR)@mandir@ MANDIR = $(DESTDIR)@mandir@
TOOLDIR = $(LIBDIR)/why3/commands
# OS specific stuff # OS specific stuff
EXE = @EXE@ EXE = @EXE@
...@@ -240,6 +241,7 @@ install_no_local:: clean_old_install $(TARGET_EMACS) ...@@ -240,6 +241,7 @@ install_no_local:: clean_old_install $(TARGET_EMACS)
endif endif
mkdir -p $(BINDIR) mkdir -p $(BINDIR)
mkdir -p $(LIBDIR)/why3 mkdir -p $(LIBDIR)/why3
mkdir -p $(TOOLDIR)
mkdir -p $(DATADIR)/why3 mkdir -p $(DATADIR)/why3
mkdir -p $(DATADIR)/why3/images mkdir -p $(DATADIR)/why3/images
mkdir -p $(DATADIR)/why3/images/boomy mkdir -p $(DATADIR)/why3/images/boomy
...@@ -421,41 +423,58 @@ install_no_local:: ...@@ -421,41 +423,58 @@ install_no_local::
# Why3 # Why3
###### ######
src/main.cmo: lib/why3/why3.cma src/tools/main.cmo: lib/why3/why3.cma
src/main.cmx: lib/why3/why3.cmxa src/tools/main.cmx: lib/why3/why3.cmxa
byte: bin/why3.byte src/tools/why3contraption.cmo: lib/why3/why3.cma
opt: bin/why3.opt src/tools/why3contraption.cmx: lib/why3/why3.cmxa
bin/why3.opt: lib/why3/why3.cmxa src/main.cmx byte: bin/why3.byte bin/why3contraption.byte
opt: bin/why3.opt bin/why3contraption.opt
bin/why3.opt: lib/why3/why3.cmxa src/tools/main.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^ $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3.byte: lib/why3/why3.cma src/main.cmo bin/why3.byte: lib/why3/why3.cma src/tools/main.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^ $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3: bin/why3.@OCAMLBEST@ bin/why3: bin/why3.@OCAMLBEST@
ln -sf why3.@OCAMLBEST@ $@ ln -sf why3.@OCAMLBEST@ $@
bin/why3contraption.opt: lib/why3/why3.cmxa src/tools/why3contraption.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3contraption.byte: lib/why3/why3.cma src/tools/why3contraption.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3contraption: bin/why3contraption.@OCAMLBEST@
ln -sf why3contraption.@OCAMLBEST@ $@
clean_old_install:: clean_old_install::
rm -f $(BINDIR)/why3$(EXE) rm -f $(BINDIR)/why3$(EXE) $(BINDIR)/why3contraption$(EXE)
install_no_local:: install_no_local::
cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE) cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
cp -f bin/why3contraption.@OCAMLBEST@ $(BINDIR)/why3contraption$(EXE)
install_local: bin/why3 install_local: bin/why3 bin/why3contraption
ifneq "$(MAKECMDGOALS)" "clean" ifneq "$(MAKECMDGOALS)" "clean"
include src/main.dep include src/tools/main.dep
include src/tools/why3contraption.dep
endif endif
depend: src/main.dep depend: src/tools/main.dep src/tools/why3contraption.dep
clean:: clean::
rm -f src/main.cm[iox] src/main.annot src/main.o src/main.dep rm -f src/tools/main.cm[iox] src/tools/main.annot src/tools/main.o src/tools/main.dep
rm -f src/tools/why3contraption.cm[iox] src/tools/why3contraption.annot src/tools/why3contraption.o src/tools/why3contraption.dep
rm -f bin/why3.byte bin/why3.opt bin/why3 rm -f bin/why3.byte bin/why3.opt bin/why3
rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml rm -f bin/why3contraption.byte bin/why3contraption.opt bin/why3contraption
############## ##############
# test targets # test targets
...@@ -580,7 +599,7 @@ clean_old_install:: ...@@ -580,7 +599,7 @@ clean_old_install::
rm -f $(BINDIR)/why3config$(EXE) rm -f $(BINDIR)/why3config$(EXE)
install_no_local:: install_no_local::
cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config$(EXE) cp -f bin/why3config.@OCAMLBEST@ $(TOOLDIR)/why3config$(EXE)
install_local: bin/why3config install_local: bin/why3config
...@@ -641,7 +660,7 @@ clean_old_install:: ...@@ -641,7 +660,7 @@ clean_old_install::
rm -f $(BINDIR)/why3ide$(EXE) rm -f $(BINDIR)/why3ide$(EXE)
install_no_local:: install_no_local::
cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide$(EXE) cp -f bin/why3ide.@OCAMLBEST@ $(TOOLDIR)/why3ide$(EXE)
install_local: bin/why3ide install_local: bin/why3ide
...@@ -696,7 +715,7 @@ clean_old_install:: ...@@ -696,7 +715,7 @@ clean_old_install::
rm -f $(BINDIR)/why3replayer$(EXE) rm -f $(BINDIR)/why3replayer$(EXE)
install_no_local:: install_no_local::
cp -f bin/why3replayer.@OCAMLBEST@ $(BINDIR)/why3replayer$(EXE) cp -f bin/why3replayer.@OCAMLBEST@ $(TOOLDIR)/why3replayer$(EXE)
install_local: bin/why3replayer install_local: bin/why3replayer
...@@ -752,7 +771,7 @@ clean_old_install:: ...@@ -752,7 +771,7 @@ clean_old_install::
rm -f $(BINDIR)/why3session$(EXE) rm -f $(BINDIR)/why3session$(EXE)
install_no_local:: install_no_local::
cp -f bin/why3session.@OCAMLBEST@ $(BINDIR)/why3session$(EXE) cp -f bin/why3session.@OCAMLBEST@ $(TOOLDIR)/why3session$(EXE)
install_local: bin/why3session install_local: bin/why3session
...@@ -810,7 +829,7 @@ clean_old_install:: ...@@ -810,7 +829,7 @@ clean_old_install::
rm -f $(BINDIR)/why3bench$(EXE) rm -f $(BINDIR)/why3bench$(EXE)
install_no_local:: install_no_local::
cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench$(EXE) cp -f bin/why3bench.@OCAMLBEST@ $(TOOLDIR)/why3bench$(EXE)
install_local: bin/why3bench install_local: bin/why3bench
...@@ -1395,7 +1414,7 @@ clean_old_install:: ...@@ -1395,7 +1414,7 @@ clean_old_install::
rm -f $(BINDIR)/why3wc$(EXE) rm -f $(BINDIR)/why3wc$(EXE)
install_no_local:: install_no_local::
cp -f bin/why3wc.@OCAMLBEST@ $(BINDIR)/why3wc$(EXE) cp -f bin/why3wc.@OCAMLBEST@ $(TOOLDIR)/why3wc$(EXE)
install_local: bin/why3wc install_local: bin/why3wc
...@@ -1452,7 +1471,7 @@ clean_old_install:: ...@@ -1452,7 +1471,7 @@ clean_old_install::
rm -f $(BINDIR)/why3doc$(EXE) rm -f $(BINDIR)/why3doc$(EXE)
install_no_local:: install_no_local::
cp -f bin/why3doc.@OCAMLBEST@ $(BINDIR)/why3doc$(EXE) cp -f bin/why3doc.@OCAMLBEST@ $(TOOLDIR)/why3doc$(EXE)
install_local: bin/why3doc install_local: bin/why3doc
......
...@@ -9,8 +9,6 @@ datadir="\"$DATADIR/why3\"" ...@@ -9,8 +9,6 @@ datadir="\"$DATADIR/why3\""
localdir="None" localdir="None"
if [ "@enable_relocation@" = "yes" ]; then if [ "@enable_relocation@" = "yes" ]; then
bindir='Filename.concat (Filename.dirname
(Filename.dirname Sys.executable_name)) "bin"'
libdir='Filename.concat (Filename.concat (Filename.dirname libdir='Filename.concat (Filename.concat (Filename.dirname
(Filename.dirname Sys.executable_name)) "lib") "why3"' (Filename.dirname Sys.executable_name)) "lib") "why3"'
datadir='Filename.concat (Filename.concat (Filename.dirname datadir='Filename.concat (Filename.concat (Filename.dirname
...@@ -34,6 +32,8 @@ let localdir = $localdir ...@@ -34,6 +32,8 @@ let localdir = $localdir
let compile_time_support = [ @COMPILETIMECOQ@ @COMPILETIMEPVS@ ] let compile_time_support = [ @COMPILETIMECOQ@ @COMPILETIMEPVS@ ]
" > $config " > $config
if [ "@enable_relocation@" = "no" ]; then
echo " echo "
BINDIR = $bindir BINDIR = $bindir
LIBDIR = $libdir LIBDIR = $libdir
...@@ -43,3 +43,4 @@ BIGINTLIB = @BIGINTLIB@ ...@@ -43,3 +43,4 @@ BIGINTLIB = @BIGINTLIB@
INCLUDE = @BIGINTINCLUDE@ -I $libdir/why3 INCLUDE = @BIGINTINCLUDE@ -I $libdir/why3
" > $makefileconfig " > $makefileconfig
fi
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2014 -- INRIA - CNRS - Paris-Sud 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. *)
(* *)
(********************************************************************)
open Format
open Why3
open Whyconf
open Theory
let usage_msg = sprintf
"Usage: %s [options] [[file|-] [-T <theory> [-G <goal>]...]...]..."
(Filename.basename Sys.argv.(0))
let version_msg = sprintf "Why3 platform, version %s (build date: %s)"
Config.version Config.builddate
let opt_config = ref None
let opt_extra = ref []
let opt_loadpath = ref []
let opt_print_libdir = ref false
let opt_print_datadir = ref false
let opt_list_transforms = ref false
let opt_list_printers = ref false
let opt_list_provers = ref false
let opt_list_formats = ref false
let opt_list_metas = ref false
let opt_version = ref false
let option_list = Arg.align [
"-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>";
"-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
"<dir> Add <dir> to the library search path";
"--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
" same as -L";
"--list-transforms", Arg.Set opt_list_transforms,
" List known transformations";
"--list-printers", Arg.Set opt_list_printers,
" List known printers";
"--list-provers", Arg.Set opt_list_provers,
" List known provers";
"--list-formats", Arg.Set opt_list_formats,
" List known input formats";
"--list-metas", Arg.Set opt_list_metas,
" List known metas";
Debug.Args.desc_debug_list;
Debug.Args.desc_debug_all;
Debug.Args.desc_debug;
"--print-libdir", Arg.Set opt_print_libdir,
" Print location of binary components (plugins, etc)";
"--print-datadir", Arg.Set opt_print_datadir,
" Print location of non-binary data (theories, modules, etc)";
"--version", Arg.Set opt_version,
" Print version information" ]
let command_path =
match Config.localdir with
| Some p -> Filename.concat p "bin"
| None -> Filename.concat Config.libdir "commands"
let command cmd =
let cmd = Filename.concat command_path ("why3" ^ cmd) in
if not (Sys.file_exists cmd) then begin
printf "'%s' is not a why3 command.@." cmd;
exit 1
end;
let args = ref [] in
(match !opt_config with Some v -> args := v :: "-C" :: !args | None -> ());
List.iter (fun v -> args := v :: "-L" :: !args) (List.rev !opt_loadpath);
for i = !Arg.current + 1 to Array.length Sys.argv - 1 do
args := Sys.argv.(i) :: !args;
done;
Unix.execv cmd (Array.of_list (("why3" ^ cmd) :: List.rev !args))
let () = try
Arg.parse option_list command usage_msg;
if !opt_version then begin
printf "%s@." version_msg;
exit 0
end;
if !opt_print_libdir then begin
printf "%s@." Config.libdir;
exit 0
end;
if !opt_print_datadir then begin
printf "%s@." Config.datadir;
exit 0
end;
(** Configuration *)
let config = read_config !opt_config in
let config = List.fold_left merge_config config !opt_extra in
let main = get_main config in
Whyconf.load_plugins main;
Debug.Args.set_flags_selected ();
(** listings*)
let sort_pair (x,_) (y,_) = String.compare x y in
let opt_list = ref false in
if !opt_list_transforms then begin
opt_list := true;
let print_trans_desc fmt (x,r) =
fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" x Pp.formatted r in
printf "@[<hov 2>Known non-splitting transformations:@\n%a@]@\n@."
(Pp.print_list Pp.newline2 print_trans_desc)
(List.sort sort_pair (Trans.list_transforms ()));
printf "@[<hov 2>Known splitting transformations:@\n%a@]@\n@."
(Pp.print_list Pp.newline2 print_trans_desc)
(List.sort sort_pair (Trans.list_transforms_l ()))
end;
if !opt_list_printers then begin
opt_list := true;
let print_printer_desc fmt (s,f) =
fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" s Pp.formatted f in
printf "@[<hov 2>Known printers:@\n%a@]@\n@."
(Pp.print_list Pp.newline2 print_printer_desc)
(List.sort sort_pair (Printer.list_printers ()))
end;
if !opt_list_formats then begin
opt_list := true;
let print1 fmt s = fprintf fmt "%S" s in
let print fmt (p, l, f) =
fprintf fmt "@[%s [%a]@\n @[%a@]@]"
p (Pp.print_list Pp.comma print1) l
Pp.formatted f
in
printf "@[Known input formats:@\n @[%a@]@]@."
(Pp.print_list Pp.newline2 print)
(List.sort Pervasives.compare (Env.list_formats ()))
end;
if !opt_list_provers then begin
opt_list := true;
let print = Pp.print_iter2 Mprover.iter Pp.newline Pp.nothing
print_prover Pp.nothing in
let provers = get_provers config in
printf "@[<hov 2>Known provers:@\n%a@]@." print provers
end;
if !opt_list_metas then begin
opt_list := true;
let print fmt m = fprintf fmt "@[<h 2>%s %s%a@\n@[<hov>%a@]@]"
(let s = m.meta_name in
if String.contains s ' ' then "\"" ^ s ^ "\"" else s)
(if m.meta_excl then "(flag) " else "")
(Pp.print_list Pp.space Pretty.print_meta_arg_type) m.meta_type
Pp.formatted m.meta_desc
in
let cmp m1 m2 = Pervasives.compare m1.meta_name m2.meta_name in
printf "@[<hov 2>Known metas:@\n%a@]@\n@."
(Pp.print_list Pp.newline2 print) (List.sort cmp (Theory.list_metas ()))
end;
opt_list := Debug.Args.option_list () || !opt_list;
if !opt_list then exit 0;
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. byte"
End:
*)
...@@ -803,6 +803,6 @@ let () = ...@@ -803,6 +803,6 @@ let () =
(* (*
Local Variables: Local Variables:
compile-command: "unset LANG; make -C .. byte" compile-command: "unset LANG; make -C ../.. byte"
End: End:
*) *)
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