Ok aja
—
Antoine
> On 1 Jun 2020, at 22:01, 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:
>
>
> Index: patches/patch-configure
> ===================================================================
> RCS file: /cvs/ports/lang/compcert/patches/patch-configure,v
> retrieving revision 1.11
> diff -u -p -r1.11 patch-configure
> --- patches/patch-configure 16 Feb 2020 04:34:23 -0000 1.11
> +++ patches/patch-configure 1 Jun 2020 19:54:04 -0000
> @@ -2,6 +2,7 @@ $OpenBSD: patch-configure,v 1.11 2020/02
>
> 1) Fixup path locations for OpenBSD
> 2) Add configuration support for macppc and aarch64 on OpenBSD
> +3) Add Coq 8.11.1 to supported coq versions
>
> Index: configure
> --- configure.orig
> @@ -73,6 +74,15 @@ Index: configure
> *)
> echo "Error: invalid eabi/system '$target' for architecture
> AArch64." 1>&2
> echo "$usage" 1>&2
> +@@ -530,7 +550,7 @@ missingtools=false
> + echo "Testing Coq... " | tr -d '\n'
> + coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof
> Assistant, version \([^ ]*\).*$/\1/p')
> + case "$coq_ver" in
> +- 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0)
> ++ 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1)
> + echo "version $coq_ver -- good!";;
> + ?*)
> + echo "version $coq_ver -- UNSUPPORTED"
> @@ -666,14 +686,14 @@ esac
> #
> # Generate Makefile.config
>
>
>
>
> --
> http://gmerlin.de
> OpenPGP: http://gmerlin.de/christopher.pub
> CB07 DA40 B0B6 571D 35E2 0DEF 87E2 92A7 13E5 DEE1
