Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
75 lines (71 sloc) 1.6 KB
opam-version: "2.0"
maintainer: "guillaume.melquiond@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/doc/"
bug-reports: "https://gitlab.inria.fr/why3/why3/issues"
dev-repo: "git+https://gitlab.inria.fr/why3/why3.git"
tags: [
"deductive"
"program verification"
"formal specification"
"automated theorem prover"
"interactive theorem prover"
]
build: [
[
"./configure"
"--prefix"
prefix
"--disable-frama-c"
"--disable-ide" {!conf-gtksourceview:installed}
]
[make "-j%{jobs}%" "all" "opt" "byte"]
[make "doc" "stdlibdoc" "apidoc"] {with-doc}
]
install: [
[make "install_no_local" "install_no_local_lib"]
[make "DOCDIR=%{doc}%/why3" "install-doc"] {with-doc}
]
remove: [
["rm" "%{bin}%/why3"]
["rm" "-r" "%{lib}%/why3"]
["rm" "-r" "%{share}%/why3"]
]
depends: [
"ocaml" {>= "4.02.3" & < "4.07.0"}
"ocamlfind" {build}
"menhir"
"num"
]
depopts: [
"lablgtk"
"conf-gtksourceview"
"zarith"
"camlzip"
"ocamlgraph"
"coq"
]
conflicts: [
"lablgtk" {< "2.14.2"}
"ocamlgraph" {< "1.8.2"}
"coq" {< "8.4"}
"coq" {>= "8.8"}
]
synopsis: "Why3 environment for deductive program verification (base)"
description: """
This package is for advanced users only, normal users should use the
full why3 package."""
flags: light-uninstall
url {
src:
"https://gforge.inria.fr/frs/download.php/file/37313/why3-0.88.3.tar.gz"
checksum: "md5=1ee0fd41075ba5e77a4b94ad0cc2dd43"
}