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

Previous Next

Full log

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!

Previous Next

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