Merge pull request #391 from MSoegtropIMC/windows-fixes

Windows fixes

.github/workflows/macos.yml

@@ -52,7 +52,7 @@ jobs:
         variant:
           # Keep this in sync with the Smoke test below
           - '8.18~2023.11'
-          - '8.18~mc2~2023.11'
+          - '8.18~mc2'
           - '8.17~2023.08'
 
     steps:
@@ -140,7 +140,7 @@ jobs:
       matrix:
         variant:
           - '8.18~2023.11'
-          - '8.18~mc2~2023.11'
+          - '8.18~mc2'
           - '8.17~2023.08'
 
     steps:

.github/workflows/ubuntu.yml

@@ -59,7 +59,7 @@ jobs:
         variant:
           # This should contain all picks introduced in the current release + all original picks of all Coq versions
           - '8.18~2023.11'
-          - '8.18~mc2~2023.11'
+          - '8.18~mc2'
           - '8.17~2023.08'
           - '8.16~2022.09'
           - '8.15~2022.09'

.github/workflows/windows.yml

@@ -53,7 +53,7 @@ jobs:
         variant:
           # Keep this in sync with the Smoke test below
           - '8.18~2023.11'
-          - '8.18~mc2~2023.11'
+          - '8.18~mc2'
           - '8.17~2023.08'
 
     steps:
@@ -75,11 +75,11 @@ jobs:
 
       - name: Create installer
         shell: cmd
-        run: C:\cygwin_coq_platform\bin\bash --login -c "cd platform/ && windows/create_installer_windows.sh && mkdir /cygdrive/c/installer && cp windows_installer/*exe /cygdrive/c/installer/"
+        run: C:\cygwin_coq_platform\bin\bash --login -c "cd /platform/ && windows/create_installer_windows.sh && mkdir /cygdrive/c/installer && cp windows_installer/*exe /cygdrive/c/installer/"
 
       - name: Create smoke test kit
         shell: cmd
-        run: C:\cygwin_coq_platform\bin\bash --login -c "cd platform/ && shell_scripts/create_smoke_test_kit.sh && mkdir /cygdrive/c/smoke && cp -ra smoke-test-kit/* /cygdrive/c/smoke/"
+        run: C:\cygwin_coq_platform\bin\bash --login -c "cd /platform/ && shell_scripts/create_smoke_test_kit.sh && mkdir /cygdrive/c/smoke && cp -ra smoke-test-kit/* /cygdrive/c/smoke/"
 
       - name: 'Upload Artifact'
         uses: actions/upload-artifact@v2
@@ -107,7 +107,7 @@ jobs:
           - '32'
         variant:
           - '8.18~2023.11'
-          - '8.18~mc2~2023.11'
+          - '8.18~mc2'
           - '8.17~2023.08'
 
     steps:

README.md

@@ -80,6 +80,16 @@ The Coq Platform team does no double check this information.
 
 <details><summary><font size="+1">Release notes / changelog</font></summary>
 
+## Changes in 2023.11.0
+
+- When using the build from sources script on Windows the root folders changed to shorten the path length (e.g. coq-serapi had build issues cause by long path names)
+  - the opam path is now `<cygroot>/opam`  instead of `<cygroot>/home/<user>/.opam`
+  - the platform path is now `<cygroot>/platform`  instead of `<cygroot>/home/<user>/platform`
+  - the (longest) recommended cygwin root path is now `C:\bin\cygwin_coq_platform` or `C:\bin\cygw32_coq_platform`
+- Added new pick 8.18~2023.11 8.18~mc2
+- coq-ott has been added back on Windows
+- coq-fiat-crypto has been removed on Windows, since version 0.0.20 results in stack overflows - there is no good work around for this - we recommend to use the prior pick 8.16~2022.09
+
 ## Changes in 2023.03.0
 
 - Added new picks 8.17~2023.08 and 8.16~2023.08

coq_platform_make_windows.bat

@@ -24,6 +24,7 @@ REM Values are x86_64 or i686 (not 64 or 32)
 SET ARCH=x86_64
 SET SETUP=setup-x86_64.exe
 SET BITS=64
+SET BITSCYGBASE=cygwin
 SET OTHER_BITS=32
 SET OTHER_ARCH=i686
 
