* [bug#33865] [PATCH] gnu: Add dedukti.
@ 2018-12-25 10:16 Gabriel Hondet
2018-12-25 11:32 ` Julien Lepiller
0 siblings, 1 reply; 4+ messages in thread
From: Gabriel Hondet @ 2018-12-25 10:16 UTC (permalink / raw)
To: 33865
[-- Attachment #1: Type: text/plain, Size: 2603 bytes --]
* gnu/packages/ocaml.scm (dedukti): New variable.
---
gnu/packages/ocaml.scm | 55 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 55 insertions(+)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 3b1ddcb5b..28e223e75 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -4989,3 +4989,58 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
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
+ `(("ocaml" ,ocaml)
+ ("menhir" ,ocaml-menhir)))
+ (native-inputs
+ `(("ocamlbuild" ,ocamlbuild)
+ ("ocamlfind" ,ocaml-findlib)
+ ("which" ,which)))
+ (build-system gnu-build-system)
+ (arguments
+ `(#:phases
+ (modify-phases %standard-phases
+ (replace 'configure
+ ;; Set ocamlfind environment vars
+ (lambda _
+ (let ((out (assoc-ref %outputs "out"))
+ (libpath "/lib/ocaml/site-lib"))
+ (begin
+ (setenv "OCAMLFIND_DESTDIR" (string-append out libpath))
+ (mkdir-p (string-append out libpath "/dedukti"))
+ (setenv "PREFIX" out)
+ #t))))
+ (replace 'build
+ (lambda _
+ (invoke "make")))
+ (replace 'check
+ (lambda _
+ (invoke "make" "tests")))
+ ;; (delete 'check)
+ (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")))))))))
+ (synopsis "Implementation of the ΛΠ-calculus modulo rewriting")
+ (description "Dedukti is a logical framework based on the
+ΛΠ-calculus modulo in which many theories and logics can be expressed.")
+ (license license:cecill-c)))
--
2.20.1
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]
^ permalink raw reply related [flat|nested] 4+ messages in thread
* [bug#33865] [PATCH] gnu: Add dedukti.
2018-12-25 10:16 [bug#33865] [PATCH] gnu: Add dedukti Gabriel Hondet
@ 2018-12-25 11:32 ` Julien Lepiller
2018-12-25 15:31 ` Gabriel Hondet
0 siblings, 1 reply; 4+ messages in thread
From: Julien Lepiller @ 2018-12-25 11:32 UTC (permalink / raw)
To: Gabriel Hondet; +Cc: 33865
Le Tue, 25 Dec 2018 11:16:13 +0100,
Gabriel Hondet <gabrielhondet@gmail.com> a écrit :
> * gnu/packages/ocaml.scm (dedukti): New variable.
Nice! Thank you!
> ---
> gnu/packages/ocaml.scm | 55
> ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55
> insertions(+)
>
> diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
> index 3b1ddcb5b..28e223e75 100644
> --- a/gnu/packages/ocaml.scm
> +++ b/gnu/packages/ocaml.scm
> @@ -4989,3 +4989,58 @@ provides BigN, BigZ, BigQ that used to be part
> of Coq standard library.") 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
> + `(("ocaml" ,ocaml)
> + ("menhir" ,ocaml-menhir)))
> + (native-inputs
> + `(("ocamlbuild" ,ocamlbuild)
> + ("ocamlfind" ,ocaml-findlib)
> + ("which" ,which)))
> + (build-system gnu-build-system)
I wonder why you didn't use the ocaml-build-system...
> + (arguments
> + `(#:phases
> + (modify-phases %standard-phases
> + (replace 'configure
> + ;; Set ocamlfind environment vars
> + (lambda _
> + (let ((out (assoc-ref %outputs "out"))
> + (libpath "/lib/ocaml/site-lib"))
> + (begin
> + (setenv "OCAMLFIND_DESTDIR" (string-append out
> libpath))
> + (mkdir-p (string-append out libpath "/dedukti"))
> + (setenv "PREFIX" out)
> + #t))))
It should automates all of this
> + (replace 'build
> + (lambda _
> + (invoke "make")))
> + (replace 'check
> + (lambda _
> + (invoke "make" "tests")))
> + ;; (delete 'check)
Be carefull not to let this kind of thing slip through ;)
> + (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")))))))))
> + (synopsis "Implementation of the ΛΠ-calculus modulo rewriting")
I don't think this synpsis is understandable to everyone. Could you use
instead a more general sentence that give an impression of what
ΛΠ-calculus modulo rewriting is?
> + (description "Dedukti is a logical framework based on the
> +ΛΠ-calculus modulo in which many theories and logics can be
> expressed.")
Or if you can't, please explain it with a sentence or two in the
description ;)
> + (license license:cecill-c)))
Other than that, looks good to me. I'll have to test it once you answer
my questions, and if it works, I'll push the patch for you. Thanks
again!
^ permalink raw reply [flat|nested] 4+ messages in thread
* [bug#33865] [PATCH] gnu: Add dedukti.
2018-12-25 11:32 ` Julien Lepiller
@ 2018-12-25 15:31 ` Gabriel Hondet
2018-12-25 17:50 ` bug#33865: " Julien Lepiller
0 siblings, 1 reply; 4+ messages in thread
From: Gabriel Hondet @ 2018-12-25 15:31 UTC (permalink / raw)
To: Julien Lepiller; +Cc: 33865
[-- Attachment #1: Type: text/plain, Size: 3776 bytes --]
* gnu/packages/ocaml.scm (dedukti): New variable.
---
gnu/packages/ocaml.scm | 58 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 58 insertions(+)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 3b1ddcb5b..8962a7339 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -4989,3 +4989,61 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
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
+ `(("ocaml" ,ocaml)
+ ("menhir" ,ocaml-menhir)))
+ (native-inputs
+ `(("ocamlbuild" ,ocamlbuild)
+ ("ocamlfind" ,ocaml-findlib)))
+ (build-system gnu-build-system)
+ (arguments
+ `(#:phases
+ (modify-phases %standard-phases
+ (replace 'configure
+ ;; Set ocamlfind environment vars
+ (lambda _
+ (let ((out (assoc-ref %outputs "out"))
+ (libpath "/lib/ocaml/site-lib"))
+ (begin
+ (setenv "OCAMLFIND_DESTDIR" (string-append out libpath))
+ (mkdir-p (string-append out libpath "/dedukti"))
+ (setenv "PREFIX" out)
+ #t))))
+ (replace 'build
+ (lambda _
+ (invoke "make")))
+ (replace 'check
+ (lambda _
+ (invoke "make" "tests")))
+ (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")))))))))
+ (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)))
--
2.20.1
On Tue 25 Dec 2018 at 12:32 Julien Lepiller wrote:
> I wonder why you didn't use the ocaml-build-system...
I'm not an expert yet regarding the different build systems, but the
current package essentially relies on a ~make~ and ~make install~
process, and is not linked with oasis or dune things (and using
ocaml-build-system failed as well, but perhaps I should investigate
more).
> I don't think this synpsis is understandable to everyone. Could you use
> instead a more general sentence that give an impression of what
> ΛΠ-calculus modulo rewriting is?
>
>> + (description "Dedukti is a logical framework based on the
>> +ΛΠ-calculus modulo in which many theories and logics can be
>> expressed.")
>
> Or if you can't, please explain it with a sentence or two in the
> description ;)
I hope the new one is clearer...
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]
^ permalink raw reply related [flat|nested] 4+ messages in thread
* bug#33865: [PATCH] gnu: Add dedukti.
2018-12-25 15:31 ` Gabriel Hondet
@ 2018-12-25 17:50 ` Julien Lepiller
0 siblings, 0 replies; 4+ messages in thread
From: Julien Lepiller @ 2018-12-25 17:50 UTC (permalink / raw)
To: 33865-done
[-- Attachment #1: Type: text/plain, Size: 160 bytes --]
Pushed as 5895696e4c28938d9201e4527d3a007dd8b47e32.
I've slightly modified your patch to add a copyright line for yourself
and use the ocaml-build-system.
[-- Attachment #2: Signature digitale OpenPGP --]
[-- Type: application/pgp-signature, Size: 833 bytes --]
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2018-12-25 17:51 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-12-25 10:16 [bug#33865] [PATCH] gnu: Add dedukti Gabriel Hondet
2018-12-25 11:32 ` Julien Lepiller
2018-12-25 15:31 ` Gabriel Hondet
2018-12-25 17:50 ` bug#33865: " Julien Lepiller
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.