ryan77627/guix
1
0
Fork 0
mirror of https://git.in.rschanz.org/ryan77627/guix.git synced 2024-12-24 21:38:07 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

gnu: Add dedukti.

Browse source 
* gnu/packages/ocaml.scm (dedukti): New variable.

Signed-off-by: Julien Lepiller <julien@lepiller.eu>
This commit is contained in:
Gabriel Hondet 2018-12-25 16:31:10 +01:00 committed by Julien Lepiller
parent d8dcbcc91d
commit 5895696e4c
No known key found for this signature in database
GPG key ID: 43111F4520086A0C
1 changed files with 55 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

55
gnu/packages/ocaml.scm
View file

@ -10,6 +10,7 @@
;;; Copyright © 2017 Ben Woodcroft <donttrustben@gmail.com>
;;; Copyright © 2017, 2018 Tobias Geerinckx-Rice <me@tobias.gr>
;;; Copyright © 2018 Peter Kreye <kreyepr@gmail.com>
;;; Copyright © 2018 Gabriel Hondet <gabrielhondet@gmail.com>
;;;
;;; This file is part of GNU Guix.
;;;
@ -4989,3 +4990,57 @@ (define-public coq-interval
simplifying the proofs of inequalities on expressions of real numbers for the
Coq proof assistant.")
(license license:cecill-c)))
(define-public dedukti
(package
(name "dedukti")
(version "2.6.0")
(home-page "https://deducteam.github.io/")
(source
(origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/deducteam/dedukti.git")
(commit (string-append "v" version))))
(file-name (git-file-name name version))
(sha256
(base32
"0frl3diff033i4fmq304b8wbsdnc9mvlhmwd7a3zd699ng2lzbxb"))))
(inputs
`(("menhir" ,ocaml-menhir)))
(native-inputs
`(("ocamlbuild" ,ocamlbuild)))
(build-system ocaml-build-system)
(arguments
`(#:phases
(modify-phases %standard-phases
(delete 'configure)
(replace 'build
(lambda _
(invoke "make")
#t))
(replace 'check
(lambda _
(invoke "make" "tests")
#t))
(add-before 'install 'set-binpath
;; Change binary path in the makefile
(lambda _
(let ((out (assoc-ref %outputs "out")))
(substitute* "GNUmakefile"
(("BINDIR = (.*)$")
(string-append "BINDIR = " out "/bin"))))
#t))
(replace 'install
(lambda _
(invoke "make" "install")
#t)))))
(synopsis "Proof-checker for the λΠ-calculus modulo theory, an extension of
the λ-calculus")
(description "Dedukti is a proof-checker for the λΠ-calculus modulo
theory. The λΠ-calculus is an extension of the simply typed λ-calculus with
dependent types. The λΠ-calculus modulo theory is itself an extension of the
λΠ-calculus where the context contains variable declaration as well as rewrite
rules. This system is not designed to develop proofs, but to check proofs
developed in other systems. In particular, it enjoys a minimalistic syntax.")
(license license:cecill-c)))