@@ -90,13 +91,16 @@ IF "%~0" == "-arch" (
     SET SETUP=setup-x86.exe
     SET CYGWIN_REPOSITORY=%CYGWIN_REPOSITORY_32%
     SET BITS=32
+    REM path length are super critical, especially for ser-api, so we can't user a longer base name for 32 than for 64 bits
+    SET BITSCYGBASE=cygw32
     SET OTHER_BITS=64
     SET OTHER_ARCH=x86_64
   ) ELSE (
     IF "%~1" == "64" (
       SET ARCH=x86_64
       SET SETUP=setup-x86_64.exe
       SET BITS=64
+      SET BITSCYGBASE=cygwin
       SET OTHER_BITS=32
       SET OTHER_ARCH=i686
     ) ELSE (
@@ -283,10 +287,11 @@ IF "%DESTCYG%" == "" (
   ECHO path should indicate that the cygwin is specialized for Coq Platform builds.
   ECHO(
   ECHO The following recommended paths can be chosen by entering a number:
-  ECHO 1  C:\cygwin%BITS%_coq.
-  ECHO 2  C:\cygwin%BITS%_coq_platform.
-  ECHO 3  C:\bin\cygwin%BITS%_coq_platform.
-  ECHO Please enter a number 1...3 or a complete path
+  ECHO 1  C:\%BITSCYGBASE%_coq
+  ECHO 2  C:\%BITSCYGBASE%_coq_platform
+  ECHO 3  C:\bin\%BITSCYGBASE%_coq
+  ECHO 4  C:\bin\%BITSCYGBASE%_coq_platform
+  ECHO Please enter a number 1...4 or a complete path
   ECHO ======================== CYGWIN INSTALLATION LOCATION ========================
   SET /P DESTCYG="Cygwin install folder: "
 )
@@ -302,16 +307,20 @@ IF "%DESTCYG%" == "" (
 )
 
 IF "%DESTCYG%" == "1" (
-  SET DESTCYG=C:\cygwin%BITS%_coq
+  SET DESTCYG=C:\%BITSCYGBASE%_coq
 ) ELSE IF "%DESTCYG%" == "2" (
-  SET DESTCYG=C:\cygwin%BITS%_coq_platform
+  SET DESTCYG=C:\%BITSCYGBASE%_coq_platform
 ) ELSE IF "%DESTCYG%" == "3" (
-  SET DESTCYG=C:\bin\cygwin%BITS%_coq_platform
+  SET DESTCYG=C:\bin\%BITSCYGBASE%_coq
+) ELSE IF "%DESTCYG%" == "4" (
+  SET DESTCYG=C:\bin\%BITSCYGBASE%_coq_platform
 ) ELSE (
   REM CHECK PATH
   IF EXIST %DESTCYG%\NUL (
-    IF NOT EXIST %DESTCYG%\home\%USERNAME%\platform\NUL (
+    IF NOT EXIST %DESTCYG%\platform\NUL (
       ECHO ERROR: The folder %DESTCYG% exists and is not a Coq Platform cygwin folder!
+      ECHO Note: the platform root and opam root path changed in 2023.11 to work around path length issues.
+      ECHO You can still reuse an existing coq platform cygwin installation by starting the script from there.
       EXIT 1
     )
   )
@@ -452,21 +461,18 @@ SET "PROFILEREAD="
 copy "%BATCHDIR%\windows\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOTO ErrorExit
 %BASH% --login "%CYGWIN_INSTALLDIR_CFMT%/var/tmp/configure_profile.sh" "%PROXY%" || GOTO ErrorExit
 
-REM Get cygwin user home folder as windows path
-REM Note: we don't write the full path from cygwin, because it is a bit dangerous if this fails.
-REM We want to prepend USER_HOME_DIR_MFMT here to be sure we stay in this folder.
-SET /p USER_HOME_DIR_CFMT=<"%CYGWIN_INSTALLDIR_WFMT%\var\tmp\main_user_folder.txt"
-SET USER_HOME_DIR_MFMT=%CYGWIN_INSTALLDIR_MFMT%%USER_HOME_DIR_CFMT%
-SET USER_HOME_DIR_WFMT=%USER_HOME_DIR_MFMT:/=\%
+REM Get platform root folder as windows path
+SET PLATFORM_ROOT_DIR_MFMT=%CYGWIN_INSTALLDIR_MFMT%/platform
+SET PLATFORM_ROOT_DIR_WFMT=%PLATFORM_ROOT_DIR_MFMT:/=\%
 
 ECHO ========== BUILD COQ PLATFORM ==========
 
 IF "%BUILD_COQ_PLATFORM%" == "y" (
-  RMDIR /S /Q "%USER_HOME_DIR_MFMT%\platform"
-  MKDIR "%USER_HOME_DIR_MFMT%\platform"
-  XCOPY /S "%BATCHDIR%*.*" "%USER_HOME_DIR_WFMT%\platform" || GOTO ErrorExit
+  RMDIR /S /Q "%PLATFORM_ROOT_DIR_MFMT%"
+  MKDIR "%PLATFORM_ROOT_DIR_MFMT%"
+  XCOPY /S "%BATCHDIR%*.*" "%PLATFORM_ROOT_DIR_WFMT%" || GOTO ErrorExit
 
-  %BASH% --login "%CYGWIN_INSTALLDIR_CFMT%/%USER_HOME_DIR_CFMT%/platform/coq_platform_make.sh" || GOTO ErrorExit
+  %BASH% --login "%CYGWIN_INSTALLDIR_CFMT%/platform/coq_platform_make.sh" || GOTO ErrorExit
 
 ) ELSE (
   ECHO Note: Automatic Coq Platform build has been disabled with -build=n

opam/opam-repository/packages/ott/ott.0.33/opam

@@ -15,6 +15,9 @@ depends: [
 build: [
   [make "world"] { ocaml:native }
   [make "world.byt"] { !ocaml:native }
+  ["rm" "src/ott"] {os = "win32"}
+  ["cp" "src/ott.opt" "src/ott"] {os = "win32" & ocaml:native}
+  ["cp" "src/ott.byte" "src/ott"] {os = "win32" & !ocaml:native}
   [make "ott.install"]
 ]
 run-test: [

package_picks/package-pick-8.18~2023.11.sh

@@ -148,13 +148,8 @@ then
   PACKAGES="${PACKAGES} coq-reglang.1.1.3"
   PACKAGES="${PACKAGES} coq-iris.4.1.0"
   PACKAGES="${PACKAGES} coq-iris-heap-lang.4.1.0"
-  if [[ "$OSTYPE" != cygwin ]]
-  then
-    # Windows: some issues with executable extensions (ott.opt instead of ott.exe)
-    # Note: 0.32 does work on Windows!
-    PACKAGES="${PACKAGES} coq-ott.0.33"
-    PACKAGES="${PACKAGES} ott.0.33"
-  fi
+  PACKAGES="${PACKAGES} coq-ott.0.33"
+  PACKAGES="${PACKAGES} ott.0.33"
   PACKAGES="${PACKAGES} coq-mathcomp-word.2.1"
 
   case "$COQ_PLATFORM_COMPCERT" in
@@ -195,11 +190,7 @@ then
   PACKAGES="${PACKAGES} coq-record-update.0.3.3"
 
   # Communication with coqtop
-  if [[ "$OSTYPE" != cygwin ]]
-  then
-    # Windows: path length issues
-    PACKAGES="${PACKAGES} coq-serapi.8.18.0+0.18.1"
-  fi
+  PACKAGES="${PACKAGES} coq-serapi.8.18.0+0.18.1"
 
   # fiat crypto, bedrock2, rupicola and dependencies
   if [ "${BITSIZE}" == "64" ]

package_picks/package-pick-8.18~mc2~2023.11.sh → package_picks/package-pick-8.18~mc2.sh

@@ -18,7 +18,7 @@ COQ_PLATFORM_VERSION_SORTORDER=2
 # It is usually either empty ot starts with ~.
 # It might also be used for installer package names, but with ~ replaced by _
 # It is also used for version specific file selections in the smoke test kit.
-COQ_PLATFORM_PACKAGE_PICK_POSTFIX='~8.18~mc2~2023.11'
+COQ_PLATFORM_PACKAGE_PICK_POSTFIX='~8.18~mc2'
 
 # The corresponding Coq development branch and tag
 COQ_PLATFORM_COQ_BRANCH='v8.18'
@@ -148,13 +148,8 @@ then
   PACKAGES="${PACKAGES} coq-reglang.1.2.0"
   PACKAGES="${PACKAGES} coq-iris.4.1.0"
   PACKAGES="${PACKAGES} coq-iris-heap-lang.4.1.0"
-  if [[ "$OSTYPE" != cygwin ]]
-  then
-    # Windows: some issues with executable extensions (ott.opt instead of ott.exe)
-    # Note: 0.32 does work on Windows!
-    PACKAGES="${PACKAGES} coq-ott.0.33"
-    PACKAGES="${PACKAGES} ott.0.33"
-  fi
+  PACKAGES="${PACKAGES} coq-ott.0.33"
+  PACKAGES="${PACKAGES} ott.0.33"
   # PACKAGES="${PACKAGES} coq-mathcomp-word.2.1" # requires coq-mathcomp-ssreflect < 1.18~
 
   case "$COQ_PLATFORM_COMPCERT" in
@@ -195,11 +190,7 @@ then
   PACKAGES="${PACKAGES} coq-record-update.0.3.3"
 
   # Communication with coqtop
-  if [[ "$OSTYPE" != cygwin ]]
-  then
-    # Windows: path length issues
-    PACKAGES="${PACKAGES} coq-serapi.8.18.0+0.18.1"
-  fi
+  PACKAGES="${PACKAGES} coq-serapi.8.18.0+0.18.1"
 
   # fiat crypto, bedrock2, rupicola and dependencies
   if [ "${BITSIZE}" == "64" ]

shell_scripts/check_system.sh

@@ -69,12 +69,15 @@ then
 	fi
 
     # On 32 bit cygwin on GitHub somehow the certificate database is broken - fix it
-	echo "============ Fix certificate database ============"
-    ls -l /etc/pki/tls/certs/
-    ls -lL /etc/pki/tls/certs/
-    update-ca-trust
-    ls -lL /etc/pki/tls/certs/
-	echo "============ Fix certificate database done ============"
+	if [ "${BITSIZE}" == "32" ]
+	then
+		echo "============ Fix certificate database ============"
+		ls -l /etc/pki/tls/certs/
+		ls -lL /etc/pki/tls/certs/
+		update-ca-trust
+		ls -lL /etc/pki/tls/certs/
+		echo "============ Fix certificate database done ============"
+	fi
 
 else
 		echo "ERROR: unsopported OS type '$OSTYPE'"

shell_scripts/create_smoke_test_kit.sh

@@ -77,7 +77,7 @@ TEST_FILES[coq-elpi~dev]='examples/tutorial_coq_elpi.v examples/tutorial_elpi_la
 TEST_FILES[coq-equations]='examples/Fin.v examples/STLC.v'
 TEST_FILES[coq-ext-lib]='examples/MonadReasoning.v examples/Printing.v'
 TEST_FILES[coq-extructures]='../../test_files/coq-extructures/tutorial.v'
-TEST_FILES[coq-extructures~8.18~mc2~2023.11]='tests/tutorial.v'
+TEST_FILES[coq-extructures~8.18~mc2]='tests/tutorial.v'
 TEST_FILES[coq-fiat-crypto]='src/Demo.v'
 TEST_FILES[coq-flocq]='examples/Average.v' # In fixing: examples/Cody_Waite.v
 TEST_FILES[coq-flocq3]='examples/Average.v' # In fixing: examples/Cody_Waite.v
@@ -121,7 +121,7 @@ TEST_FILES[coq-mathcomp-word]='../../test_files/coq-mathcomp-word/test_upto_8_16
 TEST_FILES[coq-mathcomp-word~8.16~2023.08]='../../test_files/coq-mathcomp-word/test.v'
 TEST_FILES[coq-mathcomp-word~8.17~2023.08]='../../test_files/coq-mathcomp-word/test.v'
 TEST_FILES[coq-mathcomp-word~8.18~2023.11]='../../test_files/coq-mathcomp-word/test.v'
-TEST_FILES[coq-mathcomp-word~8.18~mc2~2023.11]='../../test_files/coq-mathcomp-word/test.v'
+TEST_FILES[coq-mathcomp-word~8.18~mc2]='../../test_files/coq-mathcomp-word/test.v'
 TEST_FILES[coq-mathcomp-zify]='examples/divmod.v examples/boolean.v'
 TEST_FILES[coq-menhirlib]='coq-menhirlib/src/Alphabet.v'
 TEST_FILES[coq-metacoq]='examples/metacoq_tour_prelude.v examples/metacoq_tour.v'

windows/configure_profile.sh

@@ -39,11 +39,12 @@ if [ ! -f $donefile ] ; then
   # Set a marker that this is a cygwin intended for Coq Platform compilation
   echo export COQ_PLATFORM_CYGWIN_OK=Y
 
+  # Set the opam root folder
+  echo export OPAMROOT="'$(cygpath -aw /opam)'"
+  echo export PLATFORMROOT="'$(cygpath -aw /platform)'"
+
   exec 1>&6 6>&-       # Restore stdout from file descriptor 6 and close file descriptor #6
 
   touch $donefile
 fi
 
-###################### REPORT USER FOLDER ######################
-
-echo $HOME > /var/tmp/main_user_folder.txt