Re: update math/coq 8.11.1 supporting OCaml 4.10 - sparc64 testing needed

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

Re: update math/coq 8.11.1 supporting OCaml 4.10 - sparc64 testing needed

Christopher Zimmermann-2
testing needed
Reply-To:
In-Reply-To: <[hidden email]>

On Sun, May 24, 2020 at 05:23:25PM -0400, Daniel Dickman wrote:
>Jeremie reported a problem on sparc64. Is it addressed in the diff below?
>
>https://marc.info/?t=158196793400003&r=1&w=2

No. I forgot about this. Chances are it got fixed with Coq 8.11.1, but I
don't have access to sparc64 hardware. Who could test on sparc64 ?

Attached is a diff updating Coq 8.11.1 and OCaml to 4.10.0, including
all necessary revision bumps and a fix for compcert.

Could someone try building math/coq with this diff applied? Maybe jca@ ?


Christopher

>> On May 24, 2020, at 2:19 PM, Christopher Zimmermann <[hidden email]> wrote:
>>
>> 
>> Hi,
>>
>> this is the only port not yet compatible with OCaml 4.10. OK to upgrade? Compcert was only tested by building simple hello world program.
>>
>> Christopher
>>
>> <compcert.diff>
>> <coq.diff>
--
http://gmerlin.de
OpenPGP: http://gmerlin.de/christopher.pub
CB07 DA40 B0B6 571D 35E2  0DEF 87E2 92A7 13E5 DEE1

ocaml410.diff.gz (33K) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: update math/coq 8.11.1 supporting OCaml 4.10 - sparc64 testing needed

Daniel Dickman


> On May 25, 2020, at 5:11 AM, Christopher Zimmermann <[hidden email]> wrote:
>
> testing needed
> Reply-To:
> In-Reply-To: <[hidden email]>
>
>> On Sun, May 24, 2020 at 05:23:25PM -0400, Daniel Dickman wrote:
>> Jeremie reported a problem on sparc64. Is it addressed in the diff below?
>>
>> https://marc.info/?t=158196793400003&r=1&w=2
>
> No. I forgot about this. Chances are it got fixed with Coq 8.11.1, but I don't have access to sparc64 hardware. Who could test on sparc64 ?

I have a sparc64 box but it’s slow. I’ll get it started but someone with a faster box will definitely beat me to it.

>
> Attached is a diff updating Coq 8.11.1 and OCaml to 4.10.0, including all necessary revision bumps and a fix for compcert

I’ll commit an update for compcert shortly. That part is straightforward and we don’t have to wait for coq tests to complete.

>
> Could someone try building math/coq with this diff applied? Maybe jca@ ?
>

Reply | Threaded
Open this post in threaded view
|

Re: update math/coq 8.11.1 supporting OCaml 4.10 - sparc64 testing needed

Jeremie Courreges-Anglas-5
On Mon, May 25 2020, Daniel Dickman <[hidden email]> wrote:

>> On May 25, 2020, at 5:11 AM, Christopher Zimmermann <[hidden email]> wrote:
>>
>> testing needed
>> Reply-To:
>> In-Reply-To: <[hidden email]>
>>
>>> On Sun, May 24, 2020 at 05:23:25PM -0400, Daniel Dickman wrote:
>>> Jeremie reported a problem on sparc64. Is it addressed in the diff below?
>>>
>>> https://marc.info/?t=158196793400003&r=1&w=2
>>
>> No. I forgot about this. Chances are it got fixed with Coq 8.11.1, but I don't have access to sparc64 hardware. Who could test on sparc64 ?
>
> I have a sparc64 box but it’s slow. I’ll get it started but someone with a faster box will definitely beat me to it.

Everything looks fine on sparc64, except the lang/compcert change:
ONLY_FOR_ARCHS should be set before ".include <bsd.arch.port.mk>", else it
is ignored.  Actually, ".include <bsd.arch.port.mk>" isn't needed,
bsd.port.mk already includes that file, so please drop this line.

Christopher: there's a new camlp4 release upstream with support for
ocaml-4.10.  Diff below tested on sparc64, if you want to pick it up.
Maybe you should drop MAINTAINER for this port?

ok jca@ for this ocaml update, with the compcert issue addressed, you
folks know better regarding the new coq release.


