Skip to content

GitLab

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

rename the shared library pack to Why3

parent 1f3e60bb
Hide whitespace changes
Inline Side-by-side
Showing with 93 additions and 93 deletions
Makefile.in
View file @ cff6a051
......@@ -159,23 +159,23 @@ LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
$(LIBCMX): OFLAGS += -for-pack Why
$(LIBCMX): OFLAGS += -for-pack Why3
# build targets
byte: src/why.cma
opt: src/why.cmxa
byte: src/why3.cma
opt: src/why3.cmxa
src/why.cma: src/why.cmo
src/why3.cma: src/why3.cmo
$(OCAMLC) -a $(BFLAGS) -o $@ $^
src/why.cmxa: src/why.cmx
src/why3.cmxa: src/why3.cmx
$(OCAMLOPT) -a $(OFLAGS) -o $@ $^
src/why.cmo: $(LIBCMO)
src/why3.cmo: $(LIBCMO)
$(OCAMLC) $(BFLAGS) -pack -o $@ $^
src/why.cmx: $(LIBCMX)
src/why3.cmx: $(LIBCMX)
$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
# depend target
......@@ -199,7 +199,7 @@ LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
clean::
rm -f $(LIBCLEAN) $(LIBGENERATED)
rm -f src/why.cm[iox] src/why.[ao] src/why.cma src/why.cmxa
rm -f src/why3.cm[aiox] src/why3.[ao] src/why3.cmxa
rm -f .depend.lib
###############
......@@ -227,9 +227,9 @@ install_no_local::
install_no_local_lib::
mkdir -p $(OCAMLLIB)/why3
cp -f src/why.cm* $(OCAMLLIB)/why3
cp -f src/why3.cm* $(OCAMLLIB)/why3
cp -f META $(OCAMLLIB)/why3
if test -f src/why.a; then cp -f src/why.a $(OCAMLLIB)/why3; fi
if test -f src/why3.a; then cp -f src/why3.a $(OCAMLLIB)/why3; fi
ifeq (@enable_local@,yes)
install install-lib:
......@@ -250,20 +250,20 @@ install-all: install install-lib
byte: bin/why3.byte
opt: bin/why3.opt
bin/why3.opt: src/why.cmxa src/main.cmx
bin/why3.opt: src/why3.cmxa src/main.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
bin/why3.byte: src/why.cma src/main.cmo
bin/why3.byte: src/why3.cma src/main.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
bin/why3: bin/why3.@OCAMLBEST@
ln -sf why3.@OCAMLBEST@ $@
src/main.cmo: src/why.cma
src/main.cmx: src/why.cmxa
src/main.cmo: src/why3.cma
src/main.cmx: src/why3.cmxa
clean::
rm -f src/main.cm[iox] src/main.annot src/main.o
......@@ -295,12 +295,12 @@ $(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
byte: bin/why3ml.byte
opt: bin/why3ml.opt
bin/why3ml.opt: src/why.cmxa $(PGMCMX) src/main.cmx
bin/why3ml.opt: src/why3.cmxa $(PGMCMX) src/main.cmx
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
bin/why3ml.byte: src/why.cma $(PGMCMO) src/main.cmo
bin/why3ml.byte: src/why3.cma $(PGMCMO) src/main.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
......@@ -385,12 +385,12 @@ $(CONFIGCMO) $(CONFIGCMX): INCLUDES += -I src/programs
byte: bin/why3config.byte
opt: bin/why3config.opt
bin/why3config.opt: src/why.cmxa $(CONFIGCMX)
bin/why3config.opt: src/why3.cmxa $(CONFIGCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
bin/why3config.byte: src/why.cma $(CONFIGCMO)
bin/why3config.byte: src/why3.cma $(CONFIGCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
......@@ -449,12 +449,12 @@ bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
bin/why3ide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(IDECMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
bin/why3ide.byte: src/why.cma $(PGMCMO) $(IDECMO)
bin/why3ide.byte: src/why3.cma $(PGMCMO) $(IDECMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
......@@ -505,12 +505,12 @@ $(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
byte: bin/why3replayer.byte
opt: bin/why3replayer.opt
bin/why3replayer.opt: src/why.cmxa $(PGMCMX) $(REPLAYERCMX)
bin/why3replayer.opt: src/why3.cmxa $(PGMCMX) $(REPLAYERCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
bin/why3replayer.byte: src/why.cma $(PGMCMO) $(REPLAYERCMO)
bin/why3replayer.byte: src/why3.cma $(PGMCMO) $(REPLAYERCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
......@@ -566,12 +566,12 @@ opt: bin/why3bench.opt
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I @SQLITE3LIB@
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3
bin/why3bench.opt: src/why.cmxa $(PGMCMX) $(BENCHCMX)
bin/why3bench.opt: src/why3.cmxa $(PGMCMX) $(BENCHCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
bin/why3bench.byte: src/why.cma $(PGMCMO) $(BENCHCMO)
bin/why3bench.byte: src/why3.cma $(PGMCMO) $(BENCHCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
......@@ -627,10 +627,10 @@ opt: src/coq-plugin/whytac.cmxs
src/coq-plugin/whytac.cma: BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
src/coq-plugin/whytac.cmxs: src/why3.cmxa $(COQCMX)
$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
src/coq-plugin/whytac.cma: src/why3.cma $(COQCMO)
$(OCAMLC) -a $(BFLAGS) -o $@ $^
src/coq-plugin/g_whytac.ml: src/coq-plugin/g_whytac.ml4
......@@ -751,12 +751,12 @@ $(WHY3DOCCMO) $(WHY3DOCCMX): INCLUDES += -I src/why3doc
byte: bin/why3doc.byte
opt: bin/why3doc.opt
bin/why3doc.opt: src/why.cmxa $(WHY3DOCCMX)
bin/why3doc.opt: src/why3.cmxa $(WHY3DOCCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
bin/why3doc.byte: src/why.cma $(WHY3DOCCMO)
bin/why3doc.byte: src/why3.cma $(WHY3DOCCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
......@@ -807,7 +807,7 @@ comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)
# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
# bin/why3.byte -D bench/plugins/helloworld.drv \
# tests/test-jcf.why -T Test -G G
# bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv \
# bin/why3.$(OCAMLBEST) -D bench/plugins/helloworld.drv \
# tests/test-jcf.why -T Test -G G
###############
......@@ -849,12 +849,12 @@ testl-ide: bin/why3ide.opt
testl-type: bin/why3ml.byte
ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
test-api: src/why.cma
ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why.cma examples/use_api.ml \
test-api: src/why3.cma
ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma examples/use_api.ml \
|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
bts12244: src/why.cma
ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why.cma examples/bts12244.ml
bts12244: src/why3.cma
ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma examples/bts12244.ml
## Examples : Plugins ##
......@@ -876,8 +876,8 @@ PLUGCMXS = $(addsuffix .cmxs, $(PLUGMODULES))
# opt: src/plug-plugin/whytac.cmxs
# endif
# $(PLUGCMO): src/why.cma
# $(PLUGCMXS): src/why.cmxa
# $(PLUGCMO): src/why3.cma
# $(PLUGCMXS): src/why3.cmxa
.PHONY: examples_plugins.byte examples_plugins.opt
......
examples/plugins/genequlin.ml
View file @ cff6a051
......@@ -21,7 +21,7 @@
*)
open Why
open Why3
open Format
(***************
......
examples/use_api.ml
View file @ cff6a051
......@@ -25,7 +25,7 @@ the alt-ergo prover to check them
******************)
(* opening the Why3 library *)
open Why
open Why3
(* a ground propositional goal: true or false *)
let fmla_true : Term.term = Term.t_true
......
src/bench/bench.ml
View file @ cff6a051
......@@ -18,7 +18,7 @@
(**************************************************************************)
open Thread
open Why
open Why3
open Util
open Env
open Theory
......
src/bench/bench.mli
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
open Env
open Theory
open Task
......
src/bench/benchdb.ml
View file @ cff6a051
......@@ -20,7 +20,7 @@
(** run benchs from the database *)
open Format
open Why
open Why3
open Util
module BenchUtil = Bench.BenchUtil
......
src/bench/benchdb.mli
View file @ cff6a051
......@@ -19,6 +19,6 @@
(** run benchs from the database *)
open Why
open Why3
val db : Whyconf.config -> Env.env -> unit
src/bench/benchrc.ml
View file @ cff6a051
......@@ -19,7 +19,7 @@
open Format
open Bench
open Why
open Why3
open Util
open Theory
......
src/bench/benchrc.mli
View file @ cff6a051
......@@ -58,7 +58,7 @@ csv = "prgbench.csv"
*)
open Bench
open Why
open Why3
open Util
......
src/bench/whybench.ml
View file @ cff6a051
......@@ -18,7 +18,7 @@
(**************************************************************************)
open Format
open Why
open Why3
open Util
open Whyconf
open Theory
......
src/config/whyconfig.ml
View file @ cff6a051
......@@ -18,7 +18,7 @@
(**************************************************************************)
open Format
open Why
open Why3
open Util
open Whyconf
......
src/coq-plugin/whytac.ml
View file @ cff6a051
......@@ -30,7 +30,7 @@ open Libnames
open Declarations
open Pp
open Why
open Why3
open Call_provers
open Whyconf
open Ty
......@@ -62,10 +62,10 @@ let get_prover s =
let print_constr fmt c = pp_with fmt (Termops.print_constr c)
let print_tvm fmt m =
Idmap.iter (fun id tv -> Format.fprintf fmt "%s->%a@ "
(string_of_id id) Why.Pretty.print_tv tv) m
(string_of_id id) Why3.Pretty.print_tv tv) m
let print_bv fmt m =
Idmap.iter (fun id vs -> Format.fprintf fmt "%s->%a@ "
(string_of_id id) Why.Pretty.print_vsty vs) m
(string_of_id id) Why3.Pretty.print_vsty vs) m
(* Coq constants *)
let logic_dir = ["Coq";"Logic";"Decidable"]
......
src/driver/driver.ml
View file @ cff6a051
......@@ -305,7 +305,7 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
| NoPrinter -> Format.fprintf fmt
"No printer specified in the driver file"
| NoPlugins -> Format.fprintf fmt
"Plugins are not supported, recomplie Why"
"Plugins are not supported, recomplie Why3"
| Duplicate s -> Format.fprintf fmt
"Duplicate %s specification" s
| UnknownType (thl,idl) -> Format.fprintf fmt
......
src/driver/whyconf.mli
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
(** Managing the configuration of Why *)
(** Managing the configuration of Why3 *)
open Util
......
src/ide/db.ml
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
open Sqlite3
......
src/ide/db.mli
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
(** Proof database *)
......
src/ide/gconfig.ml
View file @ cff6a051
......@@ -18,7 +18,7 @@
(**************************************************************************)
open Format
open Why
open Why3
open Util
open Rc
open Whyconf
......@@ -272,7 +272,7 @@ let () =
eprintf " done.@."
let show_legend_window () =
let dialog = GWindow.dialog ~title:"Why: legend of icons" () in
let dialog = GWindow.dialog ~title:"Why3: legend of icons" () in
let vbox = dialog#vbox in
let text = GText.view ~packing:vbox#add
~editable:false ~cursor_visible:false () in
......@@ -340,7 +340,7 @@ let set_labels_flag =
(if b then Debug.set_flag else Debug.unset_flag) fl
let preferences c =
let dialog = GWindow.dialog ~title:"Why: preferences" () in
let dialog = GWindow.dialog ~title:"Why3: preferences" () in
let vbox = dialog#vbox in
let notebook = GPack.notebook ~packing:vbox#add () in
(** page 1 **)
......
src/ide/gconfig.mli
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
(*
type prover_data = Session.prover_data
......@@ -38,14 +38,14 @@ type t =
mutable default_editor : string;
mutable show_labels : bool;
mutable saving_policy : int;
mutable env : Why.Env.env;
mutable env : Why3.Env.env;
mutable config : Whyconf.config;
}
(*
val get_prover_data : Why.Env.env -> string ->
Why.Whyconf.config_prover ->
prover_data Why.Util.Mstr.t -> prover_data Why.Util.Mstr.t
val get_prover_data : Why3.Env.env -> string ->
Why3.Whyconf.config_prover ->
prover_data Why3.Util.Mstr.t -> prover_data Why3.Util.Mstr.t
*)
val save_config : unit -> unit
......
src/ide/newmain.ml
View file @ cff6a051
......@@ -26,7 +26,7 @@ let () =
eprintf " done.@."
open Why
open Why3
open Whyconf
open Gconfig
......
src/ide/replay.ml
View file @ cff6a051
......@@ -18,7 +18,7 @@
(**************************************************************************)
open Why
open Why3
let includes = ref []
......
src/ide/session.ml
View file @ cff6a051
......@@ -18,7 +18,7 @@
(**************************************************************************)
open Why
open Why3
open Format
(***************************)
......
src/ide/session.mli
View file @ cff6a051
......@@ -19,7 +19,7 @@
(** Proof sessions *)
open Why
open Why3
(** {2 Prover's data} *)
......
src/main.ml
View file @ cff6a051
......@@ -18,7 +18,7 @@
(**************************************************************************)
open Format
open Why
open Why3
open Util
open Whyconf
open Theory
......@@ -406,7 +406,7 @@ let output_task_prepared drv fname _tname th task dir =
close_out cout
let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
match !opt_output, !opt_command with
| Some dir, Some command when !opt_bisect ->
let test task =
......
src/programs/pgm_effect.ml
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
open Util
open Ident
open Term
......
src/programs/pgm_effect.mli
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
open Term
type reference =
......
src/programs/pgm_env.ml
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
open Util
open Theory
open Pgm_module
......
src/programs/pgm_env.mli
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
open Theory
open Pgm_module
......
src/programs/pgm_fastwp.ml
View file @ cff6a051
......@@ -20,7 +20,7 @@
(* CURRENTLY DEAD CODE; FOR LATER USE... *)
open Format
open Why
open Why3
open Ident
open Ty
open Term
......
src/programs/pgm_main.ml
View file @ cff6a051
......@@ -20,7 +20,7 @@
(* main module for whyl *)
open Format
open Why
open Why3
open Util
open Ident
open Theory
......
src/programs/pgm_module.ml
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
open Util
open Ident
open Ty
......
src/programs/pgm_module.mli
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
open Ident
open Ty
open Term
......
src/programs/pgm_pretty.ml
View file @ cff6a051
......@@ -18,7 +18,7 @@
(**************************************************************************)
open Format
open Why
open Why3
open Pp
open Ident
open Term
......
src/programs/pgm_ttree.ml
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
open Denv
open Ty
open Pgm_types
......
src/programs/pgm_types.ml
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
open Util
open Ident
open Ty
......@@ -260,7 +260,7 @@ module rec T : sig
val occur_type_v : R.t -> type_v -> bool
val v_result : ty -> vsymbol
val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
val exn_v_result : Why3.Term.lsymbol -> Why3.Term.vsymbol option
val post_map : (term -> term) -> post -> post
......
src/programs/pgm_types.mli
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
open Util
open Ident
open Ty
......@@ -161,7 +161,7 @@ module rec T : sig
val occur_type_v : R.t -> type_v -> bool
val v_result : ty -> vsymbol
val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
val exn_v_result : Why3.Term.lsymbol -> Why3.Term.vsymbol option
val post_map : (term -> term) -> post -> post
......
src/programs/pgm_typing.ml
View file @ cff6a051
......@@ -18,7 +18,7 @@
(**************************************************************************)
open Format
open Why
open Why3
open Pp
open Util
open Ident
......
src/programs/pgm_typing.mli
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
val debug : Debug.flag
......
src/programs/pgm_wp.ml
View file @ cff6a051
......@@ -18,7 +18,7 @@
(**************************************************************************)
open Format
open Why
open Why3
open Util
open Ident
open Ty
......
src/programs/pgm_wp.mli
View file @ cff6a051
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Why3
open Term
val debug : Debug.flag
......
src/tptp2why/tptp2whymain.ml
View file @ cff6a051
......@@ -22,7 +22,7 @@
open TptpTree
open Why
open Why3
open Lexing
......