[bug#73237] [PATCH] gnu: Add coq-ceres.

[bug#73237] [PATCH] gnu: Add coq-ceres.

[Antero Mejr via Guix-patches via]

* gnu/packages/coq.scm (coq-ceres): New variable.

Change-Id: I366aa3ad38a25bbcbaa70874241a22fb45d41938
---
 gnu/packages/coq.scm | 54 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 31d1e8d51d..6417b3ea48 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -777,3 +777,57 @@ (define-public coq-mathcomp-bigenough
 purposes as @code{bigenough} will be subsumed by the near tactics.  The
 formalization is based on the Mathematical Components library.")
     (license license:cecill-b)))
+
+(define-public coq-ceres
+  (package
+    (name "coq-ceres")
+    (version "0.4.1")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/Lysxia/coq-ceres")
+                    (commit version)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "080nldsxmrxdan6gd0dvdgswn3gkwpy5hdqwra6wlmh8zzrs9z7n"))))
+    (build-system gnu-build-system)
+    (arguments
+     (list #:test-target "test"
+           #:make-flags #~(list "-f" "Makefile.coq"
+                                (string-append "COQLIBINSTALL=" #$output
+                                               "/lib/coq/user-contrib")
+                                "NO_TEST=1"
+                                "COQTOP=coqtop")
+           #:phases #~(modify-phases %standard-phases
+                        ;; Need to generate Makefile.coq
+                        (replace 'configure
+                          (lambda _
+                            (invoke "coq_makefile" "-f" "_CoqProject.classic"
+                                    "-o" "Makefile.coq")))
+                        (add-after 'build 'build-doc
+                          (lambda* (#:key make-flags #:allow-other-keys)
+                            (apply invoke "make" "html" make-flags)))
+                        (replace 'check
+                          (lambda* (#:key tests? test-target parallel-build?
+                                    make-flags #:allow-other-keys)
+                            (when tests?
+                              (apply invoke "make"
+                                     "-j" (number->string
+                                           (if parallel-build?
+                                               (parallel-job-count)
+                                               1))
+                                     test-target make-flags))))
+                        (add-after 'install 'install-doc
+                          (lambda _
+                            (let ((doc (string-append #$output
+                                                      "/share/doc/ceres")))
+                              (mkdir-p doc)
+                              (copy-recursively "html" doc)))))))
+    (propagated-inputs (list coq))
+    (home-page "https://gitlab.mpi-sws.org/iris/actris")
+    (synopsis "Coq library for serialization to S-expressions")
+    (description
+     "This package provides a Coq library that allows for serialization and
+deserialization of S-expression data.")
+    (license license:bsd-3)))

base-commit: 0e0d9bc91f20ac6dda439ab09330f0163eb9bf42
-- 
2.46.0

[bug#73237] [PATCH] gnu: Add coq-ceres.

[Jean-Pierre De Jesus Diaz]

Hello,

I've also recently packaged coq-ceres for Guix in my personal channel,
it is a shorter version:

<https://github.com/jeandudey/guix-formal-verification/blob/25e9444861229f8345b7baea0a2251f5fd2c7fa8/formal-verification/packages/coq.scm#L46-L73>

I'd also adapt the install-doc to use the install-doc target of the generated
Makefile like this:

(arguments
 (list #:test-target "test"
       #:make-flags
       #~(list (string-append "COQLIBINSTALL=" #$output
                              "/lib/coq/user-contrib")
               (string-append "COQDOCINSTALL=" #$output
                              "/share/doc/" #$name "-" #$version))
       #:phases
       #~(modify-phases %standard-phases
           (delete 'configure)
           (add-after 'install 'install-documentation
             (lambda* (#:key make-flags #:allow-other-keys)
               (apply invoke "make" "install-doc" make-flags))))))

The license of the channel is GPL-3.0-or-later so feel free to take
inspiration from it to contribute to Guix.

>+ (propagated-inputs (list coq))

Coq does not need to be propagated, only needs to be a native-input.

[bug#73237] [PATCH] gnu: Add coq-ceres.

[Antero Mejr via Guix-patches via]

Jean-Pierre De Jesus Diaz <jean@foundation.xyz> writes:

> I've also recently packaged coq-ceres for Guix in my personal channel,
> it is a shorter version:

There's a lot of useful stuff there, it would be great to get it
upstreamed. Unfortunately I do not have commit access.

> I'd also adapt the install-doc to use the install-doc target of the generated
> Makefile like this:

That sounds good, I will update the patch.

> Coq does not need to be propagated, only needs to be a native-input.

Yes. For some reason, the coq-mathcomp-bigenough package propagates coq,
and coq-stdpp has it in inputs, so I was unsure where to put it. I think
those packages should be updated to have coq as a native-input as well.

[bug#73237] [PATCH] gnu: Add coq-ceres.

[Jean-Pierre De Jesus Diaz]

>Yes. For some reason, the coq-mathcomp-bigenough package propagates coq,
>and coq-stdpp has it in inputs, so I was unsure where to put it. I think
>those packages should be updated to have coq as a native-input as well.

That's odd, it also propagates `which' when it shouldn't, only coq-mathcomp
should be propagated.

On Mon, Sep 16, 2024 at 3:14 PM Antero Mejr <mail@antr.me> wrote:
>
> Jean-Pierre De Jesus Diaz <jean@foundation.xyz> writes:
>
> > I've also recently packaged coq-ceres for Guix in my personal channel,
> > it is a shorter version:
>
> There's a lot of useful stuff there, it would be great to get it
> upstreamed. Unfortunately I do not have commit access.
>
> > I'd also adapt the install-doc to use the install-doc target of the generated
> > Makefile like this:
>
> That sounds good, I will update the patch.
>
> > Coq does not need to be propagated, only needs to be a native-input.
>
> Yes. For some reason, the coq-mathcomp-bigenough package propagates coq,
> and coq-stdpp has it in inputs, so I was unsure where to put it. I think
> those packages should be updated to have coq as a native-input as well.

[bug#73237] [PATCH] gnu: Add coq-ceres.

[Jean-Pierre De Jesus Diaz]

>That's odd, it also propagates `which' when it shouldn't, only coq-mathcomp
>should be propagated.

I've sent a few patches to fix this:

<https://issues.guix.gnu.org/73298>

On Mon, Sep 16, 2024 at 3:19 PM Jean-Pierre De Jesus Diaz
<jean@foundation.xyz> wrote:
>
> >Yes. For some reason, the coq-mathcomp-bigenough package propagates coq,
> >and coq-stdpp has it in inputs, so I was unsure where to put it. I think
> >those packages should be updated to have coq as a native-input as well.
>
> That's odd, it also propagates `which' when it shouldn't, only coq-mathcomp
> should be propagated.
>
> On Mon, Sep 16, 2024 at 3:14 PM Antero Mejr <mail@antr.me> wrote:
> >
> > Jean-Pierre De Jesus Diaz <jean@foundation.xyz> writes:
> >
> > > I've also recently packaged coq-ceres for Guix in my personal channel,
> > > it is a shorter version:
> >
> > There's a lot of useful stuff there, it would be great to get it
> > upstreamed. Unfortunately I do not have commit access.
> >
> > > I'd also adapt the install-doc to use the install-doc target of the generated
> > > Makefile like this:
> >
> > That sounds good, I will update the patch.
> >
> > > Coq does not need to be propagated, only needs to be a native-input.
> >
> > Yes. For some reason, the coq-mathcomp-bigenough package propagates coq,
> > and coq-stdpp has it in inputs, so I was unsure where to put it. I think
> > those packages should be updated to have coq as a native-input as well.