aboutsummaryrefslogtreecommitdiff
path: root/gnu/packages/maths.scm
diff options
context:
space:
mode:
authorJean-Pierre De Jesus DIAZ <jean@foundation.xyz>2024-05-15 17:01:34 +0200
committerAndreas Enge <andreas@enge.fr>2024-05-15 17:21:14 +0200
commite6413c6f517f450c9c4cdfb4362b0c7ca75323db (patch)
tree482c054d3b6160433843f068995a39f469d9dbcb /gnu/packages/maths.scm
parent05d4190587bd5111da18eb3b157bd7776a37bc30 (diff)
downloadguix-e6413c6f517f450c9c4cdfb4362b0c7ca75323db.tar.gz
guix-e6413c6f517f450c9c4cdfb4362b0c7ca75323db.zip
gnu: why3: Use new style.
* gnu/packages/maths.scm (why3): Use new style and move arguments above input fields. Change-Id: Ia9cb04cafe426d7f20c5efb10ca540572dbd3be9 Signed-off-by: Andreas Enge <andreas@enge.fr>
Diffstat (limited to 'gnu/packages/maths.scm')
-rw-r--r--gnu/packages/maths.scm63
1 files changed, 34 insertions, 29 deletions
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index cbde85751c..1e10d4caa8 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9497,36 +9497,41 @@ numeric differences and differences in numeric formats.")
(base32
"0fq8wg8ji2v2ssz1d681glmk8glps1irnmdlhqfklaggx01hlf4p"))))
(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))
(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)))))
+ (list #: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"))))
+ (add-after 'configure 'fix-makefile
+ (lambda _
+ (substitute* "Makefile"
+ ;; find ocaml-num in the correct directory
+ (("site-lib/num") "site-lib"))))
+ (add-after 'install 'install-lib
+ (lambda _
+ (invoke "make" "byte")
+ (invoke "make" "install-lib"))))))
+ (native-inputs (list autoconf
+ automake
+ coq
+ ocaml
+ ocaml-findlib
+ which))
+ (propagated-inputs (list camlzip
+ ocaml-graph
+ ocaml-menhir
+ ocaml-num
+ ocaml-zarith))
+ (inputs (list coq-flocq
+ emacs-minimal
+ zlib))
(home-page "https://why3.lri.fr")
(synopsis "Deductive program verification")
(description "Why3 provides a language for specification and programming,