GNU bug report logs - #27195
Add search-paths for coq libraries

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 27195 in the body.
You can then email your comments to 27195 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: julien lepiller <julien <at> lepiller.eu>
To: guix-patches <at> gnu.org
Subject: Add search-paths for coq libraries
Date: Fri, 02 Jun 2017 10:11:23 +0200

[Message part 1 (text/plain, inline)]

Hi, here is a patch to set COQPATH, the environment variable used by coq 
to find external libraries.

[0001-gnu-coq-Add-search-paths-for-coq-libraries.patch (text/x-diff, attachment)]

Message #8 received at 27195 <at> debbugs.gnu.org (full text, mbox):

From: ludo <at> gnu.org (Ludovic Courtès)
To: julien lepiller <julien <at> lepiller.eu>
Cc: 27195 <at> debbugs.gnu.org
Subject: Re: bug#27195: Add search-paths for coq libraries
Date: Fri, 02 Jun 2017 17:55:04 +0200

julien lepiller <julien <at> lepiller.eu> skribis:

> From 7486a169bdfa0d4c5f287405b6d5fccf9dbcd1fa Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien <at> lepiller.eu>
> Date: Thu, 1 Jun 2017 17:52:12 +0200
> Subject: [PATCH] gnu: coq: Add search-paths for coq libraries.
>
> * gnu/packages/ocaml.scm (coq)[native-search-paths]: New field.
> ---
>  gnu/packages/ocaml.scm | 4 ++++
>  1 file changed, 4 insertions(+)
>
> diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
> index 863e367a5..a3475e2b9 100644
> --- a/gnu/packages/ocaml.scm
> +++ b/gnu/packages/ocaml.scm
> @@ -448,6 +448,10 @@ written in Objective Caml.")
>                (sha256
>                 (base32
>                  "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3"))))
> +    (native-search-paths
> +     (list (search-path-specification
> +            (variable "COQPATH")
> +            (files (list "lib/coq" "lib/coq/user-contrib")))))

Is “lib/coq/user-contrib” a widespread convention?  Looks unusual.

Apart from that LGTM, thanks!

Ludo’.

Message #13 received at 27195-done <at> debbugs.gnu.org (full text, mbox):

From: julien lepiller <julien <at> lepiller.eu>
To: 27195-done <at> debbugs.gnu.org
Subject: Re: bug#27195: Add search-paths for coq libraries
Date: Wed, 07 Jun 2017 10:02:59 +0200

Le 2017-06-02 17:55, ludo <at> gnu.org a écrit :
> julien lepiller <julien <at> lepiller.eu> skribis:
> 
>> From 7486a169bdfa0d4c5f287405b6d5fccf9dbcd1fa Mon Sep 17 00:00:00 2001
>> From: Julien Lepiller <julien <at> lepiller.eu>
>> Date: Thu, 1 Jun 2017 17:52:12 +0200
>> Subject: [PATCH] gnu: coq: Add search-paths for coq libraries.
>> 
>> * gnu/packages/ocaml.scm (coq)[native-search-paths]: New field.
>> ---
>>  gnu/packages/ocaml.scm | 4 ++++
>>  1 file changed, 4 insertions(+)
>> 
>> diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
>> index 863e367a5..a3475e2b9 100644
>> --- a/gnu/packages/ocaml.scm
>> +++ b/gnu/packages/ocaml.scm
>> @@ -448,6 +448,10 @@ written in Objective Caml.")
>>                (sha256
>>                 (base32
>>                  
>> "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3"))))
>> +    (native-search-paths
>> +     (list (search-path-specification
>> +            (variable "COQPATH")
>> +            (files (list "lib/coq" "lib/coq/user-contrib")))))
> 
> Is “lib/coq/user-contrib” a widespread convention?  Looks unusual.
> 
> Apart from that LGTM, thanks!
> 
> Ludo’.

This is what the coq_makefile tool produces by default. I removed the 
"lib/coq" because this directory is used only for the standard library 
and it is already found correctly. "lib/coq" also creates a conflict in 
the build environment, which I cannot reproduce outside, but it seems 
that "lib/coq/user-contrib" alone works fine: I could build a few coq 
libraries and I'll send patches this evening.

Pushed as 50cbbc9bd439c0db1cce6ba6d6a49de1d1f3bacd.

Previous Next

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