Email Gateway (Aug 18 2022 at 09:42): Email Gateway (Aug 18 2022 at 09:42):From: Francisco Jose CHAVES ALONSO <Francisco.Jose.Chaves.Alonso@ens-lyon.fr>
Hi,
I need the TeX file generated by Isabelle, to extract some parts for
another document that I also generate with another command.
"isatool make" delete the TeX generated file. It is possible to save it?
Thanks in advance
Francisco
Email Gateway (Aug 18 2022 at 09:42):From: Martin Ellis <m.a.ellis@ncl.ac.uk>
I have a patch for Pure which does a few things, including this.
I've tried to snip out the relevant parts (thank heavens for
diff-mode!), and attached the result.
It should apply against Isabelle 2005, but I haven't tested it.
(Note that I don't code in ML. Do feel free to laugh at it.)
Once applied, you'd need to delete all your logic heaps and rebuild.
To prevent the tex files being cleaned up, you can then add something
like:
Present.no_clean := true;
to the ROOT.ML file for the relevant logic (I do so at the top).
Martin
isabelle2005.diff
Email Gateway (Aug 18 2022 at 09:42):From: Martin Ellis <m.a.ellis@ncl.ac.uk>
Uh... on second thoughts, if you're not already poking about with
Pure, it's going to be much easier to edit lib/Tools/document - this
looks like it might be the offending line:
[ -n "$CLEAN" ] && rm -rf "$DIR"
Martin
Email Gateway (Aug 18 2022 at 09:42):From: Stefan Berghofer <berghofe@in.tum.de>
Francisco Jose CHAVES ALONSO wrote:
Hello Francisco,
in the IsaMakefile generated by isatool mkdir, there is a line of the form
USEDIR = $(ISATOOL) usedir -v true -i true -d pdf ## -D generated
If you remove the comment sign "##" before "-D generated", isatool make will
save the generated TeX files in the subdirectory MyTheories/generated, where
MyTheories is the subdirectory in which your theory files reside. You can
also replace "-d pdf" by "-d false" if you do not want isatool make to generate
a *.pdf file from the generated TeX files, e.g. because you want to generate
the *.pdf file yourself (after some postprocessing).
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 09:43):From: Stefan Berghofer <berghofe@in.tum.de>
Stefan Berghofer wrote:
USEDIR = $(ISATOOL) usedir -v true -i true -d pdf ## -D generated
For more information on the -D option, see also section 2.4 "Running
Isabelle sessions -- isatool usedir" of the Isabelle System Manual,
available at http://isabelle.in.tum.de/dist/Isabelle/doc/system.pdf
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 09:43):From: Makarius <makarius@sketis.net>
See the documentation, notably the system manual. The usage of isatool
usedir will also give you the right clues, e.g. about option -D to dump
generated document sources.
Makarius
Last updated: May 03 2024 at 04:19 UTC