Commit 1b4bd864 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Split the opam packages into why3 and why3-ide.

For the sake of opam pinning, the opam directories have been moved to the
root directory. They can be moved back into opam/ once opam 2.0 has been
released.
parent bc868f5e
Why3 environment for deductive program verification (base)
This package is for advanced users only, normal users should use the
full why3 package.
Why3 environment for deductive program verification.
Why3 provides a rich language for specification and programming, called
WhyML, and relies on external theorem provers, both automated and
interactive, to discharge verification conditions. Why3 comes with a
standard library of logical theories (integer and real arithmetic,
Boolean operations, sets and maps, etc.) and basic programming data
structures (arrays, queues, hash tables, etc.). A user can write WhyML
programs directly and get correct-by-construction OCaml programs
through an automated extraction mechanism. WhyML is also used as an
intermediate language for the verification of C, Java, or Ada
programs.
Why3 is a complete reimplementation of the former Why platform. Among
the new features are: numerous extensions to the input language, a new
architecture for calling external provers, and a well-designed API,
allowing to use Why3 as a software library. An important emphasis is
put on modularity and genericity, giving the end user a possibility to
easily reuse Why3 formalizations or to add support for a new external
prover if wanted.
This package provides an IDE for Why3.
......@@ -22,17 +22,34 @@ tags: [
"interactive theorem prover"
]
available: [ ocaml-version >= "4.02.3" ]
build: [
["./configure"
"--prefix" prefix
"--disable-why3-lib"
"--disable-frama-c"
"--disable-coq-tactic"
"--disable-coq-libs"
"--disable-js-of-ocaml"]
[make "-j%{jobs}%" "ide"]
]
install: [make "install-ide"]
remove: [
["rm" "-f" "%{lib}%/why3/commands/why3ide"]
["rm" "-rf" "%{share}%/why3/images"]
]
flags: [ light-uninstall ]
depends: [
"why3-base" { = "0.88.3" }
"ocamlfind" {build}
"why3"
"lablgtk"
"conf-gtksourceview"
"zarith"
"camlzip"
"ocamlgraph"
]
depopts: [
"coq"
]
messages: [
"Coq realizations of Why3 theories are only available if Coq is installed" { !coq:installed }
conflicts: [
"lablgtk" {< "2.14.2"}
]
......@@ -23,14 +23,18 @@ tags: [
]
available: [ ocaml-version >= "4.02.3" ]
# Jessie3 (frama-c plugin) is *disabled* because it is not ready
build: [
["./configure" "--prefix" prefix "--disable-frama-c"
"--disable-ide" { !conf-gtksourceview:installed }]
["./configure"
"--prefix" prefix
"--disable-frama-c"
"--disable-coq-tactic"
"--disable-coq-libs"
"--disable-js-of-ocaml"
"--disable-ide"]
[make "-j%{jobs}%" "all" "opt" "byte"]
]
install: [make "install_no_local" "install_no_local_lib"]
install: [make "install" "install-lib"]
remove: [
["rm" "%{bin}%/why3"]
......@@ -38,6 +42,8 @@ remove: [
["rm" "-r" "%{share}%/why3"]
]
flags: [ light-uninstall ]
build-doc: [
[make "doc" "stdlibdoc" "apidoc"]
[make "DOCDIR=%{doc}%/why3" "install-doc"]
......@@ -50,17 +56,11 @@ depends: [
]
depopts: [
"lablgtk"
"conf-gtksourceview"
"zarith"
"camlzip"
"ocamlgraph"
"coq"
]
conflicts: [
"lablgtk" {< "2.14.2"}
"ocamlgraph" {< "1.8.2"}
"coq" {< "8.4"}
"coq" {>= "8.8"}
]
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