Re: [isabelle] Should isatool document preparation preserve timestamps while copying?




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. 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.





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