| Message ID | 87zfob1dfj.fsf@antr.me |
|---|---|
| State | New |
| Headers | show |
| Series | [bug#73237] gnu: Add coq-ceres. | expand |
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.
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.
>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.
>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.
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)))