aboutsummaryrefslogtreecommitdiff
path: root/gnu
diff options
context:
space:
mode:
authorJulien Lepiller <julien@lepiller.eu>2022-07-02 13:36:08 +0200
committerJulien Lepiller <julien@lepiller.eu>2022-11-03 13:24:42 +0100
commite2802132e36ea8157da1c1c06217e4561b6cd79f (patch)
tree4cf39bf300e70449442f0e956038fcd85171517f /gnu
parent2e67329415fd863996d045b52c13ad96425c8119 (diff)
downloadguix-e2802132e36ea8157da1c1c06217e4561b6cd79f.tar
guix-e2802132e36ea8157da1c1c06217e4561b6cd79f.tar.gz
gnu: dedukti: Update to 2.7.
* gnu/packages/ocaml.scm (dedukti): Update to 2.7.
Diffstat (limited to 'gnu')
-rw-r--r--gnu/packages/ocaml.scm31
1 files changed, 6 insertions, 25 deletions
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 47829473b4..96659632bf 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -4675,7 +4675,7 @@ cross-platform SDL C library.")
(define-public dedukti
(package
(name "dedukti")
- (version "2.6.0")
+ (version "2.7")
(home-page "https://deducteam.github.io/")
(source
(origin
@@ -4686,31 +4686,12 @@ cross-platform SDL C library.")
(file-name (git-file-name name version))
(sha256
(base32
- "0frl3diff033i4fmq304b8wbsdnc9mvlhmwd7a3zd699ng2lzbxb"))))
- (inputs
- `(("menhir" ,ocaml-menhir)))
- (native-inputs
- (list ocamlbuild))
- (build-system ocaml-build-system)
+ "1dsr3s88kgmcg3najhc29cwfvsxa2plvjws1127fz75kmn15np28"))))
+ (build-system dune-build-system)
(arguments
- `(#:phases
- ,#~(modify-phases %standard-phases
- (delete 'configure)
- (replace 'build
- (lambda _
- (invoke "make")))
- (replace 'check
- (lambda _
- (invoke "make" "tests")))
- (add-before 'install 'set-binpath
- ;; Change binary path in the makefile
- (lambda _
- (substitute* "GNUmakefile"
- (("BINDIR = (.*)$")
- (string-append "BINDIR = " #$output "/bin")))))
- (replace 'install
- (lambda _
- (invoke "make" "install"))))))
+ `(#:test-target "tests"))
+ (inputs (list gmp ocaml-cmdliner ocaml-z3 z3))
+ (native-inputs (list ocaml-menhir))
(synopsis "Proof-checker for the λΠ-calculus modulo theory, an extension of
the λ-calculus")
(description "Dedukti is a proof-checker for the λΠ-calculus modulo