Email Gateway (Aug 18 2022 at 14:35): Email Gateway (Aug 18 2022 at 14:35):From: Makarius <makarius@sketis.net>
Using -D generated is indeed the usual way to achieve any custom
behaviour, beyond that what the example setup of the document preparation
tool is doing.
BTW, "isatool" and the $ISATOOL variable are way old. The tool wrapper is
called "isabelle", and "$ISABELLE_TOOL" refers to it within the process
environment.
Makarius
Email Gateway (Aug 18 2022 at 14:36):From: Makarius <makarius@sketis.net>
On Mon, 22 Feb 2010, Rafal Kolanski wrote:
Makarius wrote:
USEDIR = $(ISATOOL) usedir -v true -i false -d false -D generated -C false
Using -D generated is indeed the usual way to achieve any custom behaviour,
beyond that what the example setup of the document preparation tool is
doing.I understand, but that isn't my problem. The issue I'm having is that
everything copied into generated by isabelle during the document
generation process is timestamped with the time of the document
generation process, not the timestamps of the original files in the
document directory.
Alternatively, you can use "-D document" to dump the generated sources
into that very same directly, and of course keep "-C false". Or you dump
to a completely different place and adjust the make file accordingly.
No need to copy your other files at all.
If I use -C false and rsync, make will notice that blah.pdf is newer
than blah.svg and not run the conversion.
rsync is part of the answer why special behaviour is avoided by default:
it is not part of the classic Unix canon of tools. Even just plain cp is
very delicate: hardly any of the more advanced options are universally
available.
The usual Isabelle tool policy is to make things work by default, rather
than building too much sophistication into it. (Which does not mean that
the usedir and document tools are not infected by creeping featuritis.)
So I should use $ISABELLE_TOOL instead of $ISATOOL? I don't actually use
the lowercase 'isatool' anywhere. I was porting the IsaMakefile which
had $ISATOOL in it, and it turned out that in 2009-1 that magically did
the right thing (invoked isabelle instead of isatool), so I kept it.
Yes, the ISATOOL setting variable is offically marked as "legacy" since
Isabelle2009 -- see the start of that version's NEWS: "Simplified main
Isabelle executables ...".
Makarius
Email Gateway (Aug 18 2022 at 14:36):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Makarius wrote:
USEDIR = $(ISATOOL) usedir -v true -i false -d false -D generated -C
falseUsing -D generated is indeed the usual way to achieve any custom
behaviour, beyond that what the example setup of the document
preparation tool is doing.
I understand, but that isn't my problem. The issue I'm having is that
everything copied into generated by isabelle during the document
generation process is timestamped with the time of the document
generation process, not the timestamps of the original files in the
document directory. This confuses make, as the sources for files it is
to generate are always newer than any generated files. I think I am
being a bit vague, let me try with an example:
create document/blah.svg and tell document/Makefile to convert it
to a .pdf
isabelle make
(copies document/blah.svg to generated/blah.svg and
document/Makefile to generated/Makefile)
cd document; make
(creates generated/blah.pdf from generated/blah.svg)
change a theory file
isabelle make
(copies document/blah.svg to generated/blah.svg and
document/Makefile to generated/Makefile)
cd document; make
(creates generated/blah.pdf from generated/blah.svg)
Every time I make my document, it'll re-create blah.pdf, despite
blah.svg never changing. Additionally, document/Makefile has
approximately the same timestamp as generated/blah.svg.
If I use -C false and rsync, make will notice that blah.pdf is newer
than blah.svg and not run the conversion.
BTW, "isatool" and the $ISATOOL variable are way old. The tool wrapper
is called "isabelle", and "$ISABELLE_TOOL" refers to it within the
process environment.
So I should use $ISABELLE_TOOL instead of $ISATOOL? I don't actually use
the lowercase 'isatool' anywhere. I was porting the IsaMakefile which
had $ISATOOL in it, and it turned out that in 2009-1 that magically did
the right thing (invoked isabelle instead of isatool), so I kept it.
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 14:49):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Dear All,
Is there any reason that isatool does not preserve timestamps when
copying document/ into (say) generated/ ? I was under the impression
that we should put the document skeleton into document/, run the session
using isatool (so it generates .tex files in generated/) and then invoke
make inside generated/ to create the document itself. However, as it
stands, constructing anything inside generated/ confuses make.
Example: my generated/Makefile generates .pdf files from .svg graphics
for pdflatex as needed. If isatool copies the .svg files from document/,
they are always newer than the .pdf files in generated/, thereby always
undergoing the conversion process.
If .pdf files are placed in document/, they are copied across at the
same time as the .svg files, meaning they most likely have the same
timestamp, which means that even if the .svg file was changed, the .pdf
will not be updated.
My current solution to this is to tell isatool not to copy anything, and
then do the copying manually, like so:
cd ..; $(USEDIR) $(BASE_IMAGE) $(SESSION)
rsync -av -c -H document/ generated
Where:
USEDIR = $(ISATOOL) usedir -v true -i false -d false -D generated -C false
Is there something obvious I'm missing here? I just don't see the reason
not to preserve the timestamps during the copy...
Sincerely,
Rafal Kolanski.
Last updated: Apr 24 2024 at 08:20 UTC