[PATCH 0/2] gnu: coq-mathcomp-bigenough: Use native-inputs.

  • Done
  • quality assurance status badge
Details
2 participants
  • Jean-Pierre De Jesus DIAZ
  • Ludovic Courtès
Owner
unassigned
Submitted by
Jean-Pierre De Jesus DIAZ
Severity
normal
J
J
Jean-Pierre De Jesus DIAZ wrote on 16 Sep 17:28 +0200
(address . guix-patches@gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
cover.1726500406.git.jean@foundation.xyz
This simplifies the coq-mathcomp-bigenough package by removing uneeded
make flags and also moves coq and which from propagated-inputs to
native-inputs.

Jean-Pierre De Jesus DIAZ (2):
gnu: coq-mathcomp-bigenough: Use new style.
gnu: coq-mathcomp-bigenough: Use native-inputs.

gnu/packages/coq.scm | 28 ++++++++++++----------------
1 file changed, 12 insertions(+), 16 deletions(-)


base-commit: ee64bcfb796ef36db4b63f79540627fb25f3320a
--
2.46.0
J
J
Jean-Pierre De Jesus DIAZ wrote on 16 Sep 17:29 +0200
[PATCH 1/2] gnu: coq-mathcomp-bigenough: Use new style.
(address . 73298@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
aa2f8b5a506d2558c2a1d2c0884bec9d2cfd012c.1726500406.git.jean@foundation.xyz
* gnu/packages/coq.scm (coq-mathcomp-bigenough) [arguments]: Use new
style and remove uneeded make flags.

Change-Id: I11a6350a10cedd682cf598ecb8660b63a12aa00d
---
gnu/packages/coq.scm | 25 ++++++++++---------------
1 file changed, 10 insertions(+), 15 deletions(-)

Toggle diff (38 lines)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 31d1e8d51d..166657fdd1 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -753,21 +753,16 @@ (define-public coq-mathcomp-bigenough
"02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw"))))
(build-system gnu-build-system)
(arguments
- `(;; No references to tests in Makefile.common.
- ;; It doesn't appear as though tests will be included
- ;; by the packaged project in the future.
- #:tests? #f
- #:make-flags ,#~(list (string-append "COQBIN="
- #$(this-package-input "coq")
- "/bin/")
- (string-append "COQMF_COQLIB="
- (assoc-ref %outputs "out")
- "/lib/ocaml/site-lib/coq")
- (string-append "COQLIBINSTALL="
- (assoc-ref %outputs "out")
- "/lib/coq/user-contrib"))
- #:phases (modify-phases %standard-phases
- (delete 'configure))))
+ (list ;; No references to tests in Makefile.common.
+ ;; It doesn't appear as though tests will be included
+ ;; by the packaged project in the future.
+ #:tests? #f
+ #:make-flags
+ #~(list (string-append "COQLIBINSTALL=" #$output
+ "/lib/coq/user-contrib"))
+ #:phases
+ #~(modify-phases %standard-phases
+ (delete 'configure))))
(propagated-inputs (list coq coq-mathcomp which))
(home-page "https://math-comp.github.io/")
(synopsis "Small library to do epsilon - N reasoning")
--
2.46.0
J
J
Jean-Pierre De Jesus DIAZ wrote on 16 Sep 17:29 +0200
[PATCH 2/2] gnu: coq-mathcomp-bigenough: Use native-inputs.
(address . 73298@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
3c51f9cc018a15ad07c37443773482bc96b24674.1726500406.git.jean@foundation.xyz
* gnu/packages/coq.scm (coq-mathcomp-bigenough) [propagated-inputs]:
Move coq and which from here...
[native-inputs]: ... to here.

Change-Id: I1a57175b69f6b4a5eba308bf60c9e74437563f58
---
gnu/packages/coq.scm | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)

Toggle diff (16 lines)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 166657fdd1..ea0868f226 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -763,7 +763,8 @@ (define-public coq-mathcomp-bigenough
#:phases
#~(modify-phases %standard-phases
(delete 'configure))))
- (propagated-inputs (list coq coq-mathcomp which))
+ (native-inputs (list coq which))
+ (propagated-inputs (list coq-mathcomp))
(home-page "https://math-comp.github.io/")
(synopsis "Small library to do epsilon - N reasoning")
(description
--
2.46.0
L
L
Ludovic Courtès wrote on 17 Nov 23:02 +0100
Re: [bug#73298] [PATCH 0/2] gnu: coq-mathcomp-bigenough: Use native-inputs.
(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
8734jpikn5.fsf@gnu.org
Hi,

Jean-Pierre De Jesus DIAZ <jean@foundation.xyz> skribis:

Toggle quote (8 lines)
> This simplifies the coq-mathcomp-bigenough package by removing uneeded
> make flags and also moves coq and which from propagated-inputs to
> native-inputs.
>
> Jean-Pierre De Jesus DIAZ (2):
> gnu: coq-mathcomp-bigenough: Use new style.
> gnu: coq-mathcomp-bigenough: Use native-inputs.

I went ahead and applied both, even though I’m not on the Coq/OCaml
team.

I think you should consider joining that team (Julien, pukkamustard,
perhaps you could use some help?) and probably applying for commit
rights as well.

Thanks,
Ludo’.
Closed
?
Your comment

This issue is archived.

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

To respond to this issue using the mumi CLI, first switch to it
mumi current 73298
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