Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit bcaf7319 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update opam files

parent 26c5d8a3
* marks an incompatible change * marks an incompatible change
o improved task highlighting for negated premises
(contributed by Mikhail Mandrykin, AstraVer project)
version 0.86, May 11th, 2015 version 0.86, May 11th, 2015
============================ ============================
...@@ -36,7 +39,7 @@ IDE: ...@@ -36,7 +39,7 @@ IDE:
window is exited by hitting the "Save&Close" button window is exited by hitting the "Save&Close" button
o right part of main window organized in tabs. o right part of main window organized in tabs.
o better explanations and task highlighting o better explanations and task highlighting
(contributed by Mikhail Mandrykin) (contributed by Mikhail Mandrykin, AstraVer project)
bug fixes: bug fixes:
o bug in interpreter in presence of nested mutable fields 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" maintainer: "Claude.Marche@inria.fr"
authors: [ authors: [
"François Bobot" "François Bobot"
...@@ -17,29 +17,37 @@ tags: [ ...@@ -17,29 +17,37 @@ tags: [
"automated theorem prover" "automated theorem prover"
"interactive theorem prover" "interactive theorem prover"
] ]
available: [ ocaml-version >= "4.01.0" ]
# Jessie3 (frama-c plugin) is *disabled* because it is not ready
build: [ build: [
["./configure" "--prefix" prefix "--disable-bench"] ["./configure" "--prefix" prefix "--disable-frama-c"
"--disable-ide" { !conf-gtksourceview:installed }
]
[make "opt" "byte"] [make "opt" "byte"]
[make "install" "install-lib"] [make "install" "install-lib"]
] ]
build-doc: [ build-doc: [
[make "doc" "stdlibdoc" "apidoc"] [make "doc" "stdlibdoc" "apidoc"]
[make "DOCDIR=%{doc}%/why3" "install-doc"] [make "DOCDIR=%{doc}%/why3" "install-doc"]
] ]
depends: [ depends: [
"alt-ergo" "ocamlfind"
"lablgtk" {>= "2.14.2"}
"conf-gtksourceview"
"camlzip"
"zarith"
"menhir" "menhir"
] ]
depopts: [ depopts: [
"ocamlgraph" {>= "1.8.2"} "lablgtk"
"coq" {>= "8.4"} "conf-gtksourceview"
"zenon" "zarith"
"camlzip"
"ocamlgraph"
"coq"
] ]
messages: [
"Proving with Coq won't be possible unless you install the coq package" conflicts: [
{! coq:installed} "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 WhyML, and relies on external theorem provers, both automated and
interactive, to discharge verification conditions. Why3 comes with a interactive, to discharge verification conditions. Why3 comes with a
standard library of logical theories (integer and real arithmetic, standard library of logical theories (integer and real arithmetic,
...@@ -17,4 +17,4 @@ architecture for calling external provers, and a well-designed API, ...@@ -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 allowing to use Why3 as a software library. An important emphasis is
put on modularity and genericity, giving the end user a possibility to put on modularity and genericity, giving the end user a possibility to
easily reuse Why3 formalizations or to add support for a new external easily reuse Why3 formalizations or to add support for a new external
prover if wanted. prover if wanted.
\ No newline at end of file
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