From daa5d0f71657d49965f1334e417f6e0f2e13e8d9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 14 May 2020 02:56:26 +0200 Subject: [micromega] Revert bad change from 5001deed21e8f4027411cc6413a9d2b98e1bccee Analysis by Jason Gross: > The previous semantics was to reset the file offset to 0 during the > unlock operation, unless it fails, in which case you'd roll back the > file offset to it's present position (and very dubiously not report > any issues). The new semantics say to always roll the file offset > back to it's initial position, meaning that the position is at the > end of the file after unlocking. As far as I can tell, this results > in appending marshelled blobs to the cache file on every call to > add, rather than overwriting the cache file with the marshelled blob > of the updated table. Presumably unmarshelling the concatenation of > marshelled data can result in segfaults somehow? This also explains > why the bug only shows up sometimes; you need to get the system into > a state where it writes to the cache in a way that concatenates > blobs in the right way, but once you have such a cache you'll > segfault every time you read from it. > > I think we should probably assert false in the with block, or just > remove it entirely http://man7.org/linux/man-pages/man3/lockf.3.html > doesn't say anything about lockf erroring on unlocking). If we start > seeing errors, we can turn it into a warning. Closes: #12072 --- plugins/micromega/persistent_cache.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 *) -- cgit v1.2.3 From 660eef91c7ebc0350a17f1947b9bd06029cae3ff Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 13 Apr 2020 16:55:49 -0400 Subject: Revert "Temporarily disable Windows job on Azure." This reverts commit 646a12b2f4660d6e9d5a812febdccab44221d1f0. --- azure-pipelines.yml | 56 ++++++++++++++++++++++++++--------------------------- 1 file changed, 28 insertions(+), 28 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 770cc5193e..0bc30f0196 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -6,37 +6,37 @@ variables: NJOBS: "2" jobs: -#- job: Windows -# pool: -# vmImage: 'vs2017-win2016' +- job: Windows + pool: + vmImage: 'vs2017-win2016' -# 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.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' - job: macOS pool: -- cgit v1.2.3 From 6ce9ba1ca3f7795cf12798ee1bc6d9d2656f8074 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 10 Apr 2020 18:41:36 -0400 Subject: [ci] [azure] Rework windows Azure pipeline - use a different mirror for main cygwin archive - (always) publish build log as artifact - fix call to dune makefiles - we do just build Coq for now, as: + dune is rebuilding Coq to run the test-suite, this needs move investigation. + the test suite seems to take long and it times-out on Win. --- azure-pipelines.yml | 16 +++++++++++++--- dev/ci/azure-build.sh | 2 +- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 0bc30f0196..e76614a0cf 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -10,6 +10,9 @@ jobs: pool: vmImage: 'vs2017-win2016' + # Equivalent to allow_failure: true + # continueOnError: true + steps: - checkout: self fetchDepth: 10 @@ -27,7 +30,7 @@ jobs: C:\cygwin64\bin\bash -l %cd%\dev\build\windows\configure_profile.sh displayName: 'Install cygwin' env: - CYGMIRROR: "http://mirror.easyname.at/cygwin" + CYGMIRROR: "http://mirror.cs.vt.edu/pub/cygwin/cygwin" - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-opam.sh displayName: 'Install opam' @@ -35,8 +38,15 @@ jobs: - 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' + # 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 -- cgit v1.2.3