Index: Makefile
===================================================================
RCS file: /cvs/ports/lang/ocaml-camlp4/Makefile,v
retrieving revision 1.12
diff -u -p -r1.12 Makefile
--- Makefile 26 Sep 2019 09:46:11 -0000 1.12
+++ Makefile 27 May 2020 00:11:13 -0000
@@ -3,8 +3,7 @@
 COMMENT = OCaml Preprocessor and Pretty-Printer
 CATEGORIES = lang
 
-V = 4.08+1
-REVISION = 0
+V = 4.10+1
 GH_ACCOUNT = ocaml
 GH_PROJECT = camlp4
 GH_TAGNAME = ${V}
Index: distinfo
===================================================================
RCS file: /cvs/ports/lang/ocaml-camlp4/distinfo,v
retrieving revision 1.6
diff -u -p -r1.6 distinfo
--- distinfo 18 Sep 2019 19:42:58 -0000 1.6
+++ distinfo 25 May 2020 23:37:14 -0000
@@ -1,2 +1,2 @@
-SHA256 (camlp4-4.08+1.tar.gz) = ZVzTvcr7+ENYd/YPS0fdLraf7vWv2IgSke8BuhK9nYg=
-SIZE (camlp4-4.08+1.tar.gz) = 649830
+SHA256 (camlp4-4.10+1.tar.gz) = nZsYgQ6DTuEeYnNqaAMTz5DBVR4iwITKK3DGgzju8p4=
+SIZE (camlp4-4.10+1.tar.gz) = 650092
Index: patches/patch-configure
===================================================================
RCS file: patches/patch-configure
diff -N patches/patch-configure
--- patches/patch-configure 26 Sep 2019 11:04:50 -0000 1.3
+++ /dev/null 1 Jan 1970 00:00:00 -0000
@@ -1,15 +0,0 @@
-$OpenBSD: patch-configure,v 1.3 2019/09/26 11:04:50 chrisz Exp $
-camlp4 4.08 seems to work with OCaml 4.09 just fine.
-
-Index: configure
---- configure.orig
-+++ configure
-@@ -39,7 +39,7 @@ if [ $major -lt 4 -o \( $major -eq 4 -a $minor -lt 2 \
-     echo "The standalone Camlp4 requires OCaml >= 4.02."
-     echo "For previous versions of OCaml use the Camlp4 distributed with OCaml."
-     exit 2
--elif [ $major -ne 4 -o $minor -ne 8 ]; then
-+elif [ $major -ne 4 -o $minor -ne 9 -a $minor -ne 8 ]; then
-     echo "This version of Camlp4 is for OCaml 4.07 but you are using OCaml $ocaml_version."
-     if [ -d .git ] ; then
-       if [ $PINNED -eq 1 ] ; then


--
jca | PGP : 0x1524E7EE / 5135 92C1 AD36 5293 2BDF  DDCC 0DFA 74AE 1524 E7EE

Reply | Threaded
Open this post in threaded view
|

Re: update math/coq 8.11.1 supporting OCaml 4.10 - sparc64 testing needed

Christopher Zimmermann-2


On May 27, 2020 2:20:54 AM GMT+02:00, Jeremie Courreges-Anglas <[hidden email]> wrote:

>On Mon, May 25 2020, Daniel Dickman <[hidden email]> wrote:
>>> On May 25, 2020, at 5:11 AM, Christopher Zimmermann
><[hidden email]> wrote:
>>>
>>> testing needed
>>> Reply-To:
>>> In-Reply-To: <[hidden email]>
>>>
>>>> On Sun, May 24, 2020 at 05:23:25PM -0400, Daniel Dickman wrote:
>>>> Jeremie reported a problem on sparc64. Is it addressed in the diff
>below?
>>>>
>>>> https://marc.info/?t=158196793400003&r=1&w=2
>>>
>>> No. I forgot about this. Chances are it got fixed with Coq 8.11.1,
>but I don't have access to sparc64 hardware. Who could test on sparc64
>?
>>
>> I have a sparc64 box but it’s slow. I’ll get it started but someone
>with a faster box will definitely beat me to it.
>
>Everything looks fine on sparc64,

That's great. Thanks!

>except the lang/compcert change:
>ONLY_FOR_ARCHS should be set before ".include <bsd.arch.port.mk>", else
>it
>is ignored.  Actually, ".include <bsd.arch.port.mk>" isn't needed,
>bsd.port.mk already includes that file, so please drop this line.
>
>Christopher: there's a new camlp4 release upstream with support for
>ocaml-4.10.  Diff below tested on sparc64, if you want to pick it up.
>Maybe you should drop MAINTAINER for this port?

I would rather drop the port. We moved everything to camlp5 afaict. But if anyone wants to take maintainership, that's fine with me. I'm also ok with your diff. Plist didn't change I would suspect.

>ok jca@ for this ocaml update, with the compcert issue addressed, you
>folks know better regarding the new coq release.
>
>Index: Makefile
>===================================================================
>RCS file: /cvs/ports/lang/ocaml-camlp4/Makefile,v
>retrieving revision 1.12
>diff -u -p -r1.12 Makefile
>--- Makefile 26 Sep 2019 09:46:11 -0000 1.12
>+++ Makefile 27 May 2020 00:11:13 -0000
>@@ -3,8 +3,7 @@
> COMMENT = OCaml Preprocessor and Pretty-Printer
> CATEGORIES = lang
>
>-V = 4.08+1
>-REVISION = 0
>+V = 4.10+1
> GH_ACCOUNT = ocaml
> GH_PROJECT = camlp4
> GH_TAGNAME = ${V}
>Index: distinfo
>===================================================================
>RCS file: /cvs/ports/lang/ocaml-camlp4/distinfo,v
>retrieving revision 1.6
>diff -u -p -r1.6 distinfo
>--- distinfo 18 Sep 2019 19:42:58 -0000 1.6
>+++ distinfo 25 May 2020 23:37:14 -0000
>@@ -1,2 +1,2 @@
>-SHA256 (camlp4-4.08+1.tar.gz) =
>ZVzTvcr7+ENYd/YPS0fdLraf7vWv2IgSke8BuhK9nYg=
>-SIZE (camlp4-4.08+1.tar.gz) = 649830
>+SHA256 (camlp4-4.10+1.tar.gz) =
>nZsYgQ6DTuEeYnNqaAMTz5DBVR4iwITKK3DGgzju8p4=
>+SIZE (camlp4-4.10+1.tar.gz) = 650092
>Index: patches/patch-configure
>===================================================================
>RCS file: patches/patch-configure
>diff -N patches/patch-configure
>--- patches/patch-configure 26 Sep 2019 11:04:50 -0000 1.3
>+++ /dev/null 1 Jan 1970 00:00:00 -0000
>@@ -1,15 +0,0 @@
>-$OpenBSD: patch-configure,v 1.3 2019/09/26 11:04:50 chrisz Exp $
>-camlp4 4.08 seems to work with OCaml 4.09 just fine.
>-
>-Index: configure
>---- configure.orig
>-+++ configure
>-@@ -39,7 +39,7 @@ if [ $major -lt 4 -o \( $major -eq 4 -a $minor -lt 2
>\
>-     echo "The standalone Camlp4 requires OCaml >= 4.02."
>-     echo "For previous versions of OCaml use the Camlp4 distributed
>with OCaml."
>-     exit 2
>--elif [ $major -ne 4 -o $minor -ne 8 ]; then
>-+elif [ $major -ne 4 -o $minor -ne 9 -a $minor -ne 8 ]; then
>-     echo "This version of Camlp4 is for OCaml 4.07 but you are using
>OCaml $ocaml_version."
>-     if [ -d .git ] ; then
>-       if [ $PINNED -eq 1 ] ; then

Reply | Threaded
Open this post in threaded view
|

Re: update math/coq 8.11.1 supporting OCaml 4.10 - sparc64 testing needed

Daniel Dickman
On Tue, May 26, 2020 at 10:57 PM Christopher Zimmermann
<[hidden email]> wrote:

>
>
>
> On May 27, 2020 2:20:54 AM GMT+02:00, Jeremie Courreges-Anglas <[hidden email]> wrote:
> >On Mon, May 25 2020, Daniel Dickman <[hidden email]> wrote:
> >>> On May 25, 2020, at 5:11 AM, Christopher Zimmermann
> ><[hidden email]> wrote:
> >>>
> >>> testing needed
> >>> Reply-To:
> >>> In-Reply-To: <[hidden email]>
> >>>
> >>>> On Sun, May 24, 2020 at 05:23:25PM -0400, Daniel Dickman wrote:
> >>>> Jeremie reported a problem on sparc64. Is it addressed in the diff
> >below?
> >>>>
> >>>> https://marc.info/?t=158196793400003&r=1&w=2
> >>>
> >>> No. I forgot about this. Chances are it got fixed with Coq 8.11.1,
> >but I don't have access to sparc64 hardware. Who could test on sparc64
> >?
> >>
> >> I have a sparc64 box but it’s slow. I’ll get it started but someone
> >with a faster box will definitely beat me to it.
> >
> >Everything looks fine on sparc64,
>
> That's great. Thanks!
>

From your big ocaml diff, OK daniel@ to update:
- coq
- ocaml-camlp4

(since Jeremie retested on sparc64)

I did notice PLIST changes for ocaml-ocamlbuild. Is it expected? Why
does it change for a newer version of ocaml?

As for Compcert, I will update it shortly (taking a bit of time for me
as I recently rebuilt my box to pickup the recent FFS2 changes)

I don't think the patch you suggested for compcert is a good idea though:

    -ONLY_FOR_ARCHS = amd64 i386
    +ONLY_FOR_ARCHS = ${OCAML_NATIVE_ARCHS}

For this port, ONLY_FOR_ARCHS is supposed to be tied to the list of
compcert back-ends. It is independant from the OCAML native archs, no?
Was there a reason you wanted to make this change?

Once all this has gone in, let's do the ocaml update and revision
bumps separately.

p.s. I was looking at updating ocaml-menhir recently (which compcert
needs), but it seems like we need to move to a newer dune to update
ocaml-menhir any further. But dune cannot be updated without first
fixing some of the ports that use dune to support newer dune versions.
Do you have any diffs for this already?

Reply | Threaded
Open this post in threaded view
|

Re: update math/coq 8.11.1 supporting OCaml 4.10 - sparc64 testing needed

Jeremie Courreges-Anglas-5
In reply to this post by Christopher Zimmermann-2
On Wed, May 27 2020, Christopher Zimmermann <[hidden email]> wrote:

> On May 27, 2020 2:20:54 AM GMT+02:00, Jeremie Courreges-Anglas <[hidden email]> wrote:
>>On Mon, May 25 2020, Daniel Dickman <[hidden email]> wrote:
>>>> On May 25, 2020, at 5:11 AM, Christopher Zimmermann
>><[hidden email]> wrote:
>>>>
>>>> testing needed
>>>> Reply-To:
>>>> In-Reply-To: <[hidden email]>
>>>>
>>>>> On Sun, May 24, 2020 at 05:23:25PM -0400, Daniel Dickman wrote:
>>>>> Jeremie reported a problem on sparc64. Is it addressed in the diff
>>below?
>>>>>
>>>>> https://marc.info/?t=158196793400003&r=1&w=2
>>>>
>>>> No. I forgot about this. Chances are it got fixed with Coq 8.11.1,
>>but I don't have access to sparc64 hardware. Who could test on sparc64
>>?
>>>
>>> I have a sparc64 box but it’s slow. I’ll get it started but someone
>>with a faster box will definitely beat me to it.
>>
>>Everything looks fine on sparc64,
>
> That's great. Thanks!
>
>>except the lang/compcert change:
>>ONLY_FOR_ARCHS should be set before ".include <bsd.arch.port.mk>", else
>>it
>>is ignored.  Actually, ".include <bsd.arch.port.mk>" isn't needed,
>>bsd.port.mk already includes that file, so please drop this line.
>>
>>Christopher: there's a new camlp4 release upstream with support for
>>ocaml-4.10.  Diff below tested on sparc64, if you want to pick it up.
>>Maybe you should drop MAINTAINER for this port?
>
> I would rather drop the port. We moved everything to camlp5 afaict.

The last time ocamlp4 was discussed it was pointed out that net/mldonkey
still uses it.  Upstream mldonkey handled the 4.09 and 4.10 releases:

  https://github.com/camlp4/camlp4/releases

> But if anyone wants to take maintainership, that's fine with me. I'm also ok with your diff. Plist didn't change I would suspect.
>
>>ok jca@ for this ocaml update,

I should have mentioned that since camlp4 releases are tightly coupled
with OCaml releases, I have reverted the update to camlp4-4.10.

(Error message was: This version of Camlp4 is for OCaml 4.10 but you are
using OCaml 4.09.0.)

--
jca | PGP : 0x1524E7EE / 5135 92C1 AD36 5293 2BDF  DDCC 0DFA 74AE 1524 E7EE