> On Jun 1, 2020, at 4:01 PM, Christopher Zimmermann <chr...@openbsd.org> wrote:
>
> On Mon, Jun 01, 2020 at 09:35:26PM +0200, Antoine Jacoutot wrote:
>>> On Mon, Jun 01, 2020 at 12:04:50AM -0600, Christopher Zimmermann wrote:
>>> CVSROOT: /cvs
>>> Module name: ports
>>> Changes by: chr...@cvs.openbsd.org 2020/06/01 00:04:50
>>>
>>> Modified files:
>>> math/coq : Makefile distinfo
>>> math/coq/pkg : PFRAG.dynlink-native PFRAG.native
>>> PFRAG.no-native PLIST
>>>
>>> Log message:
>>> Upgrade math/coq to 8.11.1
>>>
>>> ok daniel@
>>
>> This seems to have broken lang/compcert:
>>
>> ===> lang/compcert
>> ===> Generating configure for compcert-3.7
>> ===> Configuring for compcert-3.7
>> Testing assembler support for CFI directives... yes
>> Testing linker support for '-no-pie' / '-nopie' option... yes, '-no-pie'
>> Testing Coq... version 8.11.1 -- UNSUPPORTED
>> Error: CompCert requires one of the following Coq versions: 8.11.0, 8.10.2,
>> 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0
>> Testing OCaml... version 4.09.0 -- good!
>
> This was expected. I just forgot about compcert when I committed math/coq.
> This was my fault. daniel@ ? OK to commit below patch as already done
> upstream?
>
> Christopher
>
>
> Here's the fix:
>
I fixed it a slightly different way. Let me know if any problems post the fix.
