minor cleanup for math/coq

classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

minor cleanup for math/coq

Daniel Dickman
I have an update for coq from 8.4 to 8.6, but I'd like to get the easy
bits in first:
- switch from http to https
- drop gettext module
- regen WANTLIB
- move MODULES up in the Makefile, following Makefile.template

ok?

Index: Makefile
===================================================================
RCS file: /home/cvs/ports/math/coq/Makefile,v
retrieving revision 1.33
diff -u -p -u -r1.33 Makefile
--- Makefile 29 Mar 2016 11:27:01 -0000 1.33
+++ Makefile 24 Feb 2017 01:57:29 -0000
@@ -4,10 +4,10 @@ COMMENT= proof assistant based on a typ
 
 V= 8.4pl6
 DISTNAME= coq-$V
-REVISION= 1
+REVISION= 2
 
 CATEGORIES= math
-HOMEPAGE= http://coq.inria.fr/
+HOMEPAGE= https://coq.inria.fr/
 
 MAINTAINER= Yozo Toda <[hidden email]>
 
@@ -17,23 +17,21 @@ PERMIT_PACKAGE_CDROM= Yes
 WANTLIB += X11 Xcomposite Xcursor Xdamage Xext Xfixes Xi Xinerama
 WANTLIB += Xrandr Xrender atk-1.0 c cairo fontconfig freetype
 WANTLIB += gdk-x11-2.0 gdk_pixbuf-2.0 gio-2.0 glib-2.0 gobject-2.0
-WANTLIB += gtk-x11-2.0 m pango-1.0 pangocairo-1.0
-WANTLIB += pangoft2-1.0 pthread
-WANTLIB += z
+WANTLIB += gtk-x11-2.0 intl m pango-1.0 pangocairo-1.0 pangoft2-1.0
+WANTLIB += pthread z
 
-MASTER_SITES= http://coq.inria.fr/distrib/V${V}/files/
+MASTER_SITES= https://coq.inria.fr/distrib/V${V}/files/
 
-RUN_DEPENDS= x11/lablgtk2
-BUILD_DEPENDS= ${RUN_DEPENDS} \
+MODULES= lang/ocaml
+
+BUILD_DEPENDS= x11/lablgtk2 \
  lang/ocaml-camlp4 \
  sysutils/findlib
+RUN_DEPENDS= x11/lablgtk2
 
 DESTDIRNAME= COQINSTALLPREFIX
 
 USE_GMAKE= Yes
-
-MODULES= devel/gettext \
- lang/ocaml
 
 CONFIGURE_STYLE= simple
 CONFIGURE_ARGS= -emacslib ${PREFIX}/share/emacs/site-lisp \

Reply | Threaded
Open this post in threaded view
|

Re: minor cleanup for math/coq

Alexander Shadchin
On Thu, Feb 23, 2017 at 09:13:42PM -0500, Daniel Dickman wrote:
> I have an update for coq from 8.4 to 8.6, but I'd like to get the easy
> bits in first:
> - switch from http to https
> - drop gettext module
> - regen WANTLIB
> - move MODULES up in the Makefile, following Makefile.template
>
> ok?
>

ok shadchin@

--
Alexandr Shadchin

Reply | Threaded
Open this post in threaded view
|

Re: minor cleanup for math/coq

kwesterback
On Fri, 24 Feb 2017 at 10:15 Alexandr Shadchin <[hidden email]>
wrote:

> On Thu, Feb 23, 2017 at 09:13:42PM -0500, Daniel Dickman wrote:
> > I have an update for coq from 8.4 to 8.6, but I'd like to get the easy
> > bits in first:
> > - switch from http to https
> > - drop gettext module
> > - regen WANTLIB
> > - move MODULES up in the Makefile, following Makefile.template
> >
> > ok?
> >
>
> ok shadchin@
>
> --
> Alexandr Shadchin
>
>
Not being a coq user I don't have much useful to say on the details of this
change or the update to 8.6 per se.

But I keep thinking that the best strategy would be to leverage opam more,
and eliminate as many individual ports as possible. Of course the last time
I tried I think coq didn't install from opam. :-)

