[debbugs-tracker] bug#27195: closed (Add search-paths for coq libraries)

[GNU bug Tracking System]

Your message dated Wed, 07 Jun 2017 10:02:59 +0200
with message-id <address@hidden>
and subject line Re: bug#27195: Add search-paths for coq libraries
has caused the debbugs.gnu.org bug report #27195,
regarding Add search-paths for coq libraries
to be marked as done.

(If you believe you have received this mail in error, please contact
address@hidden)


-- 
27195: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=27195
GNU Bug Tracking System
Contact address@hidden with problems

--- Begin Message --- Subject: Add search-paths for coq libraries Date: Fri, 02 Jun 2017 10:11:23 +0200 User-agent: Roundcube Webmail/1.2.5 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
Description: Text Data

--- End Message ---

> --- Begin Message ---
>
>
>
> Subject: 
>
> Re: bug#27195: Add search-paths for coq libraries
>
>
>
>
> Date: 
>
> Wed, 07 Jun 2017 10:02:59 +0200
>
>
>
>
> User-agent: 
>
> Roundcube Webmail/1.2.5
>
>
>
>
> Le 2017-06-02 17:55, address@hidden a écrit :
> > julien lepiller <address@hidden> skribis:
> >
> > > From 7486a169bdfa0d4c5f287405b6d5fccf9dbcd1fa Mon Sep 17 00:00:00 2001
> > > From: Julien Lepiller <address@hidden>
> > > 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.
>
>
> --- End Message ---