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
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