Commit da6022c4 authored by MARCHE Claude's avatar MARCHE Claude

adding support for compressed files. Needs splitting the library into

two parts: why3 and why3session.

(The Coq tactic does not include why3session)
parent 957b8118
......@@ -179,6 +179,7 @@ pvsbin/
# /src/session
/src/session/xml.ml
/src/session/compress.ml
# /src/tools
/src/tools/why3wc.ml
......
......@@ -63,7 +63,7 @@ EMACS = @EMACS@
#PSVIEWER = @PSVIEWER@
#PDFVIEWER = @PDFVIEWER@
INCLUDES =
INCLUDES = @ZIPINCLUDE@
OFLAGS = -w Aer-41-44-45 -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w Aer-41-44-45 -dtypes -g -I lib/why3 $(INCLUDES)
......@@ -77,7 +77,7 @@ endif
# external libraries common to all binaries
EXTOBJS =
EXTLIBS = str unix nums dynlink
EXTLIBS = str unix nums dynlink @ZIPLIB@
EXTCMA = $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
......@@ -108,10 +108,12 @@ LIBGENERATED = src/util/config.ml \
src/util/rc.ml src/parser/lexer.ml \
src/parser/parser.mli src/parser/parser.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml \
src/driver/driver_lexer.ml src/session/xml.ml \
lib/ocaml/why3__BigInt_compat.ml
src/driver/driver_lexer.ml \
src/session/compress.ml src/session/xml.ml \
lib/ocaml/why3__BigInt_compat.ml
LIB_UTIL = config bigInt util opt lists strings extmap extset exthtbl weakhtbl \
LIB_UTIL = config bigInt util opt lists strings \
extmap extset exthtbl weakhtbl \
hashcons stdlib exn_printer pp debug loc print_tree \
cmdline warning sysutil rc plugin bigInt number pqueue
......@@ -137,8 +139,6 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
simplify gappa cvc3 yices mathematica
LIB_SESSION = xml termcode session session_tools session_scheduler
LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
mlw_dexpr mlw_typing mlw_driver mlw_ocaml \
mlw_main mlw_interp
......@@ -149,21 +149,36 @@ LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \
$(addprefix src/driver/, $(LIB_DRIVER)) \
$(addprefix src/transform/, $(LIB_TRANSFORM)) \
$(addprefix src/printer/, $(LIB_PRINTER)) \
$(addprefix src/session/, $(LIB_SESSION)) \
$(addprefix src/whyml/, $(LIB_WHYML))
LIBDIRS = util core parser driver transform printer session whyml
LIB_SESSION = compress xml termcode session session_tools session_scheduler
LIBSESSIONMODULES = $(addprefix src/session/, $(LIB_SESSION))
LIBDIRS = util core parser driver transform printer whyml
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
LIBSESSIONDIRS = session
LIBSESSIONINCLUDES = $(addprefix -I src/, $(LIBSESSIONDIRS))
LIBDEP = $(addsuffix .dep, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
LIBSESSIONDEP = $(addsuffix .dep, $(LIBSESSIONMODULES))
LIBSESSIONCMO = $(addsuffix .cmo, $(LIBSESSIONMODULES))
LIBSESSIONCMX = $(addsuffix .cmx, $(LIBSESSIONMODULES))
$(LIBDEP): DEPFLAGS += $(LIBINCLUDES)
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
$(LIBCMX): OFLAGS += -for-pack Why3
$(LIBSESSIONDEP): DEPFLAGS += $(LIBSESSIONINCLUDES)
$(LIBSESSIONCMO) $(LIBSESSIONCMX): INCLUDES += $(LIBSESSIONINCLUDES)
$(LIBSESSIONCMX): OFLAGS += -for-pack Why3session
$(LIBDEP): $(LIBGENERATED)
$(LIBSESSIONDEP): $(LIBGENERATED)
# Zarith
......@@ -182,6 +197,23 @@ endif
clean::
rm -f lib/ocaml/why3__BigInt_compat.ml
# Ocamlzip
ifeq (@enable_zip@,yes)
src/session/compress.ml: config.status src/session/compress_z.ml
cp src/session/compress_z.ml $@
else
src/session/compress.ml: config.status src/session/compress_none.ml
cp src/session/compress_none.ml $@
endif
clean::
rm -f src/session/compress.ml
# build targets
byte: lib/why3/why3.cma
......@@ -203,13 +235,32 @@ lib/why3/why3.cmx: $(LIBCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
byte: lib/why3/why3session.cma
opt: lib/why3/why3session.cmxa
lib/why3/why3session.cma: lib/why3/why3session.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) -a $(BFLAGS) -o $@ $^
lib/why3/why3session.cmxa: lib/why3/why3session.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) -a $(OFLAGS) -o $@ $^
lib/why3/why3session.cmo: $(LIBSESSIONCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -pack -o $@ $^
lib/why3/why3session.cmx: $(LIBSESSIONCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
# clean and depend
ifneq "$(MAKECMDGOALS)" "clean"
include $(LIBDEP)
include $(LIBDEP) $(LIBSESSIONDEP)
endif
depend: $(LIBDEP)
depend: $(LIBDEP) $(LIBSESSIONDEP)
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
......@@ -734,11 +785,11 @@ opt: bin/why3ide.opt
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
bin/why3ide.opt: lib/why3/why3.cmxa src/ide/resetgc.o $(IDECMX)
bin/why3ide.opt: lib/why3/why3.cmxa lib/why3/why3session.cmxa src/ide/resetgc.o $(IDECMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3ide.byte: lib/why3/why3.cma src/ide/resetgc.o $(IDECMO)
bin/why3ide.byte: lib/why3/why3.cma lib/why3/why3session.cma src/ide/resetgc.o $(IDECMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^
......@@ -772,6 +823,63 @@ install_local:: bin/why3ide
endif
# <<<<<<< HEAD
# =======
# ###############
# # 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 lib/why3/why3session.cmxa $(REPLAYERCMX)
# $(if $(QUIET),@echo 'Linking $@' &&) \
# $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
# bin/why3replayer.byte: lib/why3/why3.cma lib/why3/why3session.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@ $(BINDIR)/why3replayer$(EXE)
# install_local:: bin/why3replayer
# >>>>>>> adding support for compressed files. Needs splitting the library into
###############
# Session
###############
......@@ -779,7 +887,7 @@ endif
SESSION_FILES = why3session_lib why3session_copy why3session_info \
why3session_latex why3session_html why3session_rm \
why3session_output why3session_run why3session_csv \
why3session
why3session_main
SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
......@@ -795,11 +903,11 @@ $(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session
byte: bin/why3session.byte
opt: bin/why3session.opt
bin/why3session.opt: lib/why3/why3.cmxa $(SESSIONCMX)
bin/why3session.opt: lib/why3/why3.cmxa lib/why3/why3session.cmxa $(SESSIONCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO)
bin/why3session.byte: lib/why3/why3.cma lib/why3/why3session.cma $(SESSIONCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
......@@ -904,7 +1012,7 @@ COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
COQPTREES = kernel lib interp parsing proofs pretyping tactics library toplevel
COQPINCLUDES = -I src/coq-tactic -I +camlp5 $(addprefix -I @COQLIB@/, $(COQPTREES))
COQPINCLUDES = -I src/coq-tactic -I +camlp5 $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@
$(COQPDEP): DEPFLAGS += -I src/coq-tactic
$(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
......@@ -1345,7 +1453,7 @@ OCAMLLIBS_CMO = $(addsuffix .cmo, $(OCAMLLIBS_MODULES))
OCAMLLIBS_CMX = $(addsuffix .cmx, $(OCAMLLIBS_MODULES))
$(OCAMLLIBS_DEP): DEPFLAGS += -I src/util -I lib/ocaml @BIGINTINCLUDE@
$(OCAMLLIBS_CMO) $(OCAMLLIBS_CMX): INCLUDES += -I src/util -I lib/ocaml @BIGINTINCLUDE@
$(OCAMLLIBS_CMO) $(OCAMLLIBS_CMX): INCLUDES += -I src/util -I lib/ocaml @BIGINTINCLUDE@
$(OCAMLLIBS_CMX): OFLAGS += -for-pack Why3extract
ifneq "$(MAKECMDGOALS)" "clean"
......@@ -1646,16 +1754,16 @@ test-api-mlw.opt: examples/use_api/mlw.ml lib/why3/why3.cmxa
#test-shape: lib/why3/why3.cma
# ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) $? examples/test_shape.ml
test-session.byte: examples/use_api/create_session.ml lib/why3/why3.cma
test-session.byte: examples/use_api/create_session.ml lib/why3/why3.cma lib/why3/why3session.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null\
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma lib/why3/why3session.cma $< > /dev/null\
|| (rm -f why3session.xml; \
printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
@rm -f why3session.xml
test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa lib/why3/why3session.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa lib/why3/why3session.cmxa $< \
&& ./test-session.opt > /dev/null) \
|| (rm -f test-session.opt why3session.xml; \
printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
......
......@@ -72,6 +72,13 @@ AC_ARG_ENABLE(zarith,
enable_zarith=yes)
# Ocamlzip
AC_ARG_ENABLE(zip,
AS_HELP_STRING([--enable-zip], [use LZ compression to store session files]),,
enable_zip=yes)
# IDE
AC_ARG_ENABLE(ide,
......@@ -365,6 +372,33 @@ else
fi
# checking for Ocamlzip
if test "$enable_zip" = yes; then
if test "$USEOCAMLFIND" = yes; then
ZIPINCLUDE=$(ocamlfind query zip)
fi
if test -n "$ZIPINCLUDE"; then
echo "ocamlfind found ocamlzip in $ZIPINCLUDE"
ZIPINCLUDE="-I $ZIPINCLUDE"
else
AC_CHECK_FILE($OCAMLLIB/zip/zip.cma,,enable_zip=no)
if test "$enable_zip" = no; then
AC_MSG_WARN([Lib Ocamlzip not found, sessions files will not be compressed.])
reason_zip=" (ocamlzip not found)"
else
ZIPINCLUDE="-I +zip"
fi
fi
fi
if test "$enable_zip" = yes; then
ZIPLIB=zip
else
ZIPLIB=
fi
# checking for lablgtk2
if test "$enable_ide" = yes ; then
if test "$USEOCAMLFIND" = yes; then
......@@ -710,6 +744,10 @@ AC_SUBST(enable_zarith)
AC_SUBST(BIGINTINCLUDE)
AC_SUBST(BIGINTLIB)
AC_SUBST(enable_zip)
AC_SUBST(ZIPINCLUDE)
AC_SUBST(ZIPLIB)
AC_SUBST(enable_coq_tactic)
AC_SUBST(enable_coq_libs)
AC_SUBST(enable_coq_fp_libs)
......@@ -781,6 +819,7 @@ echo " Library path : $OCAMLLIB"
echo " Native compilation : $enable_native_code"
echo " Profiling : $enable_profiling"
echo "Zarith : $enable_zarith$reason_zarith"
echo "Ocamlzip : $enable_zip$reason_zip"
echo "IDE : $enable_ide$reason_ide"
echo "Bench tool : $enable_bench$reason_bench"
echo "Documentation : $enable_doc$reason_doc"
......
......@@ -483,8 +483,9 @@ One can run provers on those tasks exactly as we did above.
\section{Proof Sessions}
See the example \verb|examples/use_api/create_session.ml| of the distribution for
an illustration on how to manipulate proof sessions from an OCaml program.
See the example \verb|examples/use_api/create_session.ml| of the
distribution for an illustration on how to manipulate proof sessions
from an OCaml program.
\section{ML Programs}
......
......@@ -23,6 +23,8 @@ open Format
(* opening the Why3 library *)
open Why3
(* opening the Why3 session library *)
open Why3session
(* access to the Why configuration *)
......
......@@ -3,3 +3,9 @@ version = "@VERSION@"
archive(byte) = "why3.cma"
archive(native) = "why3.cmxa"
requires = "str unix num dynlink"
description = "Why3 session library"
version = "@VERSION@"
archive(byte) = "why3session.cma"
archive(native) = "why3session.cmxa"
requires = "str unix num dynlink @ZIPLIB@ why3"
(* This file is a stub for ocamldep. Do not delete it. *)
......@@ -10,9 +10,11 @@
(********************************************************************)
open Format
open Why3
open Rc
open Whyconf
open Why3session
let debug = Debug.register_info_flag "ide_info"
~desc:"Print@ why3ide@ debugging@ messages."
......
......@@ -10,6 +10,7 @@
(********************************************************************)
open Why3
open Why3session
type t =
{ mutable window_width : int;
......
......@@ -17,6 +17,9 @@ open Whyconf
open Gconfig
open Stdlib
open Debug
open Why3session
module C = Whyconf
external reset_gc : unit -> unit = "ml_reset_gc"
......
val compression_supported : bool
module type S = sig
type out_channel
val open_out: string -> out_channel
val output_char: out_channel -> char -> unit
val output: out_channel -> string -> int -> int -> unit
val output_string: out_channel -> string -> unit
val close_out: out_channel -> unit
type in_channel
val open_in: string -> in_channel
val input: in_channel -> string -> int -> int -> int
val really_input: in_channel -> string -> int -> int -> unit
val input_char: in_channel -> char
val close_in: in_channel -> unit
end
module Compress_z : S
module Compress_none : S
let compression_supported = false
module type S = sig
type out_channel
val open_out: string -> out_channel
val output_char: out_channel -> char -> unit
val output: out_channel -> string -> int -> int -> unit
val output_string: out_channel -> string -> unit
val close_out: out_channel -> unit
type in_channel
val open_in: string -> in_channel
val input: in_channel -> string -> int -> int -> int
val really_input: in_channel -> string -> int -> int -> unit
val input_char: in_channel -> char
val close_in: in_channel -> unit
end
module Compress_none = Pervasives
module Compress_z = Pervasives
let compression_supported = true
module type S = sig
type out_channel
val open_out: string -> out_channel
val output_char: out_channel -> char -> unit
val output: out_channel -> string -> int -> int -> unit
val output_string: out_channel -> string -> unit
val close_out: out_channel -> unit
type in_channel
val open_in: string -> in_channel
val input: in_channel -> string -> int -> int -> int
val really_input: in_channel -> string -> int -> int -> unit
val input_char: in_channel -> char
val close_in: in_channel -> unit
end
module Compress_none = Pervasives
module Compress_z = struct
type out_channel = Gzip.out_channel
let open_out fn = Gzip.open_out ~level:6 fn
let output_char = Gzip.output_char
let output = Gzip.output
let output_string ch s = output ch s 0 (String.length s)
let close_out = Gzip.close_out
type in_channel = Gzip.in_channel
let open_in = Gzip.open_in
let input = Gzip.input
let really_input = Gzip.really_input
let input_char = Gzip.input_char
let close_in = Gzip.close_in
end
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Debug
open Why3
open Stdlib
open Ty
open Ident
......@@ -404,7 +404,7 @@ let empty_session ?shape_version dir =
let create_session ?shape_version project_dir =
if not (Sys.file_exists project_dir) then
begin
dprintf debug
Debug.dprintf debug
"[Info] '%s' does not exists. Creating directory of that name \
for the project@." project_dir;
Unix.mkdir project_dir 0o777
......@@ -494,6 +494,7 @@ open Format
let db_filename = "why3session.xml"
let shape_filename = "why3shapes.dat"
let compressed_shape_filename = "why3shapes.gz"
let session_dir_for_save = ref "."
let save_string fmt s =
......@@ -574,8 +575,11 @@ let save_label fmt s =
fprintf fmt "@\n@[<hov 1><label@ name=\"%a\"/>@]" save_string s.Ident.lab_string
*)
module Compr = Compress.Compress_z
type save_ctxt = {
provers : (int * int * int) Mprover.t; ch_shapes : out_channel
provers : (int * int * int) Mprover.t;
ch_shapes : Compr.out_channel;
}
let rec save_goal ctxt fmt g =
......@@ -588,10 +592,10 @@ let rec save_goal ctxt fmt g =
(opt "expl") g.goal_expl
save_string checksum
(save_bool_def "expanded" false) g.goal_expanded;
output_string ctxt.ch_shapes checksum;
output_char ctxt.ch_shapes ' ';
output_string ctxt.ch_shapes shape;
output_char ctxt.ch_shapes '\n';
Compr.output_string ctxt.ch_shapes checksum ;
Compr.output_char ctxt.ch_shapes ' ';
Compr.output_string ctxt.ch_shapes shape;
Compr.output_char ctxt.ch_shapes '\n';
(*
Ident.Slab.iter (save_label fmt) g.goal_name.Ident.id_label;
*)
......@@ -719,7 +723,7 @@ let save_prover fmt p (timelimits,memlimits) (provers,id) =
let save fname shfname _config session =
let ch = open_out fname in
let chsh = open_out shfname in
let chsh = Compr.open_out shfname in
let fmt = formatter_of_out_channel ch in
fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
fprintf fmt "<!DOCTYPE why3session PUBLIC \"-//Why3//proof session v5//EN\"@ \"http://why3.lri.fr/why3session.dtd\">@\n";
......@@ -739,14 +743,17 @@ let save fname shfname _config session =
fprintf fmt "@]@\n</why3session>";
fprintf fmt "@.";
close_out ch;
close_out chsh
Compr.close_out chsh
let save_session config session =
let f = Filename.concat session.session_dir db_filename in
Sysutil.backup_file f;
let fs = Filename.concat session.session_dir shape_filename in
Sysutil.backup_file fs;
let fz = Filename.concat session.session_dir compressed_shape_filename in
Sysutil.backup_file fz;
session_dir_for_save := session.session_dir;
let fs = if Compress.compression_supported then fz else fs in
save f fs config session
(*****************************)
......@@ -1114,7 +1121,7 @@ let load_ident elt =
type load_ctxt = {
old_provers : (Whyconf.prover * int * int) Mstr.t ;
shapes : (string, Tc.shape) Hashtbl.t