Re: [isabelle] root.bib as link

On 17/02/12 02:10, Makarius wrote:
> 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.
>     Makarius

Thanks for doing all this.  For now I think it is sufficient for me to
avoid the problem by linking into "root.bib" in the "document"
directory, instead of making "root.bib" a link pointing out of the
directory.  In future, if I have a more complex situation, I'll keep in
mind the possibility of putting more fine-grained commands in the
makefile, as you suggest.


Attachment: signature.asc
Description: OpenPGP digital signature

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