From ec505a2fa67b0776b624be54417e06c6512f1734 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 19 Dec 2019 14:18:12 +0100
Subject: Fix #11303: skip complexity tests on windows even if bogomips found

Apparently the bogomips produced by cygwin are extra-bogo.
---
 test-suite/Makefile | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 609a61226b..bcaac9752e 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -71,6 +71,9 @@ get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_
 get_set_impredicativity= $(filter "-impredicative-set",$(call get_coq_prog_args,$(1)))
 
 bogomips:=
+ifeq (win32,$(ARCH))
+  $(warning windows detected: skipping complexity tests)
+else
 ifneq (,$(wildcard /proc/cpuinfo))
   sedbogo := -e "s/bogomips.*: \([0-9]*\).*/\1/p" # i386, ppc
   sedbogo += -e "s/Cpu0Bogo.*: \([0-9]*\).*/\1/p" # sparc
@@ -81,6 +84,7 @@ endif
 ifeq (,$(bogomips))
   $(warning cannot run complexity tests (no bogomips found))
 endif
+endif
 
 # keep these synced with test-suite/save-logs.sh
 log_success = "==========> SUCCESS <=========="
-- 
cgit v1.2.3


From 4a402fe71e79fd005f7c03a9b5cc0d0a30dc9fe9 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 19 Dec 2019 09:12:51 -0500
Subject: Revert "Fix #11303: skip complexity tests on windows even if bogomips
 found"

This reverts commit ec505a2fa67b0776b624be54417e06c6512f1734.

A better fix is coming
---
 test-suite/Makefile | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index bcaac9752e..609a61226b 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -71,9 +71,6 @@ get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_
 get_set_impredicativity= $(filter "-impredicative-set",$(call get_coq_prog_args,$(1)))
 
 bogomips:=
-ifeq (win32,$(ARCH))
-  $(warning windows detected: skipping complexity tests)
-else
 ifneq (,$(wildcard /proc/cpuinfo))
   sedbogo := -e "s/bogomips.*: \([0-9]*\).*/\1/p" # i386, ppc
   sedbogo += -e "s/Cpu0Bogo.*: \([0-9]*\).*/\1/p" # sparc
@@ -84,7 +81,6 @@ endif
 ifeq (,$(bogomips))
   $(warning cannot run complexity tests (no bogomips found))
 endif
-endif
 
 # keep these synced with test-suite/save-logs.sh
 log_success = "==========> SUCCESS <=========="
-- 
cgit v1.2.3


From 6b309b4297f28fcc6774ac3a19ab830713ec5e62 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 18 Dec 2019 18:16:13 -0500
Subject: Fix complexity test-suite failure reporting on Win

Apparently `expr 1 \+ 1` is fine on Linux but not cygwin/Windows, where
it fails with "syntax error".  Similarly for `-` and `/`.
---
 test-suite/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 609a61226b..7e2ef3bc75 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -544,7 +544,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	    true "find expected time * 100"; \
 	    exp=`sed -n -e "s/(\*.*Expected time < \([0-9]\).\([0-9][0-9]\)s.*\*)/\1\2/p" "$<"`; \
 	    true "compute corrected effective time, rounded up"; \
-	    rescorrected=`expr \( $$res \* $(bogomips) \+ 6120 \- 1 \) \/ 6120`; \
+	    rescorrected=`expr \( $$res \* $(bogomips) + 6120 - 1 \) / 6120`; \
 	    ok=`expr \( $$res \* $(bogomips) \) "<" \( $$exp \* 6120 \)`; \
 	    if [ "$$ok" = 1 ]; then \
 	      echo $(log_success); \
-- 
cgit v1.2.3


From baab1c01b22d754df64a09be436d350663cc1c28 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 18 Dec 2019 20:39:06 -0500
Subject: Better error reporting when res is not what is expected

c.f. https://dev.azure.com/coq/coq/_build/results?buildId=6485&view=logs&jobId=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&j=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&t=77aad734-2057-5694-9ae2-ee1f5f26eae8
---
 test-suite/Makefile | 28 +++++++++++++++++-----------
 1 file changed, 17 insertions(+), 11 deletions(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 7e2ef3bc75..1546b7cf62 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -540,19 +540,25 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	    echo "    $<...Error! (couldn't find a time measure)"; \
 	  else \
 	    true "express effective time in centiseconds"; \
+	    resorig="$$res"; \
 	    res=`echo "$$res"00 | sed -n -e "s/\([0-9]*\)\.\([0-9][0-9]\).*/\1\2/p"`; \
-	    true "find expected time * 100"; \
-	    exp=`sed -n -e "s/(\*.*Expected time < \([0-9]\).\([0-9][0-9]\)s.*\*)/\1\2/p" "$<"`; \
-	    true "compute corrected effective time, rounded up"; \
-	    rescorrected=`expr \( $$res \* $(bogomips) + 6120 - 1 \) / 6120`; \
-	    ok=`expr \( $$res \* $(bogomips) \) "<" \( $$exp \* 6120 \)`; \
-	    if [ "$$ok" = 1 ]; then \
-	      echo $(log_success); \
-	      echo "    $<...Ok"; \
-	    else \
+	    if [ "$$res" = "" ]; then \
 	      echo $(log_failure); \
-	      echo "    $<...Error! (should run faster ($$rescorrected >= $$exp))"; \
-	      $(FAIL); \
+	      echo "    $<...Error! (invalid time measure: $$resorig)"; \
+	    else \
+	      true "find expected time * 100"; \
+	      exp=`sed -n -e "s/(\*.*Expected time < \([0-9]\).\([0-9][0-9]\)s.*\*)/\1\2/p" "$<"`; \
+	      true "compute corrected effective time, rounded up"; \
+	      rescorrected=`expr \( $$res \* $(bogomips) + 6120 - 1 \) / 6120`; \
+	      ok=`expr \( $$res \* $(bogomips) \) "<" \( $$exp \* 6120 \)`; \
+	      if [ "$$ok" = 1 ]; then \
+	        echo $(log_success); \
+	        echo "    $<...Ok"; \
+	      else \
+	        echo $(log_failure); \
+	        echo "    $<...Error! (should run faster ($$rescorrected >= $$exp))"; \
+	        $(FAIL); \
+	      fi; \
 	    fi; \
 	  fi; \
 	} > "$@"
-- 
cgit v1.2.3


From 925a87275245fbd1ea5142f02950f89a8b37d19c Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 19 Dec 2019 09:13:48 -0500
Subject: Remove trailing \r in complexity measures for Windows

---
 test-suite/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 1546b7cf62..b3a633e528 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -530,7 +530,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
 	  true "extract effective user time"; \
-	  res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \
+	  res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1 | sed "s/\r//g"`; \
 	  R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	    echo $(log_failure); \
-- 
cgit v1.2.3