> On May 25, 2020, at 5:11 AM, Christopher Zimmermann <chrisz@openbsd.org> wrote:
>
> testing needed
> Reply-To:
> In-Reply-To: <20A364D1-D8BC-441F-9814-EBE7DFC0297B@gmail.com>
>
>> 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@ ?
>
No comments:
Post a Comment