@@ -9201,50 +9201,51 @@ (define-public numdiff
(define-public why3
(package
(name "why3")
- (version "1.4.1")
- (source (origin
- (method git-fetch)
- (uri (git-reference
- (url "https://gitlab.inria.fr/why3/why3")
- (commit version)))
- (file-name (git-file-name name version))
- (sha256
- (base32
- "1yca6mx8bjm8x0i594ivh31aw45s6fbimmwfj8g2v9zwrgmr1i4s"))))
+ (version "1.6.0")
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://gitlab.inria.fr/why3/why3")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "0k3y98xzhrl44vwzq2m6k4nrllrwp3ll69lc2gfl8d77w0wg7gkp"))))
(build-system ocaml-build-system)
- (native-inputs
- (list autoconf automake coq ocaml which))
- (propagated-inputs
- (list camlzip ocaml-graph ocaml-menhir ocaml-num ocaml-zarith))
- (inputs
- (list coq-flocq emacs-minimal zlib))
+ (native-inputs (list autoconf automake coq ocaml which))
+ (propagated-inputs (list camlzip ocaml-graph ocaml-menhir ocaml-num
+ ocaml-zarith))
+ (inputs (list coq-flocq emacs-minimal zlib))
(arguments
- `(#:phases
- (modify-phases %standard-phases
- (add-before 'configure 'bootstrap
- (lambda _
- (invoke "./autogen.sh")
- (setenv "CONFIG_SHELL" (which "sh"))
- (substitute* "configure"
- (("#! /bin/sh") (string-append "#!" (which "sh")))
- ;; find ocaml-num in the correct directory
- (("\\$DIR/nums.cma") "$DIR/num.cma")
- (("\\$DIR/num.cmi") "$DIR/core/num.cmi"))
- #t))
- (add-after 'configure 'fix-makefile
- (lambda _
- (substitute* "Makefile"
- ;; find ocaml-num in the correct directory
- (("site-lib/num") "site-lib"))
- #t))
- (add-after 'install 'install-lib
- (lambda _
- (invoke "make" "byte")
- (invoke "make" "install-lib")
- #t)))))
+ `(#:phases (modify-phases %standard-phases
+ (add-before 'configure 'bootstrap
+ (lambda _
+ (invoke "./autogen.sh")
+ (setenv "CONFIG_SHELL"
+ (which "sh"))
+ (substitute* "configure"
+ (("#! /bin/sh")
+ (string-append "#!"
+ (which "sh")))
+ ;; find ocaml-num in the correct directory
+ (("\\$DIR/nums.cma")
+ "$DIR/num.cma")
+ (("\\$DIR/num.cmi")
+ "$DIR/core/num.cmi")) #t))
+ (add-after 'configure 'fix-makefile
+ (lambda _
+ (substitute* "Makefile"
+ ;; find ocaml-num in the correct directory
+ (("site-lib/num")
+ "site-lib")) #t))
+ (add-after 'install 'install-lib
+ (lambda _
+ (invoke "make" "byte")
+ (invoke "make" "install-lib") #t)))))
(home-page "https://why3.lri.fr")
(synopsis "Deductive program verification")
- (description "Why3 provides a language for specification and programming,
+ (description
+ "Why3 provides a 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,
From: Arnaud DABY-SEESARAM <ds-ac@nanein.fr> * gnu/packages/maths.scm (why3): Update to 1.6.0. Change-Id: I4d6e0e2224f1ffe85b84493f1834114bc8687d1b --- gnu/packages/maths.scm | 81 +++++++++++++++++++++--------------------- 1 file changed, 41 insertions(+), 40 deletions(-)