Email Gateway (Aug 18 2022 at 10:14): Email Gateway (Aug 18 2022 at 10:14):From: Peter Lammich <peter.lammich@uni-muenster.de>
I want to prepare a pdf using isatool make, (with isabelle 2005)
isatool mkdir HOL MySession
isatool make
Everything ok up to now, some pdf has been created
cp somewhere/A.thy MySession/
echo 'use_thy "A";' >> MySession/ROOT.ML
Now A.thy should be in the session
isatool make
Now I get the output:
make: Für das Ziel »default« ist nichts zu tun.
in english: Nothing to do for target »default«
Also, if I do the first "isatool make" after I have added A.thy, and
then change A.thy later or add other theories, isatool make tells me
that there is nothing to do and does not regenerate anything.
What am I doing wrong ? Currently the only way I know to get something
regenerated is to brute-force do: rm -r ~/isabelle, and so delete every
intermediate info of "isatool make"
Thanks in advance for any hints
Peter Lammich
Email Gateway (Aug 18 2022 at 10:14):From: "Janney, Mark-P26816" <Mark.Janney@gdc4s.com>
One fix is to modify your IsaMakefile.
In that file you will find a dependency like this:
$(LOG)/HOL-MySession.gz: MySession/Root.ML # MySession/document/root.tex MySession/*.thy
Delete the '#' to make this target depend upon the .thy files in MySession. Then anytime you update these files, or add a new one, it will regenerate the PDF.
Alternatively run the command line:
isatool make clean; isatool make
This will force a rebuild of the PDF.
Email Gateway (Aug 18 2022 at 10:14):From: Michael Wahler <WAH@zurich.ibm.com>
I can't tell you what's going wrong, but I usually invoke
isatool make clean; isatool make
to rebuild the PDF.
Hope that helps,
Michael
IBM Zurich Research Lab. E-Mail: wah@zurich.ibm.com
Saeumerstr. 4 Notes: Michael Wahler/Zurich/IBM@IBMCH
CH-8803 Rueschlikon Phone: +41-44-724-8401
Switzerland Fax: +41-44-724-8953
Last updated: Nov 21 2024 at 12:39 UTC