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

Previous Next

Full log

View this message in rfc822 format

From: Jean-Pierre De Jesus Diaz <jean <at> foundation.xyz>
To: 73237 <at> debbugs.gnu.org
Cc: mail <at> antr.me
Subject: [bug#73237] [PATCH] gnu: Add coq-ceres.
Date: Mon, 16 Sep 2024 14:54:07 +0000

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.

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.