Re: [isabelle] root.bib as link
On Tue, 31 Jan 2012, Tim (McKenzie) Makarios wrote:
I just tried adding a reference list to an Isabelle-generated pdf.
Instead of writing a new .bib file, I decided just to link root.bib to
an existing .bib file that had the necessary reference. Unfortunately,
this didn't result in the reference list being generated and added to
the final Isabelle-generated pdf. It took me quite a while to figure
out what was wrong, because I haven't used .bib files with Isabelle much
before, so I didn't know if I'd inadvertently done something else wrong.
Because of the re-usability of .bib files in general, it would be useful
to be able to link to a large .bib file that contains all the references
an Isabelle-generated document needs. Is the present behaviour a
feature or a bug? (I'm using Isabelle 2009-2.)
Historically there have been occasional surprises about the generated
document directory, so the system is as defensive as feasible, and there
are always ways to deactivate default behaviour and do whatever you like
by hand -- the usedir option -D is particularly useful for that.
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
Is dereferencing what you have expected? Or the other way round? You may
also consider absolute symlinks or hardlinks.
This archive was generated by a fusion of
Pipermail (Mailman edition) and