Add CI tests for Windows and Mac

.github/workflows/coq-macos.yml

@@ -0,0 +1,82 @@
+name: CI (Coq, MacOS)
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build-macos:
+
+    runs-on: macOS-11
+
+    concurrency:
+      group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+      cancel-in-progress: true
+
+    env:
+      NJOBS: "2"
+      COQ_VERSION: "8.15.2"
+      COQCHKEXTRAFLAGS: ""
+
+    steps:
+    - uses: actions/checkout@v3
+      with:
+        submodules: recursive
+    - name: Set up OCaml
+      uses: ocaml/setup-ocaml@v2
+      with:
+        ocaml-compiler: 4.11.1
+
+    - name: Install system dependencies
+      run: |
+        set -e
+        brew install gnu-time coreutils
+
+    - name: Install Coq
+      run: |
+        set -e
+        eval $(opam env)
+        opam update
+        opam pin add coq ${COQ_VERSION}
+      env:
+        OPAMYES: "true"
+        OPAMCONFIRMLEVEL: "unsafe-yes"
+
+    - name: echo build params
+      run: |
+        eval $(opam env)
+        echo "::group::sysctl -n machdep.cpu.brand_string"
+        sysctl -n machdep.cpu.brand_string
+        echo "::endgroup::"
+        echo "::group::sysctl -a | grep machdep.cpu"
+        sysctl -a | grep machdep.cpu
+        echo "::endgroup::"
+        echo "::group::uname -a"
+        uname -a
+        echo "::endgroup::"
+        echo "::group::sw_vers -productVersion"
+        sw_vers -productVersion
+        echo "::endgroup::"
+        echo "::group::system_profiler SPSoftwareDataType"
+        system_profiler SPSoftwareDataType
+        echo "::endgroup::"
+        echo "::group::opam list"
+        opam list
+        echo "::endgroup::"
+        echo "::group::ocamlc -config"
+        ocamlc -config
+        echo "::endgroup::"
+        echo "::group::coqc --config"
+        coqc --config
+        echo "::endgroup::"
+        echo "::group::coqc --version"
+        coqc --version
+        echo "::endgroup::"
+        echo "::group::true | coqtop"
+        true | coqtop
+        echo "::endgroup::"
+    - name: make
+      run: |
+        eval $(opam env)
+        make TIMED=1 -j${NJOBS}

.github/workflows/coq-windows.yml

@@ -0,0 +1,88 @@
+name: CI (Coq, Windows)
+
+# Note that we must split up each command into a separate step for Windows, because otherwise we don't get error code
+# See also /~https://github.com/avsm/setup-ocaml/issues/72
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build-windows:
+
+    runs-on: windows-latest
+
+    concurrency:
+      group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+      cancel-in-progress: true
+
+    env:
+      NJOBS: "2"
+      COQ_VERSION: "8.15.2" # https://packages.debian.org/testing/coq
+      COQEXTRAFLAGS: "-async-proofs-j 1"
+      COQCHKEXTRAFLAGS: ""
+      OPAMYES: "true"
+      OPAMCONFIRMLEVEL: "unsafe-yes"
+
+    steps:
+    - uses: actions/checkout@v3
+      with:
+        submodules: recursive
+    - name: Set up OCaml
+      uses: ocaml/setup-ocaml@v2
+      with:
+        ocaml-compiler: 4.11.1
+    - run: opam depext coq.${{ env.COQ_VERSION }}
+    - run: opam pin add --kind=version coq ${{ env.COQ_VERSION }}
+
+    - name: Install System Dependencies
+      run: |
+        %CYGWIN_ROOT%\setup-x86_64.exe -qnNdO -P time
+      shell: cmd
+
+    - name: Work around /~https://github.com/actions/checkout/issues/766
+      run: |
+        %CYGWIN_ROOT%\bin\bash.exe -l -c 'git config --global --add safe.directory "*"'
+      shell: cmd
+
+    - name: echo build params
+      run: |
+        ECHO ::group::wmic cpu get caption, deviceid, name, numberofcores, maxclockspeed, status
+        wmic cpu get caption, deviceid, name, numberofcores, maxclockspeed, status
+        ECHO ::endgroup::
+        ECHO ::group::wmic cpu list /format:list
+        wmic cpu list /format:list
+        ECHO ::endgroup::
+        ECHO ::group::git config -l
+        %CYGWIN_ROOT%\bin\bash.exe -l -c 'git config -l'
+        ECHO ::endgroup::
+        ECHO ::group::git config --global -l
+        %CYGWIN_ROOT%\bin\bash.exe -l -c 'git config --global -l'
+        ECHO ::endgroup::
+        ECHO ::group::opam list
+        opam list
+        ECHO ::endgroup::
+        ECHO ::group::ocamlc -config
+        opam exec -- ocamlc -config
+        ECHO ::endgroup::
+        ECHO ::group::coqc --config
+        opam exec -- coqc --config
+        ECHO ::endgroup::
+        ECHO ::group::coqc --version
+        opam exec -- coqc --version
+        ECHO ::endgroup::
+        ECHO ::group::coqtop version
+        echo | opam exec -- coqtop
+        ECHO ::endgroup::
+        ECHO ::group::make printenv
+        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- make printenv'
+        ECHO ::endgroup::
+        ECHO ::group::PATH
+        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; echo "${PATH}"'
+        ECHO ::endgroup::
+      shell: cmd
+    - name: make
+      run: |
+        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- make TIMED=1 -j${NJOBS}'
+      shell: cmd

