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 the past).

Is dereferencing what you have expected? Or the other way round? You may also consider absolute symlinks or hardlinks.


	Makarius





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