* [bug#34466] [PATCH] gnu: Add coq-equations. @ 2019-02-13 10:40 Dan Frumin 2019-02-13 11:04 ` Julien Lepiller 2019-02-13 21:22 ` bug#34466: " Julien Lepiller 0 siblings, 2 replies; 9+ messages in thread From: Dan Frumin @ 2019-02-13 10:40 UTC (permalink / raw) To: 34466; +Cc: Dan Frumin --- 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 ^ permalink raw reply related [flat|nested] 9+ messages in thread
* [bug#34466] [PATCH] gnu: Add coq-equations. 2019-02-13 10:40 [bug#34466] [PATCH] gnu: Add coq-equations Dan Frumin @ 2019-02-13 11:04 ` Julien Lepiller 2019-02-13 11:35 ` Dan Frumin 2019-02-13 21:22 ` bug#34466: " Julien Lepiller 1 sibling, 1 reply; 9+ messages in thread From: Julien Lepiller @ 2019-02-13 11:04 UTC (permalink / raw) To: Dan Frumin; +Cc: 34466 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 ;) ^ permalink raw reply [flat|nested] 9+ messages in thread
* [bug#34466] [PATCH] gnu: Add coq-equations. 2019-02-13 11:04 ` Julien Lepiller @ 2019-02-13 11:35 ` Dan Frumin 2019-02-13 11:36 ` [bug#34466] Fwd: " Dan Frumin 0 siblings, 1 reply; 9+ messages in thread From: Dan Frumin @ 2019-02-13 11:35 UTC (permalink / raw) To: Julien Lepiller; +Cc: 34466 [-- Attachment #1: Type: text/plain, Size: 4955 bytes --] 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 ;) [-- Attachment #2: 0001-gnu-Add-coq-equations.patch --] [-- Type: text/x-patch, Size: 2406 bytes --] From ebbb6e1cb1f667f33cc4e4320fdb91edf33264dc Mon Sep 17 00:00:00 2001 From: Dan Frumin <dfrumin@cs.ru.nl> Date: Wed, 13 Feb 2019 12:34:40 +0100 Subject: [PATCH] gnu: Add coq-equations. --- gnu/packages/coq.scm | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index fa02f85cd..b7eadc2fd 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") + (version "1.1") + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/mattam82/Coq-Equations.git") + (commit (string-append "v" version "-8.8")))) + (file-name (git-file-name name version)) + (sha256 + (base32 "129rxsdsf88vjcw0xhm74yax1hmnk6f8n9ksg0hcyyjq1ijddiwa")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,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")))))) + (home-page "https://mattam82.github.io/Coq-Equations/") + (synopsis "Function definition plugin for Coq") + (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.") + (license license:lgpl2.1))) -- 2.17.1 ^ permalink raw reply related [flat|nested] 9+ messages in thread
* [bug#34466] Fwd: Re: [bug#34466] [PATCH] gnu: Add coq-equations. 2019-02-13 11:35 ` Dan Frumin @ 2019-02-13 11:36 ` Dan Frumin 2019-02-13 12:19 ` Julien Lepiller 0 siblings, 1 reply; 9+ messages in thread From: Dan Frumin @ 2019-02-13 11:36 UTC (permalink / raw) To: 34466 [-- Attachment #1: Type: text/plain, Size: 5025 bytes --] (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 ;) [-- Attachment #2: 0001-gnu-Add-coq-equations.patch --] [-- Type: text/x-patch, Size: 2407 bytes --] From ebbb6e1cb1f667f33cc4e4320fdb91edf33264dc Mon Sep 17 00:00:00 2001 From: Dan Frumin <dfrumin@cs.ru.nl> Date: Wed, 13 Feb 2019 12:34:40 +0100 Subject: [PATCH] gnu: Add coq-equations. --- gnu/packages/coq.scm | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index fa02f85cd..b7eadc2fd 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") + (version "1.1") + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/mattam82/Coq-Equations.git") + (commit (string-append "v" version "-8.8")))) + (file-name (git-file-name name version)) + (sha256 + (base32 "129rxsdsf88vjcw0xhm74yax1hmnk6f8n9ksg0hcyyjq1ijddiwa")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,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")))))) + (home-page "https://mattam82.github.io/Coq-Equations/") + (synopsis "Function definition plugin for Coq") + (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.") + (license license:lgpl2.1))) -- 2.17.1 ^ permalink raw reply related [flat|nested] 9+ messages in thread
* [bug#34466] Fwd: Re: [bug#34466] [PATCH] gnu: Add coq-equations. 2019-02-13 11:36 ` [bug#34466] Fwd: " Dan Frumin @ 2019-02-13 12:19 ` Julien Lepiller 2019-02-13 12:39 ` Danny Milosavljevic 0 siblings, 1 reply; 9+ messages in thread From: Julien Lepiller @ 2019-02-13 12:19 UTC (permalink / raw) To: Dan Frumin; +Cc: 34466 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. ^ permalink raw reply [flat|nested] 9+ messages in thread
* [bug#34466] Fwd: Re: [bug#34466] [PATCH] gnu: Add coq-equations. 2019-02-13 12:19 ` Julien Lepiller @ 2019-02-13 12:39 ` Danny Milosavljevic 2019-02-13 12:45 ` Julien Lepiller 0 siblings, 1 reply; 9+ messages in thread From: Danny Milosavljevic @ 2019-02-13 12:39 UTC (permalink / raw) To: Julien Lepiller; +Cc: Dan Frumin, 34466 [-- Attachment #1: Type: text/plain, Size: 383 bytes --] 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) [-- Attachment #2: OpenPGP digital signature --] [-- Type: application/pgp-signature, Size: 488 bytes --] ^ permalink raw reply [flat|nested] 9+ messages in thread
* [bug#34466] Fwd: Re: [bug#34466] [PATCH] gnu: Add coq-equations. 2019-02-13 12:39 ` Danny Milosavljevic @ 2019-02-13 12:45 ` Julien Lepiller 2019-02-13 13:23 ` Danny Milosavljevic 0 siblings, 1 reply; 9+ messages in thread From: Julien Lepiller @ 2019-02-13 12:45 UTC (permalink / raw) To: Danny Milosavljevic; +Cc: Dan Frumin, 34466 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? ^ permalink raw reply [flat|nested] 9+ messages in thread
* [bug#34466] Fwd: Re: [bug#34466] [PATCH] gnu: Add coq-equations. 2019-02-13 12:45 ` Julien Lepiller @ 2019-02-13 13:23 ` Danny Milosavljevic 0 siblings, 0 replies; 9+ messages in thread From: Danny Milosavljevic @ 2019-02-13 13:23 UTC (permalink / raw) To: Julien Lepiller; +Cc: Dan Frumin, 34466 [-- Attachment #1: Type: text/plain, Size: 217 bytes --] On Wed, 13 Feb 2019 13:45:43 +0100 Julien Lepiller <julien@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. [-- Attachment #2: OpenPGP digital signature --] [-- Type: application/pgp-signature, Size: 488 bytes --] ^ permalink raw reply [flat|nested] 9+ messages in thread
* bug#34466: [PATCH] gnu: Add coq-equations. 2019-02-13 10:40 [bug#34466] [PATCH] gnu: Add coq-equations Dan Frumin 2019-02-13 11:04 ` Julien Lepiller @ 2019-02-13 21:22 ` Julien Lepiller 1 sibling, 0 replies; 9+ messages in thread From: Julien Lepiller @ 2019-02-13 21:22 UTC (permalink / raw) To: 34466-done Pushed as ec23bae682ab144179fad8d5ed6c2545d85384ad, thank you! ^ permalink raw reply [flat|nested] 9+ messages in thread
end of thread, other threads:[~2019-02-13 21:24 UTC | newest] Thread overview: 9+ messages (download: mbox.gz follow: Atom feed -- links below jump to the message on this page -- 2019-02-13 10:40 [bug#34466] [PATCH] gnu: Add coq-equations Dan Frumin 2019-02-13 11:04 ` Julien Lepiller 2019-02-13 11:35 ` Dan Frumin 2019-02-13 11:36 ` [bug#34466] Fwd: " Dan Frumin 2019-02-13 12:19 ` Julien Lepiller 2019-02-13 12:39 ` Danny Milosavljevic 2019-02-13 12:45 ` Julien Lepiller 2019-02-13 13:23 ` Danny Milosavljevic 2019-02-13 21:22 ` bug#34466: " Julien Lepiller
Code repositories for project(s) associated with this public inbox https://git.savannah.gnu.org/cgit/guix.git This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).