[PATCH] gnu: Add coq-ceres.

  • Open
  • quality assurance status badge
Details
2 participants
  • Jean-Pierre De Jesus Diaz
  • Antero Mejr
Owner
unassigned
Submitted by
Antero Mejr
Severity
normal
A
A
Antero Mejr wrote on 13 Sep 2024 22:55
(address . guix-patches@gnu.org)
87zfob1dfj.fsf@antr.me
* gnu/packages/coq.scm (coq-ceres): New variable.

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

Toggle diff (66 lines)
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
J
J
Jean-Pierre De Jesus Diaz wrote on 16 Sep 2024 16:54
(address . 73237@debbugs.gnu.org)(address . mail@antr.me)
CAG1gdUpqdcc7Q1jMoHnCYEcZVw=V9WWB3RFZ2bJFgd3tPUcx=w@mail.gmail.com
Hello,

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


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.

Toggle quote (2 lines)
>+ (propagated-inputs (list coq))

Coq does not need to be propagated, only needs to be a native-input.
A
A
Antero Mejr wrote on 16 Sep 2024 17:14
(name . Jean-Pierre De Jesus Diaz)(address . jean@foundation.xyz)(address . 73237@debbugs.gnu.org)
87o74nr5p6.fsf@antr.me
Jean-Pierre De Jesus Diaz <jean@foundation.xyz> writes:

Toggle quote (3 lines)
> 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.

Toggle quote (3 lines)
> 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.

Toggle quote (2 lines)
> 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.
J
J
Jean-Pierre De Jesus Diaz wrote on 16 Sep 2024 17:19
(name . Antero Mejr)(address . mail@antr.me)(address . 73237@debbugs.gnu.org)
CAG1gdUqp6u=2kuVBhCFsdFSODYR7+XjVdWatq8AUXgVNC3MnnA@mail.gmail.com
Toggle quote (4 lines)
>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:
Toggle quote (19 lines)
>
> 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.
J
J
Jean-Pierre De Jesus Diaz wrote on 16 Sep 2024 17:30
(name . Antero Mejr)(address . mail@antr.me)(address . 73237@debbugs.gnu.org)
CAG1gdUrRDfpsDgqSEtkAU1+sYkdEJUHaSeLiZZDA-UmT=ikZRA@mail.gmail.com
Toggle quote (3 lines)
>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:


On Mon, Sep 16, 2024 at 3:19?PM Jean-Pierre De Jesus Diaz
<jean@foundation.xyz> wrote:
Toggle quote (28 lines)
>
> >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.
?
Your comment

Commenting via the web interface is currently disabled.

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

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