GNU bug report logs - #34466
[PATCH] gnu: Add coq-equations.

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 34466 in the body.
You can then email your comments to 34466 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: Dan Frumin <dfrumin <at> cs.ru.nl>
To: guix-patches <at> gnu.org
Cc: Dan Frumin <dfrumin <at> cs.ru.nl>
Subject: [PATCH] gnu: Add coq-equations.
Date: Wed, 13 Feb 2019 11:40:24 +0100

---
 gnu/packages/coq.scm | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index fa02f85cd..494c3404b 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -500,3 +500,43 @@ work on a decision procedure for the equational theory of an extension of the
 sigma-calculus by Abadi et al.  The library is completely written in Coq and
 uses Ltac to synthesize the substitution operation.")
       (license license:bsd-3))))
+
+(define-public coq-equations
+  (package
+    (name "coq-equations")
+    (synopsis "Equations - a function definition plugin")
+    (version "1.2-beta")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append
+                    "https://github.com/mattam82/Coq-Equations/archive/v"
+                    version "-8.8.tar.gz"))
+              (file-name (string-append name "-v" version "8.8.tar.gz"))
+              (sha256
+               (base32 "1j7yarhddk2c2l4b6h8g5n0xz5vfy1bqmgh832g01di5gjwshy3f"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("findlib" ,ocaml)
+       ("coq"     ,coq)
+       ("camlp5"  ,camlp5)))
+    (arguments
+     `(#:test-target "test-suite"
+       #:phases
+       (modify-phases %standard-phases
+         (replace 'configure
+           (lambda* (#:key outputs #:allow-other-keys)
+             (invoke "coq_makefile" "-f" "_CoqProject" "-o" "Makefile")))
+         (replace 'install
+           (lambda* (#:key outputs #:allow-other-keys)
+             (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
+             (invoke "make"
+                     (string-append "COQLIB=" (assoc-ref outputs "out")
+                                    "/lib/coq/")
+                     "install"))))))
+    (description "Equations provides a notation for writing programs
+by dependent pattern-matching and (well-founded) recursion in Coq. It
+compiles everything down to eliminators for inductive types, equality
+and accessibility, providing a definitional extension to the Coq
+kernel.")
+    (home-page "https://mattam82.github.io/Coq-Equations/")
+    (license license:lgpl2.1)))
-- 
2.17.1

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

From: Julien Lepiller <julien <at> lepiller.eu>
To: Dan Frumin <dfrumin <at> cs.ru.nl>
Cc: 34466 <at> debbugs.gnu.org
Subject: Re: [bug#34466] [PATCH] gnu: Add coq-equations.
Date: Wed, 13 Feb 2019 12:04:48 +0100

Le 2019-02-13 11:40, Dan Frumin a écrit :
> ---
>  gnu/packages/coq.scm | 40 ++++++++++++++++++++++++++++++++++++++++
>  1 file changed, 40 insertions(+)
> 
> diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
> index fa02f85cd..494c3404b 100644
> --- a/gnu/packages/coq.scm
> +++ b/gnu/packages/coq.scm
> @@ -500,3 +500,43 @@ work on a decision procedure for the equational
> theory of an extension of the
>  sigma-calculus by Abadi et al.  The library is completely written in 
> Coq and
>  uses Ltac to synthesize the substitution operation.")
>        (license license:bsd-3))))

Hi Dan, thanks for this patch! I have some comments below to help 
improve the
quality of future patches, as well as two questions you need to answer 
before
I can push that patch.

> +
> +(define-public coq-equations
> +  (package
> +    (name "coq-equations")
> +    (synopsis "Equations - a function definition plugin")

Could you put this just before the description field, so this package 
definition
looks more like the rest of guix? A better synopsis would be "Function 
definiton
plugin for coq" I think.

> +    (version "1.2-beta")

Why a beta version? We try to stick to stable releases in Guix. Please 
add a
comment explaining the reason.

> +    (source (origin
> +              (method url-fetch)
> +              (uri (string-append
> +                    
> "https://github.com/mattam82/Coq-Equations/archive/v"
> +                    version "-8.8.tar.gz"))
> +              (file-name (string-append name "-v" version 
> "8.8.tar.gz"))

We cannot use auto-generated tarballs from github, because we found that
they sometimes get regenerated in an unreproducible way, so it breaks 
the
checksum test. You can use this instead:

(method git-fetch)
(uri (git-reference
       (url "https://githu.com/mattam82/Coq-Equations.git")
       (commit (string-append "v" version "-8.8"))))

and update the sha256 accordingly. As an added bonus, this means that we
can always fetch from the software heritage in case the repo disappears
one day :)

> +              (sha256
> +               (base32
> "1j7yarhddk2c2l4b6h8g5n0xz5vfy1bqmgh832g01di5gjwshy3f"))))
> +    (build-system gnu-build-system)
> +    (native-inputs
> +     `(("findlib" ,ocaml)

ocaml doesn't provide findlib directly, ocaml-findlib does. What do you
want to do here?

> +       ("coq"     ,coq)
> +       ("camlp5"  ,camlp5)))
> +    (arguments
> +     `(#:test-target "test-suite"
> +       #:phases
> +       (modify-phases %standard-phases
> +         (replace 'configure
> +           (lambda* (#:key outputs #:allow-other-keys)
> +             (invoke "coq_makefile" "-f" "_CoqProject" "-o" 
> "Makefile")))
> +         (replace 'install
> +           (lambda* (#:key outputs #:allow-other-keys)
> +             (setenv "COQLIB" (string-append (assoc-ref outputs
> "out") "/lib/coq/"))
> +             (invoke "make"
> +                     (string-append "COQLIB=" (assoc-ref outputs 
> "out")
> +                                    "/lib/coq/")
> +                     "install"))))))

Please make sure that these two phases both return #t.

> +    (description "Equations provides a notation for writing programs
> +by dependent pattern-matching and (well-founded) recursion in Coq. It
> +compiles everything down to eliminators for inductive types, equality
> +and accessibility, providing a definitional extension to the Coq
> +kernel.")

Please make sure that each sentence is separated by two spaces.
`guix lint coq-equations` should be able to tell you about it.

> +    (home-page "https://mattam82.github.io/Coq-Equations/")
> +    (license license:lgpl2.1)))

Thanks again! I really only need an answer for the beta version and
ocaml/findlib questions. I can take care of the rest, but I would
appreciate it if you could do it yourself ;)

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

From: Dan Frumin <dfrumin <at> cs.ru.nl>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 34466 <at> debbugs.gnu.org
Subject: Re: [bug#34466] [PATCH] gnu: Add coq-equations.
Date: Wed, 13 Feb 2019 12:35:29 +0100

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

Hi Julien.

Thank you for your thorough comments, I really appreciate it!
I hope that the quality of my patches increase in time so please bear with me for a bit :)

On 13-02-19 12:04, Julien Lepiller wrote:
> Le 2019-02-13 11:40, Dan Frumin a écrit :
>> ---
>>  gnu/packages/coq.scm | 40 ++++++++++++++++++++++++++++++++++++++++
>>  1 file changed, 40 insertions(+)
>>
>> diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
>> index fa02f85cd..494c3404b 100644
>> --- a/gnu/packages/coq.scm
>> +++ b/gnu/packages/coq.scm
>> @@ -500,3 +500,43 @@ work on a decision procedure for the equational
>> theory of an extension of the
>>  sigma-calculus by Abadi et al.  The library is completely written in Coq and
>>  uses Ltac to synthesize the substitution operation.")
>>        (license license:bsd-3))))
> 
> Hi Dan, thanks for this patch! I have some comments below to help improve the
> quality of future patches, as well as two questions you need to answer before
> I can push that patch.
> 
>> +
>> +(define-public coq-equations
>> +  (package
>> +    (name "coq-equations")
>> +    (synopsis "Equations - a function definition plugin")
> 
> Could you put this just before the description field, so this package definition
> looks more like the rest of guix? A better synopsis would be "Function definiton
> plugin for coq" I think.

I've reordered the fields to match the rest of the package definitions in guix.

> 
>> +    (version "1.2-beta")
> 
> Why a beta version? We try to stick to stable releases in Guix. Please add a
> comment explaining the reason.
> 

Oh, I just wanted to use the latest released version. I can replace it with the version 1.1 while I wait for the non-beta 1.2 releas.

>> +    (source (origin
>> +              (method url-fetch)
>> +              (uri (string-append
>> + "https://github.com/mattam82/Coq-Equations/archive/v"
>> +                    version "-8.8.tar.gz"))
>> +              (file-name (string-append name "-v" version "8.8.tar.gz"))
> 
> We cannot use auto-generated tarballs from github, because we found that
> they sometimes get regenerated in an unreproducible way, so it breaks the
> checksum test. You can use this instead:
> 
> (method git-fetch)
> (uri (git-reference
>         (url "https://githu.com/mattam82/Coq-Equations.git")
>         (commit (string-append "v" version "-8.8"))))
> 
> and update the sha256 accordingly. As an added bonus, this means that we
> can always fetch from the software heritage in case the repo disappears
> one day :)

I was not aware of that. How can I get the sha256 hash in this case? Normally I would do `guix download <url>`.

> 
>> +              (sha256
>> +               (base32
>> "1j7yarhddk2c2l4b6h8g5n0xz5vfy1bqmgh832g01di5gjwshy3f"))))
>> +    (build-system gnu-build-system)
>> +    (native-inputs
>> +     `(("findlib" ,ocaml)
> 
> ocaml doesn't provide findlib directly, ocaml-findlib does. What do you
> want to do here?

Sorry, I think I was confused here. I've corrected this in the updated patch.

> 
>> +       ("coq"     ,coq)
>> +       ("camlp5"  ,camlp5)))
>> +    (arguments
>> +     `(#:test-target "test-suite"
>> +       #:phases
>> +       (modify-phases %standard-phases
>> +         (replace 'configure
>> +           (lambda* (#:key outputs #:allow-other-keys)
>> +             (invoke "coq_makefile" "-f" "_CoqProject" "-o" "Makefile")))
>> +         (replace 'install
>> +           (lambda* (#:key outputs #:allow-other-keys)
>> +             (setenv "COQLIB" (string-append (assoc-ref outputs
>> "out") "/lib/coq/"))
>> +             (invoke "make"
>> +                     (string-append "COQLIB=" (assoc-ref outputs "out")
>> +                                    "/lib/coq/")
>> +                     "install"))))))
> 
> Please make sure that these two phases both return #t.

I thought that `invoke' automatically checks that the return code is correct?

> 
>> +    (description "Equations provides a notation for writing programs
>> +by dependent pattern-matching and (well-founded) recursion in Coq. It
>> +compiles everything down to eliminators for inductive types, equality
>> +and accessibility, providing a definitional extension to the Coq
>> +kernel.")
> 
> Please make sure that each sentence is separated by two spaces.
> `guix lint coq-equations` should be able to tell you about it.
> 
>> +    (home-page "https://mattam82.github.io/Coq-Equations/")
>> +    (license license:lgpl2.1)))
> 
> Thanks again! I really only need an answer for the beta version and
> ocaml/findlib questions. I can take care of the rest, but I would
> appreciate it if you could do it yourself ;)

