Packaging Coq

Packaging Coq

[Nikita Karetnikov]

[-- Attachment #1.1: Type: text/plain, Size: 34 bytes --]

Does anyone know how to proceed?


[-- Attachment #1.2: coq.scm --]
[-- Type: text/plain, Size: 3563 bytes --]

;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2014 Nikita Karetnikov <nikita@karetnikov.org>
;;;
;;; This file is part of GNU Guix.
;;;
;;; GNU Guix is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or (at
;;; your option) any later version.
;;;
;;; GNU Guix is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;;; GNU General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.

(define-module (gnu packages coq)
  #:use-module (guix licenses)
  #:use-module (guix packages)
  #:use-module (guix download)
  #:use-module (guix build-system gnu)
  #:use-module (gnu packages compression)
  #:use-module (gnu packages ocaml))

(define-public coq
  (package
    (name "coq")
    (version "8.4pl5")
    (source
     (origin
      (method url-fetch)
      (uri (string-append "https://" name ".inria.fr/distrib/V" version
                          "/files/" name "-" version ".tar.gz"))
      (sha256
       (base32
        "0iajsabyrgypk1ncm0kqcxqv02k24xa1bayaxacjgmsqiavmm09m"))))
    (build-system gnu-build-system)
    (arguments
     '(#:phases
        (alist-replace 'configure
                      (lambda* (#:key outputs #:allow-other-keys)
                        ;; This 'configure' script doesn't support
                        ;; variables passed as arguments.
                        (let ((out (assoc-ref outputs "out")))
                          (setenv "CONFIG_SHELL" (which "bash"))
                          (zero?
                           ;; 'configure' does not recognize the flags if you
                           ;; use 'system*'.
                           (system (string-append "./configure"
                                                  " -prefix " out
                                                  " -camldir "
                                                  (dirname (which "ocaml")))))))
                      (alist-replace 'build
                                     (lambda _
                                       (system* "make" "world"))
                                     (alist-replace 'check
                                                    (lambda _
                                                      (chdir "test-suite")
                                                      (system* "make" "check")
                                                      (chdir ".."))
                                                    %standard-phases)))))
    (native-inputs
     `(("ocaml" ,ocaml)
       ("bzip2" ,bzip2)))
    (home-page "https://coq.inria.fr")
    (synopsis "Formal proof management system")
    (description
     "Coq is a formal proof management system.  It provides a formal language
to write mathematical definitions, executable algorithms and theorems together
with an environment for semi-interactive development of machine-checked
proofs.  Typical applications include the certification of properties of
programming languages, the formalization of mathematics (e.g., the full
formalization of the Feit-Thompson theorem or homotopy type theory) and
teaching.")
    (license lgpl2.1)))

[-- Attachment #2: Type: application/pgp-signature, Size: 835 bytes --]

Re: Packaging Coq

[Nikita Karetnikov]

[-- Attachment #1: Type: text/plain, Size: 123 bytes --]

Since people are commenting only on the recipe, I guess I need to
clarify that I’d like to know why it fails to build.

[-- Attachment #2: Type: application/pgp-signature, Size: 835 bytes --]

Re: Packaging Coq

[Nikita Karetnikov]

[-- Attachment #1: Type: text/plain, Size: 129 bytes --]

I haven’t done the obvious thing…  The package in Nixpkgs does more
things, so I’ll try to change my recipe accordingly.

[-- Attachment #2: Type: application/pgp-signature, Size: 835 bytes --]

Re: Packaging Coq

[Andreas Enge]

On Thu, Dec 04, 2014 at 05:02:27AM +0400, Nikita Karetnikov wrote:
>                            ;; 'configure' does not recognize the flags if you
>                            ;; use 'system*'.
>                            (system (string-append "./configure"
>                                                   " -prefix " out
>                                                   " -camldir "
>                                                   (dirname (which "ocaml")))))))

This is very strange, how is it at all possible that system* does not work?

>                       (alist-replace 'build
>                                      (lambda _
>                                        (system* "make" "world"))

Instead of this, you could use
  #:make-flags '("world")

Andreas

Re: Packaging Coq

[Ludovic Courtès]

Andreas Enge <andreas@enge.fr> skribis:

> On Thu, Dec 04, 2014 at 05:02:27AM +0400, Nikita Karetnikov wrote:
>>                            ;; 'configure' does not recognize the flags if you
>>                            ;; use 'system*'.
>>                            (system (string-append "./configure"
>>                                                   " -prefix " out
>>                                                   " -camldir "
>>                                                   (dirname (which "ocaml")))))))
>
> This is very strange, how is it at all possible that system* does not work?

I’m guess that the problem instead was that the default ‘configure’
phase passes arguments not recognized by this hand-written ‘configure’
script.

However, please use ‘system*’ instead of ‘system’.

Thanks,
Ludo’.

Re: Packaging Coq

[Mark H Weaver]

Andreas Enge <andreas@enge.fr> writes:

> On Thu, Dec 04, 2014 at 05:02:27AM +0400, Nikita Karetnikov wrote:
>>                       (alist-replace 'build
>>                                      (lambda _
>>                                        (system* "make" "world"))
>
> Instead of this, you could use
>   #:make-flags '("world")

IMO, this is a misuse of #:make-flags.  'world' is not a make flag, it
is a make *target*.  The make flags are also passed to 'make' during the
default 'check' and 'install' phases.

      Mark

Re: Packaging Coq

[Andreas Enge]

On Thu, Dec 04, 2014 at 06:56:25PM -0500, Mark H Weaver wrote:
> Andreas Enge <andreas@enge.fr> writes:
> > Instead of this, you could use
> >   #:make-flags '("world")
> IMO, this is a misuse of #:make-flags.  'world' is not a make flag, it
> is a make *target*.  The make flags are also passed to 'make' during the
> default 'check' and 'install' phases.

In that case, maybe we should add a variable 'build-target' to our build
system.

Andreas

Re: Packaging Coq

[Mark H Weaver]

Andreas Enge <andreas@enge.fr> writes:

> On Thu, Dec 04, 2014 at 06:56:25PM -0500, Mark H Weaver wrote:
>> Andreas Enge <andreas@enge.fr> writes:
>> > Instead of this, you could use
>> >   #:make-flags '("world")
>> IMO, this is a misuse of #:make-flags.  'world' is not a make flag, it
>> is a make *target*.  The make flags are also passed to 'make' during the
>> default 'check' and 'install' phases.
>
> In that case, maybe we should add a variable 'build-target' to our build
> system.

Sounds reasonable to me, although it should be 'build-targets' since
there is often more than one.  Ditto for 'install-targets' and
'check-targets' (or 'test-targets') if we don't already have them.

On the other hand, I'm not sure that these are needed often enough to
justify these new variables.  What do others think?

     Mark

Re: Packaging Coq

[Andreas Enge]

On Fri, Dec 05, 2014 at 09:59:56AM -0500, Mark H Weaver wrote:
> Sounds reasonable to me, although it should be 'build-targets' since
> there is often more than one.  Ditto for 'install-targets' and
> 'check-targets' (or 'test-targets') if we don't already have them.

We already have test-target, which often becomes "test" instead of "check".

Andreas

Re: Packaging Coq

[Ludovic Courtès]

Mark H Weaver <mhw@netris.org> skribis:

> Sounds reasonable to me, although it should be 'build-targets' since
> there is often more than one.  Ditto for 'install-targets' and
> 'check-targets' (or 'test-targets') if we don't already have them.

I think it’s quite infrequent, so I would not bother.

BTW, using #:make-flags to specify a target may not work well because
the ‘install’ phase also honors #:make-flags.

Thanks,
Ludo’.

Re: Packaging Coq

[John Darrington]

[-- Attachment #1: Type: text/plain, Size: 566 bytes --]

On Thu, Dec 04, 2014 at 05:02:27AM +0400, Nikita Karetnikov wrote:
                                (system (string-append "./configure"
                                                       " -prefix " out
                                                       " -camldir "
 --------------------------------------------------------^
Should these arguments not be a double -- ??


-- 
PGP Public key ID: 1024D/2DE827B3 
fingerprint = 8797 A26D 0854 2EAB 0285  A290 8A67 719C 2DE8 27B3
See http://sks-keyservers.net or any PGP keyserver for public key.


[-- Attachment #2: Digital signature --]
[-- Type: application/pgp-signature, Size: 198 bytes --]

Re: Packaging Coq

[Nikita Karetnikov]

[-- Attachment #1: Type: text/plain, Size: 52 bytes --]

> Should these arguments not be a double -- ??

No.

[-- Attachment #2: Type: application/pgp-signature, Size: 835 bytes --]

Re: Packaging Coq

[Mark H Weaver]

Nikita Karetnikov <nikita@karetnikov.org> writes:
> Does anyone know how to proceed?

It would help if you told us something about the problem you ran into,
preferably with relevant excerpts of the failed build output.

I'm also interested in Coq, and attempted to package it about 6 weeks
ago.  I started by trying to update to ocaml 4.02.x, but there were many
test suite failures that looked non-trivial to debug.  I stalled there.

If I were to proceed without the ocaml update, I would start by
packaging "camlp5", which is listed as a build dependency in the Coq
build documentation (INSTALL in the top-level source directory).

It looks like we don't yet have camlp5, and that you didn't attempt to
package it.  Maybe that's the problem?

     Regards,
       Mark