Re: [isabelle] root.bib as link

On Thu, 16 Feb 2012, Tim (McKenzie) Makarios wrote:

On 15/02/12 23:52, Makarius wrote:
Nonetheless, brief inspection of the default way of copying the document
sources in Isabelle2009-2 (and current Isabelle2011-1) reveals that it
is done by "cp -r -f", which should normally dereference symlinks
(unless you have a very odd version of "cp", which has also happened to
some users in the past).

Further investigation reveals that "cp -r" behaves differently depending
on whether you're using Linux or BSD.  In fact, the BSD man page for cp
says "Historic versions of the cp utility had a -r option.  This
implementation supports that option, however, its use is strongly
discouraged, as it does not correctly copy special files, symbolic links
or fifo's."

It is indeed a running gag of POSIX standards that the meaning of options for cp changes in delicate ways over the decades. We've had to adjust it already 2-3 times before.

I've myself grown up in a classic SunOS / Solaris environment, where -r was the only recursive option, and it did not preserve symlinks. Later GNU cp introduced the more convenient -R and even better the -a option; a bit later they unfortunately made -r coincide with -R. The latter could have dire effects when an avarage Linux user would try to copy directory hierarchies on Solaris, if cp -r in the sense of -R was intended, but would suddenly dereference symlinks -- including cyclic directory links!

Anyway, I've briedly reviewed our current state of affairs, and the man pages for cp of GNU, BSD, POSIX.

I think the intention of cp -r the Isabelle_System.copy_dir function that is used here is to copy a hierarchy without as little surprises as possible. This means to preserve most things, including symlinks. To make this a bit more robust on old-style BSD (i.e. Mac OS X), I am re-using already established option from the Isabelle/jEdit script in Isabelle2011-1: cp -p -R -f.

Since your application of document preparations needs it the other way round, the standard way is to break up the default generation process (e.g. in the makefile). Options of "isabelle usedir" such as -C false and -D generated produce exactly the freshly generated files in generated/. You can then augment the content in any way with cp etc. and finally run something like "isabelle latex -o pdf" on the result. These Isabelle tools are have their man pages in the Isabelle system manual as usual.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.