[0001-gnu-Add-coq-equations.patch (text/x-patch, attachment)]

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

From: Dan Frumin <dfrumin <at> cs.ru.nl>
To: 34466 <at> debbugs.gnu.org
Subject: Fwd: Re: [bug#34466] [PATCH] gnu: Add coq-equations.
Date: Wed, 13 Feb 2019 12:36:59 +0100

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

(sorry, sending this again because I forgot to CC the bugtracker)


Hi Julien.

Thank you for your thorough comments, I really appreciate it!
I hope that the quality of my patches increase in time so please bear with me for a bit :)

On 13-02-19 12:04, Julien Lepiller wrote:
> Le 2019-02-13 11:40, Dan Frumin a écrit :
>> ---
>>  gnu/packages/coq.scm | 40 ++++++++++++++++++++++++++++++++++++++++
>>  1 file changed, 40 insertions(+)
>>
>> diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
>> index fa02f85cd..494c3404b 100644
>> --- a/gnu/packages/coq.scm
>> +++ b/gnu/packages/coq.scm
>> @@ -500,3 +500,43 @@ work on a decision procedure for the equational
>> theory of an extension of the
>>  sigma-calculus by Abadi et al.  The library is completely written in Coq and
>>  uses Ltac to synthesize the substitution operation.")
>>        (license license:bsd-3))))
> 
> Hi Dan, thanks for this patch! I have some comments below to help improve the
> quality of future patches, as well as two questions you need to answer before
> I can push that patch.
> 
>> +
>> +(define-public coq-equations
>> +  (package
>> +    (name "coq-equations")
>> +    (synopsis "Equations - a function definition plugin")
> 
> Could you put this just before the description field, so this package definition
> looks more like the rest of guix? A better synopsis would be "Function definiton
> plugin for coq" I think.

I've reordered the fields to match the rest of the package definitions in guix.

> 
>> +    (version "1.2-beta")
> 
> Why a beta version? We try to stick to stable releases in Guix. Please add a
> comment explaining the reason.
> 

Oh, I just wanted to use the latest released version. I can replace it with the version 1.1 while I wait for the non-beta 1.2 releas.

>> +    (source (origin
>> +              (method url-fetch)
>> +              (uri (string-append
>> + "https://github.com/mattam82/Coq-Equations/archive/v"
>> +                    version "-8.8.tar.gz"))
>> +              (file-name (string-append name "-v" version "8.8.tar.gz"))
> 
> We cannot use auto-generated tarballs from github, because we found that
> they sometimes get regenerated in an unreproducible way, so it breaks the
> checksum test. You can use this instead:
> 
> (method git-fetch)
> (uri (git-reference
>         (url "https://githu.com/mattam82/Coq-Equations.git")
>         (commit (string-append "v" version "-8.8"))))
> 
> and update the sha256 accordingly. As an added bonus, this means that we
> can always fetch from the software heritage in case the repo disappears
> one day :)

I was not aware of that. How can I get the sha256 hash in this case? Normally I would do `guix download <url>`.

> 
>> +              (sha256
>> +               (base32
>> "1j7yarhddk2c2l4b6h8g5n0xz5vfy1bqmgh832g01di5gjwshy3f"))))
>> +    (build-system gnu-build-system)
>> +    (native-inputs
>> +     `(("findlib" ,ocaml)
> 
> ocaml doesn't provide findlib directly, ocaml-findlib does. What do you
> want to do here?

Sorry, I think I was confused here. I've corrected this in the updated patch.

> 
>> +       ("coq"     ,coq)
>> +       ("camlp5"  ,camlp5)))
>> +    (arguments
>> +     `(#:test-target "test-suite"
>> +       #:phases
>> +       (modify-phases %standard-phases
>> +         (replace 'configure
>> +           (lambda* (#:key outputs #:allow-other-keys)
>> +             (invoke "coq_makefile" "-f" "_CoqProject" "-o" "Makefile")))
>> +         (replace 'install
>> +           (lambda* (#:key outputs #:allow-other-keys)
>> +             (setenv "COQLIB" (string-append (assoc-ref outputs
>> "out") "/lib/coq/"))
>> +             (invoke "make"
>> +                     (string-append "COQLIB=" (assoc-ref outputs "out")
>> +                                    "/lib/coq/")
>> +                     "install"))))))
> 
> Please make sure that these two phases both return #t.

I thought that `invoke' automatically checks that the return code is correct?

> 
>> +    (description "Equations provides a notation for writing programs
>> +by dependent pattern-matching and (well-founded) recursion in Coq. It
>> +compiles everything down to eliminators for inductive types, equality
>> +and accessibility, providing a definitional extension to the Coq
>> +kernel.")
> 
> Please make sure that each sentence is separated by two spaces.
> `guix lint coq-equations` should be able to tell you about it.
> 
>> +    (home-page "https://mattam82.github.io/Coq-Equations/")
>> +    (license license:lgpl2.1)))
> 
> Thanks again! I really only need an answer for the beta version and
> ocaml/findlib questions. I can take care of the rest, but I would
> appreciate it if you could do it yourself ;)

[0001-gnu-Add-coq-equations.patch (text/x-patch, attachment)]

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

From: Julien Lepiller <julien <at> lepiller.eu>
To: Dan Frumin <dfrumin <at> cs.ru.nl>
Cc: 34466 <at> debbugs.gnu.org
Subject: Re: [bug#34466] Fwd: Re: [bug#34466] [PATCH] gnu: Add coq-equations.
Date: Wed, 13 Feb 2019 13:19:32 +0100

Le 2019-02-13 12:36, Dan Frumin a écrit :
> (sorry, sending this again because I forgot to CC the bugtracker)
> 
> 
> Hi Julien.
> 
> Thank you for your thorough comments, I really appreciate it!
> I hope that the quality of my patches increase in time so please bear
> with me for a bit :)
> 
> On 13-02-19 12:04, Julien Lepiller wrote:
>> 
>> We cannot use auto-generated tarballs from github, because we found 
>> that
>> they sometimes get regenerated in an unreproducible way, so it breaks 
>> the
>> checksum test. You can use this instead:
>> 
>> (method git-fetch)
>> (uri (git-reference
>>         (url "https://githu.com/mattam82/Coq-Equations.git")
>>         (commit (string-append "v" version "-8.8"))))
>> 
>> and update the sha256 accordingly. As an added bonus, this means that 
>> we
>> can always fetch from the software heritage in case the repo 
>> disappears
>> one day :)
> 
> I was not aware of that. How can I get the sha256 hash in this case?
> Normally I would do `guix download <url>`.

you can always try to build the package, which will fail and tell you
what the correct hash was. I forgot, the filename should be:

(file-name (git-file-name name version))

>> 
>> Please make sure that these two phases both return #t.
> 
> I thought that `invoke' automatically checks that the return code is 
> correct?

It does, and when the code is not correct, it throws an exception. When 
it is
correct, it returns #<unspecified>, so we need to explicitly return #t.

Thank you! I'll try to build the package and take care of the rest 
before pushing
your patch later today.

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

From: Danny Milosavljevic <dannym <at> scratchpost.org>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 34466 <at> debbugs.gnu.org, Dan Frumin <dfrumin <at> cs.ru.nl>
Subject: Re: [bug#34466] Fwd: Re: [bug#34466] [PATCH] gnu: Add coq-equations.
Date: Wed, 13 Feb 2019 13:39:24 +0100

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

Hi Julien,

> When [invoke's child return status] is correct, [invoke] returns #<unspecified>, so we need to explicitly return #t.

That's not true.  invoke returns #t in the successful case--I designed it that way mostly to get rid of the many vestigal #t's in phases.

(I hope that in a future version of guix, the necessity of using #t to end phases will be gone entirely)

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

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

From: Julien Lepiller <julien <at> lepiller.eu>
To: Danny Milosavljevic <dannym <at> scratchpost.org>
Cc: 34466 <at> debbugs.gnu.org, Dan Frumin <dfrumin <at> cs.ru.nl>
Subject: Re: [bug#34466] Fwd: Re: [bug#34466] [PATCH] gnu: Add coq-equations.
Date: Wed, 13 Feb 2019 13:45:43 +0100

Le 2019-02-13 13:39, Danny Milosavljevic a écrit :
> Hi Julien,
> 
>> When [invoke's child return status] is correct, [invoke] returns 
>> #<unspecified>, so we need to explicitly return #t.
> 
> That's not true.  invoke returns #t in the successful case--I designed
> it that way mostly to get rid of the many vestigal #t's in phases.
> 
> (I hope that in a future version of guix, the necessity of using #t to
> end phases will be gone entirely)

Ah, thanks for the info! So I guess we don't need to end any phase with 
#t
in that package definition, correct?

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

From: Danny Milosavljevic <dannym <at> scratchpost.org>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 34466 <at> debbugs.gnu.org, Dan Frumin <dfrumin <at> cs.ru.nl>
Subject: Re: [bug#34466] Fwd: Re: [bug#34466] [PATCH] gnu: Add coq-equations.
Date: Wed, 13 Feb 2019 14:23:23 +0100

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

On Wed, 13 Feb 2019 13:45:43 +0100
Julien Lepiller <julien <at> lepiller.eu> wrote:

> Ah, thanks for the info! So I guess we don't need to end any phase with 
> #t
> in that package definition, correct?

Correct.

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

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

From: Julien Lepiller <julien <at> lepiller.eu>
To: 34466-done <at> debbugs.gnu.org
Subject: Re: [bug#34466] [PATCH] gnu: Add coq-equations.
Date: Wed, 13 Feb 2019 22:22:54 +0100

Pushed as ec23bae682ab144179fad8d5ed6c2545d85384ad, thank you!

Previous Next

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