[PATCH] gnu: Add dedukti.

Done

Details

2 participants

Gabriel Hondet
Julien Lepiller

Owner: unassigned

Submitted by: Gabriel Hondet

Severity: normal

Debbugs page

Gabriel Hondet wrote 6 years ago

Recipients:(address . guix-patches@gnu.org)

Message-ID:871s65ykf7.fsf@gmail.com

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

---

gnu/packages/ocaml.scm | 55 ++++++++++++++++++++++++++++++++++++++++++

1 file changed, 55 insertions(+)

Toggle diff (65 lines)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

Julien Lepiller wrote 6 years ago

Recipients:(name . Gabriel Hondet)(address . gabrielhondet@gmail.com)(address . 33865@debbugs.gnu.org)

Message-ID:20181225123219.3c10f4ad@lepiller.eu

Le Tue, 25 Dec 2018 11:16:13 +0100,

Gabriel Hondet <gabrielhondet@gmail.com> a écrit :

Toggle quote (2 lines)

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

Nice! Thank you!

Toggle quote (38 lines)> ---
>  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...

Toggle quote (15 lines)> +    (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

Toggle quote (10 lines)

> + (replace 'build

> + (lambda _

> + (invoke "make")))

> + (replace 'check

> + (lambda _

> + (invoke "make" "tests")))

> + ;; (delete 'check)

Be carefull not to let this kind of thing slip through ;)

Toggle quote (9 lines)

> + (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?

Toggle quote (4 lines)

> + (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 ;)

Toggle quote (2 lines)

> + (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!

Gabriel Hondet wrote 6 years ago

Recipients:(name . Julien Lepiller)(address . julien@lepiller.eu)(address . 33865@debbugs.gnu.org)

Message-ID:87y38dwrlt.fsf@gmail.com

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

---

gnu/packages/ocaml.scm | 58 ++++++++++++++++++++++++++++++++++++++++++

1 file changed, 58 insertions(+)

Toggle diff (91 lines)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...

Julien Lepiller wrote 6 years ago

Recipients:(address . 33865-done@debbugs.gnu.org)

Message-ID:20181225185005.2177deb3@lepiller.eu

Pushed as 5895696e4c28938d9201e4527d3a007dd8b47e32.

I've slightly modified your patch to add a copyright line for yourself

and use the ocaml-build-system.

Closed

Your comment

This issue is archived.

To comment on this conversation send an email to 33865@debbugs.gnu.org

To respond to this issue using the mumi CLI, first switch to it

mumi current 33865

Then, you may apply the latest patchset in this issue (with sign off)

mumi am -- -s

Or, compose a reply to this issue

mumi compose

Or, send patches to this issue

mumi send-email *.patch

You may also tag this issue. See list of standard tags. For example, to set the confirmed and easy tags

mumi command -t +confirmed -t +easy

Or, remove the moreinfo tag and set the help tag

mumi command -t -moreinfo -t +help

is:open	open issues
is:done	closed issues
submitter:<who>	search issue submitter
author:<who>	search by message author
date:yesterday..now	search by issue date
mdate:3m..2d	search by message date