.... Ken
Reply | Threaded
Open this post in threaded view
|

Re: minor cleanup for math/coq

Daniel Dickman


> On Feb 24, 2017, at 10:39 AM, Kenneth Westerback <[hidden email]> wrote:
>
>
>
>> On Fri, 24 Feb 2017 at 10:15 Alexandr Shadchin <[hidden email]> wrote:
>> On Thu, Feb 23, 2017 at 09:13:42PM -0500, Daniel Dickman wrote:
>> > I have an update for coq from 8.4 to 8.6, but I'd like to get the easy
>> > bits in first:
>> > - switch from http to https
>> > - drop gettext module
>> > - regen WANTLIB
>> > - move MODULES up in the Makefile, following Makefile.template
>> >
>> > ok?
>> >
>>
>> ok shadchin@
>>
>> --
>> Alexandr Shadchin
>>
>
> Not being a coq user I don't have much useful to say on the details of this change or the update to 8.6 per se.
>
> But I keep thinking that the best strategy would be to leverage opam more, and eliminate as many individual ports as possible. Of course the last time I tried I think coq didn't install from opam. :-)

i'm not an opam expert but i think this makes more sense for ocaml modules than for applications that happen to be written in ocaml. i personally like the ports system where i can just pkg_add to get a pre-built binary for things like coq. but like i said, i'm not really expert enough to properly weigh in here so will leave that to others.


>
> .... Ken
Reply | Threaded
Open this post in threaded view
|

Re: minor cleanup for math/coq

Yozo TODA
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

thanks Daniel,
I found "minor cleanup" is already checked in.
I don't have enough resource now to try the update yet, but
please go ahead to 8.6 update.


> i'm not an opam expert but i think this makes more sense for ocaml modules
> than for applications that happen to be written in ocaml. i personally like
> the ports system where i can just pkg_add to get a pre-built binary for
> things like coq. but like i said, i'm not really expert enough to properly
>  weigh in here so will leave that to others.

I'm another opam beginner, but totally agree to this comment.

 -- yozo.

-----BEGIN PGP SIGNATURE-----

iQIyBAEBCAAcBQJYsmalFRx5b3pvQHYwMDcudmFpby5uZS5qcAAKCRB+B2lyJHdb
7G5wD/4ky9U2uxFalsJRqSBFmiBDF1mP4LG4yJeIBejVfdqVe7pDOf8lQJW/Ajyp
tSbhC0nW4qBeM8WIEWDAgkgbYUdTPxhpB0wR54dg4f8fSPaY+NQ9RsYwsH0MOPAz
C4jxry5D/Vxi3GAJRWIIWgpQG/iM01moGe9yGCnWkT0JHemT4iH3UMi5bbZBGJBk
+Wq/v01ulMa3NqIRjRfbmrGdaBlmaQmBHnZi5JM1gp9rnRoAbIZuzst0yxHzgo+C
ADt0tTNzjqO9mZEDqXUQUHUSWgn2kxSgbkdjiasF562U8HJb5ab5xXmCYyqtrFFK
zNUgHGW8IocBJy+ddNOcMvA3+ji/SWF4R33XqFzlyWssJg3nh0jUP5Z+KurZKjTO
Z3SlxPT7ycm8rk1v7/iKmtmAGvHoU6rk+rd/h2rFgmc89IvfQ27WZ1hPHAelKNja
Zgo696wRZvhpCrgL3SP/aAT4w6H6btthzThWCkPsMpBNDOc9INKAdeobwgOFbY7v
tiNiDe6geG/z0SHHZu1MfqNOWtPQ70kqD0T3oyMmc/7tA7u5qvNKEkI7eBZKpWqt
RexELw1RjIqwha3BK0U2TZx2UzKaaCL9QMlUZ7w0s+t8n3Zl4QV7pxhvzyTft1E5
MU16PSNtKqV1l0Q+9n7Mw+jPnrs2GijbRnKWQQdx6jw/eSyw/g==
=TWx8
-----END PGP SIGNATURE-----