Bug#238257: race condition on timestamps for cmi/mli files

[Remi Vanicat <remi.vanicat@laposte.net>]

Mike Furr <mfurr@debian.org> writes:

> On Tue, 2004-03-16 at 01:57, Remi Vanicat wrote:
>> What is strange here is that OCamlMakefile use explicit depend over
>> some system library. It should not even bother. He may even not know
>> that there exist a gl.cmi (and gl.mli) file. How do you use the
>> OCamlMakefile ?
> Yes.  The problem is that it uses ocamldep too strictly.
>
> On Tue, 2004-03-16 at 04:55, Remi Vanicat wrote: 
>> precisely this Makefile do Work :
> <snip>
> This is essentially what I was using.  To be sure, I copied your
> example and the same thing occurs.  You should be able to replicate
> it by doing
>  $ sudo touch /usr/lib/ocaml/3.07/lablgl/gl.mli
>  $ make
> So the problem is that dpkg might unpack some ocaml package and start
> copying the files while crossing over a 1 second boundry.
> Since gl.cm* is copied before gl.mli, its possible that the gl.mli
> will get a later timestamp.  Thus when ocamldep reports that
> gears.ml depends on gl.mli and gl.mli is older than gl.cmi, it will
> try and recompile them, resulting in an error.  Precisely:
>  ocamlc -c -I +labltk -I +lablgl -I +labltk -I +lablgl 
>   /usr/lib/ocaml/3.07/lablgl/gl.mli
>  I/O error: /usr/lib/ocaml/3.07/lablgl/gl.cmi: Permission denied

Okay, I've understood, and I believed I see from where it come. I will
contact upstream (Markus Mottle) about it.

-- 
Rémi Vanicat