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: [email protected] 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
