GNU bug report logs - #33865
[PATCH] gnu: Add dedukti.

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 33865 in the body.
You can then email your comments to 33865 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Gabriel Hondet <gabrielhondet <at> gmail.com>
To: guix-patches <at> gnu.org
Subject: [PATCH] gnu: Add dedukti.
Date: Tue, 25 Dec 2018 11:16:13 +0100

[Message part 1 (text/plain, inline)]

* 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

[signature.asc (application/pgp-signature, inline)]

Message #8 received at 33865 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: Gabriel Hondet <gabrielhondet <at> gmail.com>
Cc: 33865 <at> debbugs.gnu.org
Subject: Re: [bug#33865] [PATCH] gnu: Add dedukti.
Date: Tue, 25 Dec 2018 12:32:24 +0100

Le Tue, 25 Dec 2018 11:16:13 +0100,
Gabriel Hondet <gabrielhondet <at> 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!

Message #11 received at 33865 <at> debbugs.gnu.org (full text, mbox):

From: Gabriel Hondet <gabrielhondet <at> gmail.com>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 33865 <at> debbugs.gnu.org
Subject: Re: [bug#33865] [PATCH] gnu: Add dedukti.
Date: Tue, 25 Dec 2018 16:31:10 +0100

[Message part 1 (text/plain, inline)]

* 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...

[signature.asc (application/pgp-signature, inline)]

Message #16 received at 33865-done <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 33865-done <at> debbugs.gnu.org
Subject: Re: [bug#33865] [PATCH] gnu: Add dedukti.
Date: Tue, 25 Dec 2018 18:50:05 +0100

[Message part 1 (text/plain, inline)]

Pushed as 5895696e4c28938d9201e4527d3a007dd8b47e32.

I've slightly modified your patch to add a copyright line for yourself
and use the ocaml-build-system.

[Message part 2 (application/pgp-signature, inline)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.