Skip to content

why3
why3
Commit 28c8b0ff authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

bring camlzip into coq-tactic 

and merge the why3 and why3session libraries back into one.
parent 89556a91
Hide whitespace changes
Inline Side-by-side
Showing with 38 additions and 114 deletions
Makefile.in
View file @ 28c8b0ff
......@@ -109,7 +109,7 @@ LIBGENERATED = src/util/config.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/compress.ml src/session/xml.ml \
src/session/compress.ml src/session/xml.ml \
src/session/strategy_parser.ml \
lib/ocaml/why3__BigInt_compat.ml
......@@ -124,7 +124,7 @@ LIB_CORE = ident ty term pattern decl theory \
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
whyconf autodetection
LIB_MLW = ity
LIB_MLW = ity
LIB_PARSER = ptree glob parser typing lexer
......@@ -147,6 +147,9 @@ 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
LIB_SESSION = compress xml termcode session session_tools strategy \
strategy_parser session_scheduler
LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \
$(addprefix src/core/, $(LIB_CORE)) \
$(addprefix src/driver/, $(LIB_DRIVER)) \
......@@ -154,50 +157,30 @@ LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \
$(addprefix src/parser/, $(LIB_PARSER)) \
$(addprefix src/transform/, $(LIB_TRANSFORM)) \
$(addprefix src/printer/, $(LIB_PRINTER)) \
$(addprefix src/whyml/, $(LIB_WHYML))
$(addprefix src/whyml/, $(LIB_WHYML)) \
$(addprefix src/session/, $(LIB_SESSION))
LIB_SESSION = compress xml termcode session session_tools strategy \
strategy_parser session_scheduler
LIBSESSIONMODULES = $(addprefix src/session/, $(LIB_SESSION))
LIBDIRS = util core driver mlw parser transform printer whyml
LIBDIRS = util core driver mlw parser transform printer whyml session
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
ifeq (@enable_zarith@,yes)
lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_zarith.ml
cp lib/ocaml/why3__BigInt_zarith.ml $@
else
lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_num.ml
cp lib/ocaml/why3__BigInt_num.ml $@
endif
clean::
......@@ -206,15 +189,11 @@ clean::
# 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::
......@@ -241,32 +220,13 @@ 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) $(LIBSESSIONDEP)
include $(LIBDEP)
endif
depend: $(LIBDEP) $(LIBSESSIONDEP)
depend: $(LIBDEP)
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
......@@ -279,7 +239,7 @@ LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
clean::
rm -f $(LIBCLEAN) $(LIBGENERATED)
rm -f lib/why3/why3.cm* lib/why3/why3.[ao]
rm -f lib/why3/why3session.* lib/why3/why3.cm* lib/why3/why3.[ao]
###############
# installation
......@@ -326,7 +286,6 @@ endif
install_no_local_lib::
mkdir -p $(OCAMLINSTALLLIB)/why3
cp -f lib/why3/why3.cm* lib/why3/why3.[ao] \
lib/why3/why3session.cm* lib/why3/why3session.[ao] \
lib/why3/META $(OCAMLINSTALLLIB)/why3
ifeq (@enable_local@,yes)
......@@ -579,17 +538,17 @@ bin/why3realize.byte: lib/why3/why3.cma src/tools/why3realize.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3replay.opt: lib/why3/why3.cmxa lib/why3/why3session.cmxa src/tools/why3replay.cmx
bin/why3replay.opt: lib/why3/why3.cmxa src/tools/why3replay.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3replay.byte: lib/why3/why3.cma lib/why3/why3session.cma src/tools/why3replay.cmo
bin/why3replay.byte: lib/why3/why3.cma src/tools/why3replay.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
clean_old_install::
rm -f $(TOOLS_BIN:%=$(TOOLDIR)/%$(EXE)) $(BINDIR)/why3$(EXE)
rm -f $(BINDIR)/why3config$(EXE) $(BINDIR)/why3bench$(EXE) $(BINDIR)/why3replayer$(EXE)
rm -f $(BINDIR)/why3bench$(EXE) $(BINDIR)/why3replayer$(EXE)
install_no_local::
cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
......@@ -721,11 +680,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 lib/why3/why3session.cmxa src/ide/resetgc.o $(IDECMX)
bin/why3ide.opt: lib/why3/why3.cmxa src/ide/resetgc.o $(IDECMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3ide.byte: lib/why3/why3.cma lib/why3/why3session.cma src/ide/resetgc.o $(IDECMO)
bin/why3ide.byte: lib/why3/why3.cma src/ide/resetgc.o $(IDECMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^
......@@ -780,11 +739,11 @@ $(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session
byte: bin/why3session.byte
opt: bin/why3session.opt
bin/why3session.opt: lib/why3/why3.cmxa lib/why3/why3session.cmxa $(SESSIONCMX)
bin/why3session.opt: lib/why3/why3.cmxa $(SESSIONCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3session.byte: lib/why3/why3.cma lib/why3/why3session.cma $(SESSIONCMO)
bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
......@@ -844,11 +803,11 @@ src/coq-tactic/coqCompat.ml: src/coq-tactic/coqCompat@coq_compat_version@.ml
lib/coq-tactic/why3tac.cmxs: lib/why3/why3.cmxa $(COQPCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
$(OCAMLOPT) $(OFLAGS) -o $@ -shared $(addsuffix .cmxa, @ZIPLIB@) $^
lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) -a $(BFLAGS) -o $@ $^
$(OCAMLC) -a $(BFLAGS) -o $@ $(addsuffix .cma, @ZIPLIB@) $^
src/coq-tactic/g_why3tac.ml: src/coq-tactic/g_why3tac.ml4
$(if $(QUIET),@echo 'Camlp5 $<' &&) \
......@@ -1559,16 +1518,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 lib/why3/why3session.cma
test-session.byte: examples/use_api/create_session.ml lib/why3/why3.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma lib/why3/why3session.cma $< > /dev/null\
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null\
|| (rm -f why3session.xml why3shapes why3shapes.gz; \
printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
@rm -f why3session.xml why3shapes why3shapes.gz
test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa lib/why3/why3session.cmxa
test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa lib/why3/why3session.cmxa $< \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
&& ./test-session.opt > /dev/null) \
|| (rm -f test-session.opt why3session.xml why3shapes why3shapes.gz; \
printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
......@@ -1692,8 +1651,7 @@ doc/apidoc:
apidoc: doc/apidoc $(FILESTODOC)
$(OCAMLDOC) -d doc/apidoc -html -t "Why3 API documentation" \
-keep-code $(INCLUDES) \
$(LIBINCLUDES) $(LIBSESSIONINCLUDES) -I lib/why3 $(FILESTODOC)
-keep-code $(INCLUDES) $(LIBINCLUDES) -I lib/why3 $(FILESTODOC)
# could we include also the dependency graph ? -- someone
# At least we can give a way to create it -- francois
......
examples/use_api/create_session.ml
View file @ 28c8b0ff
......@@ -13,7 +13,7 @@
This file builds a new session from a given file.
To each goal is added as many proof attempts as provers
To each goal is added as many proof attempts as provers
found in the configuration.
......@@ -23,9 +23,6 @@ open Format
(* opening the Why3 library *)
open Why3
(* opening the Why3 session library *)
open Why3session
(* access to the Why configuration *)
......@@ -63,11 +60,11 @@ let keygen ?parent () = ()
(* create an empty session in the current directory *)
let env_session,_,_ =
let dummy_session : unit Session.session = Session.create_session "." in
Session.update_session ~use_shapes:false ~keygen ~allow_obsolete:true
Session.update_session ~use_shapes:false ~keygen ~allow_obsolete:true
dummy_session env config
(* adds a file in the new session *)
let file : unit Session.file =
let file : unit Session.file =
let file_name = "examples/logic/hello_proof.why" in
try
Session.add_file keygen env_session file_name
......@@ -77,7 +74,7 @@ let file : unit Session.file =
exit 1
(* explore the theories in that file *)
let theories = file.Session.file_theories
let theories = file.Session.file_theories
let () = eprintf "%d theories found@." (List.length theories)
(* add proof attempts for each goals in the theories *)
......@@ -94,7 +91,7 @@ let add_proofs_attempts g =
~memlimit:1000
~edit:None
g p.Whyconf.prover Session.Scheduled
in ())
in ())
provers
let () =
......
lib/why3/META.in
View file @ 28c8b0ff
......@@ -2,10 +2,4 @@ description = "Why3 library"
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"
requires = "str unix num dynlink @ZIPLIB@"
lib/why3/why3session.ml deleted 100644 → 0
View file @ 89556a91
(* This file is a stub for ocamldep. Do not delete it. *)
src/ide/gconfig.ml
View file @ 28c8b0ff
......@@ -12,7 +12,6 @@
open Why3
open Rc
open Whyconf
open Why3session
let debug = Debug.register_info_flag "ide_info"
~desc:"Print@ why3ide@ debugging@ messages."
......
src/ide/gconfig.mli
View file @ 28c8b0ff
......@@ -10,7 +10,6 @@
(********************************************************************)
open Why3
open Why3session
type t =
{ mutable window_width : int;
......
src/ide/gmain.ml
View file @ 28c8b0ff
......@@ -18,8 +18,6 @@ open Gconfig
open Stdlib
open Debug
open Why3session
module C = Whyconf
external reset_gc : unit -> unit = "ml_reset_gc"
......
src/session/session.ml
View file @ 28c8b0ff
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Why3
open Stdlib
open Ty
open Ident
......
src/session/session.mli
View file @ 28c8b0ff
......@@ -9,8 +9,6 @@
(* *)
(********************************************************************)
open Why3
(** Proof sessions
Define all the functions needed for managing a session:
......
src/session/session_scheduler.ml
View file @ 28c8b0ff
......@@ -10,7 +10,6 @@
(********************************************************************)
open Format
open Why3
open Session
let debug = Debug.register_info_flag "scheduler"
......
src/session/session_scheduler.mli
View file @ 28c8b0ff
......@@ -30,7 +30,6 @@ module Todo : sig
end
open Why3
open Session
(** {2 Observers signature} *)
......
src/session/session_tools.ml
View file @ 28c8b0ff
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Why3
open Whyconf
open Session
......
src/session/session_tools.mli
View file @ 28c8b0ff
......@@ -11,7 +11,6 @@
(** Generic tools that can be applied on sessions *)
open Why3
open Session
val unknown_to_known_provers :
......
src/session/termcode.ml
View file @ 28c8b0ff
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Why3
open Term
(*******************************)
......
src/session/termcode.mli
View file @ 28c8b0ff
......@@ -9,8 +9,6 @@
(* *)
(********************************************************************)
open Why3
(** Explanations *)
val goal_expl_task:
......
src/session/xml.mll
View file @ 28c8b0ff
......@@ -46,7 +46,7 @@
let parse_error s = raise (Parse_error s)
let debug = Why3.Debug.register_info_flag "xml"
let debug = Debug.register_info_flag "xml"
~desc:"Print@ the@ XML@ parser@ debugging@ messages."
}
......@@ -68,7 +68,7 @@ rule xml_prolog fixattrs = parse
| "<?xml" space+ "version=\"1.0\"" space+ "encoding=\"UTF-8\"" space+ "?>"
{ xml_doctype fixattrs "1.0" "" lexbuf }
| "<?xml" ([^'?']|'?'[^'>'])* "?>"
{ Why3.Debug.dprintf debug "[Xml warning] prolog ignored@.";
{ Debug.dprintf debug "[Xml warning] prolog ignored@.";
xml_doctype fixattrs "1.0" "" lexbuf }
| _
{ parse_error "wrong prolog" }
......@@ -98,26 +98,26 @@ and elements fixattrs group_stack element_stack = parse
| "</" (ident as celem) space* '>'
{ match group_stack with
| [] ->
Why3.Debug.dprintf debug
Debug.dprintf debug
"[Xml warning] unexpected closing Xml element `%s'@."
celem;
elements fixattrs group_stack element_stack lexbuf
| (elem,att,stack)::g ->
if celem <> elem then
Why3.Debug.dprintf debug
Debug.dprintf debug
"[Xml warning] Xml element `%s' closed by `%s'@."
elem celem;
let e = mk_element elem att element_stack in
elements fixattrs g (e::stack) lexbuf
}
| '<'
{ Why3.Debug.dprintf debug "[Xml warning] unexpected '<'@.";
{ Debug.dprintf debug "[Xml warning] unexpected '<'@.";
elements fixattrs group_stack element_stack lexbuf }
| eof
{ match group_stack with
| [] -> element_stack
| (elem,_,_)::_ ->
Why3.Debug.dprintf debug "[Xml warning] unclosed Xml element `%s'@." elem;
Debug.dprintf debug "[Xml warning] unclosed Xml element `%s'@." elem;
pop_all group_stack element_stack
}
| _ as c
......
src/tools/why3replay.ml
View file @ 28c8b0ff
......@@ -11,7 +11,6 @@
open Format
open Why3
open Why3session
(** {2 Warnings} *)
......
src/why3session/why3session_copy.ml
View file @ 28c8b0ff
......@@ -10,7 +10,6 @@
(********************************************************************)
open Why3
open Why3session
open Why3session_lib
open Whyconf
open Session
......
src/why3session/why3session_csv.ml
View file @ 28c8b0ff
......@@ -10,7 +10,6 @@
(********************************************************************)
open Why3
open Why3session
open Why3session_lib
open Format
......
src/why3session/why3session_html.ml
View file @ 28c8b0ff
......@@ -11,7 +11,6 @@
open Format
open Why3
open Why3session
open Why3session_lib
module Hprover = Whyconf.Hprover
......
src/why3session/why3session_info.ml
View file @ 28c8b0ff
......@@ -15,7 +15,6 @@
(**************************************************************************)
open Why3
open Why3session
open Why3session_lib
open Whyconf
open Format
......
src/why3session/why3session_latex.ml
View file @ 28c8b0ff
......@@ -10,7 +10,6 @@
(********************************************************************)
open Why3
open Why3session
open Why3session_lib
open Format
......
src/why3session/why3session_lib.ml
View file @ 28c8b0ff
......@@ -10,7 +10,7 @@
(********************************************************************)
open Why3
open Why3session
module S = Session
module C = Whyconf
......
src/why3session/why3session_lib.mli
View file @ 28c8b0ff
......@@ -11,7 +11,6 @@
open Why3
open Whyconf
open Why3session
val verbose: Debug.flag
......
src/why3session/why3session_output.ml
View file @ 28c8b0ff
......@@ -10,7 +10,6 @@
(********************************************************************)
open Why3
open Why3session
open Why3session_lib
open Session
open Format
......
src/why3session/why3session_rm.ml
View file @ 28c8b0ff
......@@ -10,7 +10,6 @@
(********************************************************************)
open Why3
open Why3session
open Why3session_lib
open Session
open Format
......
src/why3session/why3session_run.ml
View file @ 28c8b0ff
......@@ -10,7 +10,6 @@
(********************************************************************)
open Why3
open Why3session
open Why3session_lib
open Whyconf
open Session
......
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