Email Gateway (Aug 18 2022 at 19:03): Email Gateway (Aug 18 2022 at 19:03):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
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.)
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 19:08):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 19:09):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
On 15/02/12 23:52, Makarius wrote:
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).
I have the cp that comes by default with Ubuntu 10.04 --- it reports
itself as "cp (GNU coreutils) 7.4".
Is dereferencing what you have expected? Or the other way round? You
may also consider absolute symlinks or hardlinks.
What happens is that in the directory of generated LaTeX sources, I get
a copy of the "root.bib" symlink, which is a relative link, and does, in
fact, point to the right file. This is because in my "geometry"
directory, which has my .thy files and ROOT.ML, I have the
subdirectories "document" and "generated". The former has "root.tex"
and "root.bib", which is a link to "../../thesis/references.bib". As a
consequence, when this link is copied to the "generated" directory,
"../../thesis/references.bib" still points to the correct file.
However, the "document.pdf" that ends up being generated has only [?]
instead of [1], and has no reference list at the end.
An absolute symlink would be difficult to arrange, because I'm using
Subversion to work on the same files in two locations, and the directory
layout differs between the locations. I don't have experience with
hardlinks, but I could find out about them if necessary. At the moment
it's not necessary, though, because my current workaround is to have
"root.bib" as an ordinary file, and "../../thesis/references.bib" as a
symlink to "root.bib".
Makarius
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 19:09):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
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."
I suggest that Isabelle should use "cp -R -L -f" instead of "cp -r -f",
in order to behave the same way on Linux and BSD.
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 19:10):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 19:10):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
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.
Tim
<><
signature.asc
Last updated: Apr 16 2024 at 20:15 UTC