diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-06 09:48:03 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-06 09:48:03 +0000 |
commit | 43100469fcdc2c39e9540222648000f5de661ee5 (patch) | |
tree | 73aa813441fae544693e949e667a018aa7d87a2e /plugins/micromega/persistent_cache.ml | |
parent | c8326c6365bb7b07d3c2fa86757ba364c5879dc5 (diff) |
Try to make the use of Unix.lockf in micromega compatible with Win32
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15684 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/micromega/persistent_cache.ml')
-rw-r--r-- | plugins/micromega/persistent_cache.ml | 30 |
1 files changed, 20 insertions, 10 deletions
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index ed9fdcead..aa5ff857c 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -95,14 +95,24 @@ let read_key_elem inch = | End_of_file -> None | _ -> raise InvalidTableFormat +(** In win32, it seems that we should unlock the exact zone + that has been locked, and not the whole file *) -let unlock fd = - try - let pos = lseek fd 0 SEEK_CUR in - ignore (lseek fd 0 SEEK_SET) ; - lockf fd F_ULOCK 0 ; +let locked_start = ref 0 + +let lock fd = + locked_start := lseek fd 0 SEEK_CUR; + lockf fd F_LOCK 0 + +let rlock fd = + locked_start := lseek fd 0 SEEK_CUR; + lockf fd F_RLOCK 0 + +let unlock fd = + let pos = lseek fd 0 SEEK_CUR in + ignore (lseek fd !locked_start SEEK_SET); + lockf fd F_ULOCK 0; ignore (lseek fd pos SEEK_SET) - with exc -> failwith (Printexc.to_string exc) let open_in f = let flags = [O_RDONLY ; O_CREAT] in @@ -118,7 +128,7 @@ let open_in f = xload () in try (* Locking of the (whole) file while reading *) - lockf finch F_RLOCK 0 ; + rlock finch; finally (fun () -> xload () ) (fun () -> @@ -136,7 +146,7 @@ let open_in f = let flags = [O_WRONLY; O_TRUNC;O_CREAT] in let out = (openfile f flags 0o666) in let outch = out_channel_of_descr out in - lockf out F_LOCK 0 ; + lock out; (try Table.iter (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl; @@ -168,8 +178,8 @@ let add t k e = let fd = descr_of_out_channel outch in begin Table.add tbl k e ; - lockf fd F_LOCK 0 ; - ignore (lseek fd 0 SEEK_END) ; + lock fd; + ignore (lseek fd 0 SEEK_END); Marshal.to_channel outch (k,e) [Marshal.No_sharing] ; flush outch ; unlock fd |