...
  View open merge request
Commits (4)
......@@ -38,8 +38,9 @@ why3.conf
/distrib
/why3regtests.err
/why3regtests.out
/.merlin
.merlin
/src/jessie/.merlin
/why3*.install
# /bench/
/bench/programs/good/booleans/
......@@ -346,3 +347,4 @@ pvsbin/
/trash
trywhy3.tar.gz
/_build/
......@@ -152,11 +152,16 @@ endif
# main target
###############
ifeq (@enable_why3_lib@,yes)
all: @OCAMLBEST@
else
all:
endif
.PHONY: dune
all: dune
dune: src/util/config.ml
dune build @install
$(HIDE) mkdir -p bin
clean::
dune clean
plugins: plugins.@OCAMLBEST@
opt: plugins.opt
......@@ -325,10 +330,6 @@ lib/why3/why3.cmx: $(LIBCMX) lib/why3/why3.cmo
# clean and depend
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(LIBDEP)
endif
depend: $(LIBDEP)
CLEANDIRS += src $(addprefix src/, $(LIBDIRS))
......@@ -501,11 +502,6 @@ lib/plugins/microc.cmxs: $(MICROCCMX)
lib/plugins/microc.cmo: $(MICROCCMO)
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(PLUGDEP)
endif
depend: $(PLUGDEP)
CLEANDIRS += plugins $(addprefix plugins/, $(PLUGDIRS)) lib/plugins
......@@ -582,8 +578,9 @@ install-bin::
install_local:: bin/why3 $(addprefix bin/,$(TOOLS_BIN))
bin/%: bin/%.@OCAMLBEST@
ln -sf $(notdir $<) $@
#TODO use dune promote or dune exec
bin/%: dune
$(HIDE) cp _build/install/default/bin/$* $@
install_local:: share/drivers share/stdlib
......@@ -593,10 +590,6 @@ share/drivers:
share/stdlib:
ln -snf ../stdlib share/stdlib
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(TOOLSDEP)
endif
depend: $(TOOLSDEP)
CLEANDIRS += src/tools
......@@ -747,7 +740,7 @@ ifeq (@enable_ide@,yes)
IDEGENERATED = src/ide/gtkcompat.ml
IDE_FILES = gtkcompat gconfig ide_utils why3ide
IDE_FILES = gtkcompat gconfig ide_utils why3_resetgc why3ide
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
......@@ -777,11 +770,6 @@ src/ide/resetgc.o: src/ide/resetgc.c
$(HIDE)$(OCAMLC) -c -ccopt "-Wall -o $@" $<
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(IDEDEP)
endif
depend: $(IDEDEP)
CLEANDIRS += src/ide
......@@ -851,11 +839,6 @@ bin/why3webserver.byte: $(WHY3CMA) $(WEBSERVCMO)
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(WEBSERVDEP)
endif
depend: $(WEBSERVDEP)
CLEANDIRS += src/ide
......@@ -899,10 +882,6 @@ bin/why3session.byte: $(WHY3CMA) $(SESSIONCMO)
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(SESSIONDEP)
endif
depend: $(SESSIONDEP)
CLEANDIRS += src/why3session
......@@ -945,11 +924,6 @@ bin/why3shell.byte: $(WHY3CMA) $(SHELLCMO)
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(SHELLDEP)
endif
depend: $(SHELLDEP)
uninstall-bin::
......@@ -1528,10 +1502,6 @@ bin/why3doc.byte: $(WHY3CMA) $(WHY3DOCCMO)
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(WHY3DOCDEP)
endif
depend: $(WHY3DOCDEP)
CLEANDIRS += src/why3doc
......
......@@ -292,6 +292,12 @@ MENHIRVERSION=`$MENHIR --version | sed -n -e 's,.*version *\(.*\)$,\1,p'`
AX_VERSION_GE([$MENHIRVERSION], 20151112, [],
[AC_MSG_ERROR(You need Menhir 20151112 or higher.)])
AC_CHECK_PROG(DUNE,dune,dune,no)
if test "$DUNE" = no ; then
AC_MSG_ERROR(Cannot find dune.)
fi
## Where are the library we need
# we look for ocamlfind; if not present, we just don't use it to find
# libraries
......
(lang dune 1.6)
(using menhir 2.0)
......@@ -52,8 +52,8 @@ RUN opam repository add coq-released https://coq.inria.fr/opam/released --all-sw
ARG opam_packages
RUN opam install -y depext
RUN opam depext --dry-run menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo
RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo
RUN opam depext --dry-run menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo dune
RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo dune
RUN test -z "$opam_packages" || opam depext --dry-run $opam_packages
RUN test -z "$opam_packages" || opam install -y $opam_packages
(library
(name why3_core)
(public_name why3.core)
(modules
ident ty term pattern decl coercion theory
task pretty dterm env trans printer model_parser
)
(flags -open Why3_util -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util num)
)
(ocamllex driver_lexer parse_smtv2_model_lexer)
(menhir (modules driver_parser parse_smtv2_model_parser))
(library
(name why3_driver)
(public_name why3.driver)
(modules
prove_client call_provers driver_ast driver_parser driver_lexer driver
whyconf autodetection
smt2_model_defs parse_smtv2_model_parser
collect_data_model parse_smtv2_model_lexer parse_smtv2_model
parse_smtv2_model
)
(flags -open Why3_util -open Why3_core -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util why3.core num unix)
)
(library
(public_name why3)
(modules v1 v2)
(libraries why3.util why3.core why3.driver why3.parser why3.transform why3.printer why3.session)
)
(executable
(public_name why3ide)
(modules gtkcompat gconfig ide_utils why3ide)
(libraries why3 why3_resetgc
(select gtkcompat.ml from
(lablgtk3 lablgtk3-sourceview3 -> gtkcompat3.ml )
(lablgtk2 lablgtk2.sourceview2 -> gtkcompat2.ml )
)
)
(flags -open Why3.V1 -linkall)
(package why3-ide)
)
(library
(name why3_resetgc)
(modules why3_resetgc)
(c_names resetgc)
)
(executable
(name why3web)
(public_name why3webserver)
(modules wserver why3web)
(libraries why3)
(flags -open Why3.V1 -linkall)
(package why3)
)
external reset_gc : unit -> unit = "ml_reset_gc"
......@@ -18,8 +18,6 @@ open History
open Itp_communication
open Gtkcompat
external reset_gc : unit -> unit = "ml_reset_gc"
let debug = Debug.lookup_flag "ide_info"
let debug_stack_trace = Debug.lookup_flag "stack_trace"
......@@ -960,7 +958,7 @@ let fan =
let update_monitor =
let c = ref 0 in
fun t s r ->
reset_gc ();
Why3_resetgc.reset_gc ();
incr c;
let f = if r = 0 then " " else fan !c in
let text = Printf.sprintf "%s %d/%d/%d" f t s r in
......
(library
(name why3_mlw)
(public_name why3.mlw)
(modules
ity expr pdecl eval_match typeinv vc pmodule dexpr
pinterp mltree compile mlinterp pdriver cprinter ml_printer
ocaml_printer cakeml_printer
)
(flags -open Why3_util -open Why3_core -open Why3_driver -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util why3.core why3.driver num unix)
)
(ocamllex lexer)
(menhir (modules parser)
(infer false)
)
(library
(name why3_parser)
(public_name why3.parser)
(modules
ptree glob typing parser typing lexer
)
(flags -open Why3_util -open Why3_core -open Why3_mlw -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util why3.core why3.mlw num menhirLib)
)
(library
(name why3_printer)
(public_name why3.printer)
(modules
cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq
pvs isabelle
simplify gappa cvc3 yices mathematica
)
(flags -open Why3_util -open Why3_core -open Why3_transform -open Why3_mlw -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util why3.core why3.transform why3.mlw num)
)
(ocamllex xml strategy_parser)
(library
(name why3_session)
(public_name why3.session)
(modules
compress xml termcode session_itp
strategy strategy_parser controller_itp
server_utils itp_communication
itp_server json_util
)
(libraries why3.util why3.core num why3.transform why3.driver why3.parser
(select compress.ml from
(zip -> compress_z.ml)
( -> compress_none.ml))
)
(flags -open Why3_util -open Why3_core -open Why3_transform -open Why3_driver -open Why3_parser -w A-4-9-41-44-45-50-52@5@8@48)
)
(include_subdirs no)
(executables
(public_names why3config why3execute why3extract why3prove why3realize why3wc)
(libraries why3)
(modules why3config why3execute why3extract why3prove why3realize why3wc)
(flags -linkall -open Why3.V1)
(package why3)
)
(executable
(name main)
(public_name why3)
(libraries why3)
(modules main)
(flags -linkall -open Why3.V1)
(package why3)
)
(ocamllex why3wc)
(library
(name why3_unix_scheduler)
(modules unix_scheduler)
(libraries why3)
(flags -linkall -open Why3.V1)
)
(executable
(public_name why3replay)
(libraries why3 why3_unix_scheduler)
(modules why3replay)
(flags -linkall -open Why3.V1 -open Why3_unix_scheduler)
(package why3)
)
(executable
(public_name why3shell)
(modules why3shell)
(libraries why3 why3_unix_scheduler)
(flags -linkall -open Why3.V1 -open Why3_unix_scheduler)
(package why3)
)
(library
(name why3_transform)
(public_name why3.transform)
(modules
simplify_formula inlining split_goal
args_wrapper detect_polymorphism reduction_engine compute
eliminate_definition eliminate_algebraic
abstract_quantifiers eliminate_unknown_types
eliminate_unknown_lsymbols eliminate_symbol
eliminate_inductive eliminate_let eliminate_if
libencoding discriminate encoding encoding_select
encoding_guards_full encoding_tags_full
encoding_guards encoding_tags encoding_twin
encoding_sort simplify_array filter_trigger
abstraction close_epsilon lift_epsilon
eliminate_epsilon intro_projections_counterexmp
instantiate_predicate smoke_detector
prop_curry eliminate_literal
generic_arg_trans_utils case apply subst
introduction ind_itp destruct cut congruence
intro_vc_vars_counterexmp prepare_for_counterexmp
induction induction_pr matching reflection
)
(flags -open Why3_util -open Why3_core -open Why3_mlw -open Why3_parser -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util why3.core why3.mlw why3.parser num)
)
(ocamllex rc lexlib json_lexer)
(menhir (modules json_parser))
(library
(name why3_util)
(public_name why3.util)
(modules
config bigInt util opt lists strings
pp extmap extset exthtbl weakhtbl
hashcons wstdlib exn_printer
json_base json_parser json_lexer
debug loc lexlib print_tree
cmdline warning sysutil rc plugin bigInt number vector pqueue
)
(flags -w A-4-9-41-44-45-50-52@5@8@48)
(libraries num dynlink str unix)
)
module Why3 = struct
include Why3_util
include Why3_core
include Why3_driver
include Why3_mlw
include Why3_parser
include Why3_transform
include Why3_printer
include Why3_session
end
module Util = Why3_util
module Core = Why3_core
module Driver = Why3_driver
module Mlw = Why3_mlw
module Parser = Why3_parser
module Transform = Why3_transform
module Printer = Why3_printer
module Session = Why3_session
(executable
(public_name why3doc)
(name doc_main)
(modules doc_html doc_def doc_lexer doc_main)
(libraries why3)
(flags -linkall -open Why3.V1)
(package why3)
)
(ocamllex doc_lexer)
(executable
(public_name why3session)
(name why3session_main)
(modules why3session_lib why3session_info
why3session_html why3session_latex why3session_update
why3session_main)
(libraries why3)
(flags -open Why3.V1 -linkall)
(package why3)
)