.github/workflows/coq.yml

@@ -5,6 +5,7 @@ name: Coq
 on:
   push:
   pull_request:
+  workflow_dispatch:
 
 jobs:
   build:
@@ -22,6 +23,10 @@ jobs:
 
     env: ${{ matrix.env }}
 
+    concurrency:
+      group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+      cancel-in-progress: true
+
     steps:
     - name: install Coq
       run: |
@@ -56,7 +61,7 @@ jobs:
         echo | coqtop
         echo "::endgroup::"
     - uses: actions/checkout@v3
-    - name: submodules-init
-      run: git submodule update --init --recursive
+      with:
+        submodules: recursive
     - name: make
       run: TIMED=1 make

Makefile

@@ -72,13 +72,13 @@ install_coqutil:
 	$(MAKE) -C $(DEPS_DIR)/coqutil install
 
 coq-record-update:
-	$(MAKE) -C $(DEPS_DIR)/coq-record-update
+	$(MAKE) NO_TEST=1 -C $(DEPS_DIR)/coq-record-update
 
 clean_coq-record-update:
-	$(MAKE) -C $(DEPS_DIR)/coq-record-update clean
+	$(MAKE) NO_TEST=1 -C $(DEPS_DIR)/coq-record-update clean
 
 install_coq-record-update:
-	$(MAKE) -C $(DEPS_DIR)/coq-record-update install
+	$(MAKE) NO_TEST=1 -C $(DEPS_DIR)/coq-record-update install
 
 kami:
 	$(MAKE) -C $(DEPS_DIR)/kami

etc/bytedump.sh

@@ -7,23 +7,28 @@ coqtop -q -quiet $COQFLAGS 2>/dev/null << EOF
 Require bedrock2.PrintListByte ${1%.*}.
 Local Set Printing Width 2147483647.
 Goal True.
-  idtac "COQTOP_CRAP_ENDS_HERE".
+  idtac "COQBUG(15373)".
+  idtac "LINE_SEPARATOR_LOTTERY".
   PrintListByte.print_list_byte ${1}.
 Abort.
 EOF
-} | python3 -c '
-import os, sys
-needle = b"\nCOQTOP_CRAP_ENDS_HERE\n"
-waiting_on_coqbug_15373 = True
+} | python3 -c '#  strip header, detect \r\n or \n, convert to \n, strip last \n
+import os, sys # os.linesep is \n on cygwin but \r\n in cygwin coq on github ci
+b = b""
+while not b.endswith(b"COQBUG(15373)"):
+	r = os.read(0, 1); b += r
+	if not r: print(f"{b!r}"); sys.exit(4)
+b = b""
+while not b.endswith(b"LINE_SEPARATOR_LOTTERY"):
+	r = os.read(0, 1); b += r
+	if not r: print(f"{b!r}"); sys.exit(3)
+linesep = b[:-len(b"LINE_SEPARATOR_LOTTERY")]
+os.read(0, len(linesep)) == linesep or sys.exit(2)
 b = b""
 while True:
-	r = os.read(0, 1)
-	if not r:
-		sys.exit(waiting_on_coqbug_15373 + 2*(not b.endswith(b"\n")))
-	b = b[-(len(needle)-len(r)):] + r
-	if b == needle:
-		waiting_on_coqbug_15373 = 0
-		b = b""
-	if not waiting_on_coqbug_15373:
-		os.write(1, b[-2:-1])
+	r = os.read(0, 1); b += r
+	if not r: sys.exit(not b.endswith(b"\n"))
+	if b == linesep: b = b"\n"
+	os.write(1, b[-2:-1])
+	b = b[-1:]
 '