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

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

[Jean-Pierre De Jesus DIAZ]

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

[bug#73298] [PATCH 1/2] gnu: coq-mathcomp-bigenough: Use new style.

[Jean-Pierre De Jesus DIAZ]

* 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(-)

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

[bug#73298] [PATCH 2/2] gnu: coq-mathcomp-bigenough: Use native-inputs.

[Jean-Pierre De Jesus DIAZ]

* 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(-)

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

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

[Ludovic Courtès]

Hi,

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

> 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’.