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 ?
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 <chrisz@openbsd.org> 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
No comments:
Post a Comment