Merge PR #12071: [ci] [micromega] Fix windows build and Micromega bug introduced in #11756

Reviewed-by: Zimmi48

3 files changed, 41 insertions, 31 deletions

diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 770cc5193e..e76614a0cf 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -6,37 +6,47 @@ variables:
   NJOBS: "2"
 
 jobs:
-#- job: Windows
-#  pool:
-#    vmImage: 'vs2017-win2016'
+- job: Windows
+  pool:
+    vmImage: 'vs2017-win2016'
+
+  # Equivalent to allow_failure: true
+  # continueOnError: true
 
-#  steps:
-#  - checkout: self
-#    fetchDepth: 10
+  steps:
+  - checkout: self
+    fetchDepth: 10
 
   # cygwin package list not checked for minimality
-#  - script: |
-#      powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')"
-#      SET CYGROOT=C:\cygwin64
-#      SET CYGCACHE=%CYGROOT%\var\cache\setup
-#      setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python3
-
-#      SET TARGET_ARCH=x86_64-w64-mingw32
-#      SET CD_MFMT=%cd:\=/%
-#      SET RESULT_INSTALLDIR_CFMT=%CD_MFMT:C:/=/cygdrive/c/%
-#      C:\cygwin64\bin\bash -l %cd%\dev\build\windows\configure_profile.sh
-#    displayName: 'Install cygwin'
-#    env:
-#      CYGMIRROR: "http://mirror.easyname.at/cygwin"
-
-#  - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-opam.sh
-#    displayName: 'Install opam'
-
-#  - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-build.sh
-#    displayName: 'Build Coq'
-
-#  - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-test.sh
-#    displayName: 'Test Coq'
+  - script: |
+      powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')"
+      SET CYGROOT=C:\cygwin64
+      SET CYGCACHE=%CYGROOT%\var\cache\setup
+      setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python3
+
+      SET TARGET_ARCH=x86_64-w64-mingw32
+      SET CD_MFMT=%cd:\=/%
+      SET RESULT_INSTALLDIR_CFMT=%CD_MFMT:C:/=/cygdrive/c/%
+      C:\cygwin64\bin\bash -l %cd%\dev\build\windows\configure_profile.sh
+    displayName: 'Install cygwin'
+    env:
+      CYGMIRROR: "http://mirror.cs.vt.edu/pub/cygwin/cygwin"
+
+  - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-opam.sh
+    displayName: 'Install opam'
+
+  - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-build.sh
+    displayName: 'Build Coq'
+
+  # We are hitting a bug where Dune is rebuilding Coq to run the
+  # test-suite, also it seems to time out, so we just build for now
+  #
+  # - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-test.sh
+  #   displayName: 'Test Coq'
+
+  - publish: _build/log
+    artifact: Dune Build Log
+    condition: always()
 
 - job: macOS
   pool:
diff --git a/dev/ci/azure-build.sh b/dev/ci/azure-build.sh
index 04c7d5db91..494651c5bf 100755
--- a/dev/ci/azure-build.sh
+++ b/dev/ci/azure-build.sh
@@ -4,4 +4,4 @@ set -e -x
 
 cd $(dirname $0)/../..
 
-make -f Makefile.dune coq coqide-server
+dune build coq.install coqide-server.install
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 9051bbb5ca..3360a9a51c 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -93,9 +93,9 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct
            there is a pending lock which could cause a deadlock.
            Should it be an anomaly or produce a warning ?
         *)
-        ()
+        ignore (lseek fd pos SEEK_SET)
     in
-    ignore (lseek fd pos SEEK_SET)
+    ()
 
   (* We make the assumption that an acquired lock can always be released *)