Commit e8ecc8d2 authored by MARCHE Claude's avatar MARCHE Claude

update opam files

parent 5063cd85
* marks an incompatible change
o improved task highlighting for negated premises
(contributed by Mikhail Mandrykin, AstraVer project)
version 0.86, May 11th, 2015
============================
......@@ -36,7 +39,7 @@ IDE:
window is exited by hitting the "Save&Close" button
o right part of main window organized in tabs.
o better explanations and task highlighting
(contributed by Mikhail Mandrykin)
(contributed by Mikhail Mandrykin, AstraVer project)
bug fixes:
o bug in interpreter in presence of nested mutable fields
......
archive: "https://gforge.inria.fr/frs/download.php/file/<fixme>/why3-<fixme>.tar.gz"
checksum: "<fixme>"
Why3 environment for deductive program verification (base)
This package is for advanced users only, normal users should use the
full why3 package.
opam-version: "1"
opam-version: "1.2"
maintainer: "Claude.Marche@inria.fr"
authors: [
"François Bobot"
......@@ -17,29 +17,37 @@ tags: [
"automated theorem prover"
"interactive theorem prover"
]
available: [ ocaml-version >= "4.01.0" ]
# Jessie3 (frama-c plugin) is *disabled* because it is not ready
build: [
["./configure" "--prefix" prefix "--disable-bench"]
["./configure" "--prefix" prefix "--disable-frama-c"
"--disable-ide" { !conf-gtksourceview:installed }
]
[make "opt" "byte"]
[make "install" "install-lib"]
]
build-doc: [
[make "doc" "stdlibdoc" "apidoc"]
[make "DOCDIR=%{doc}%/why3" "install-doc"]
]
depends: [
"alt-ergo"
"lablgtk" {>= "2.14.2"}
"conf-gtksourceview"
"camlzip"
"zarith"
"ocamlfind"
"menhir"
]
depopts: [
"ocamlgraph" {>= "1.8.2"}
"coq" {>= "8.4"}
"zenon"
"lablgtk"
"conf-gtksourceview"
"zarith"
"camlzip"
"ocamlgraph"
"coq"
]
messages: [
"Proving with Coq won't be possible unless you install the coq package"
{! coq:installed}
conflicts: [
"lablgtk" {< "2.14.2"}
"ocamlgraph" {< "1.8.2"}
"coq" {< "8.4"}
]
archive: "https://gforge.inria.fr/frs/download.php/file/34775/why3-0.86.tar.gz"
checksum: "4521da929108a7329d3945a7cc5bca92"
Why3 is a platform for deductive program verification.
Why3 environment for deductive program verification.
It provides a rich language for specification and programming, called
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,
......@@ -17,4 +17,4 @@ 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.
\ No newline at end of file
prover if wanted.
opam-version: "1.2"
maintainer: "Claude.Marche@inria.fr"
authors: [
"François Bobot"
"Jean-Christophe Filliâtre"
"Claude Marché"
"Guillaume Melquiond"
"Andrei Paskevich"
]
homepage: "http://why3.lri.fr/"
license: "GNU Lesser General Public License version 2.1"
doc: ["http://why3.lri.fr/#documentation"]
tags: [
"deductive"
"program verification"
"formal specification"
"automated theorem prover"
"interactive theorem prover"
]
available: [ ocaml-version >= "4.01.0" ]
depends: [
"why3-base" { = "0.86" }
"lablgtk"
"conf-gtksourceview"
"zarith"
"camlzip"
"ocamlgraph"
]
messages:[
"Coq realizations of Why3 theories are only available if Coq is installed" { !coq:installed }
]
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