Email Gateway (Aug 19 2022 at 12:43): Email Gateway (Aug 19 2022 at 12:43):From: Alfio Martini <alfio.martini@acm.org>
Dear Users,
I am having repeatedly problems when running build for
document preparation in Isabelle 2013-1 for Windows.
The program seems not to detect
that I have made (several) editions in the corresponding
.thy file(s) and it process the session by doing "nothing".
$ isabelle build -v -D WeitSession
Started at 27 Nov 2013 10:39:13 (polyml-5.5.1_x86-cygwin on isabelle)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86-cygwin"
ML_HOME="/cygdrive/c/Users/Alfio/Isabelle2013-1/contrib/polyml-5.5.1-1/x86-cygwi
n"
ML_SYSTEM="polyml-5.5.1"
ML_OPTIONS="-H 500"
Session Pure/Pure
Session HOL/HOL (main)
Session Unsorted/WeitSession
Finished at 27 Nov 2013 10:39:30
0:00:17 elapsed time, 0:00:00 cpu time
So, to avoid this, I kind of fake a change in the root.tex file so it
can properly process the entire set of documents:
Started at 27 Nov 2013 10:43:42 (polyml-5.5.1_x86-cygwin on isabelle)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86-cygwin"
ML_HOME="/cygdrive/c/Users/Alfio/Isabelle2013-1/contrib/polyml-5.5.1-1/x86-cygwi
n"
ML_SYSTEM="polyml-5.5.1"
ML_OPTIONS="-H 500"
Session Pure/Pure
Session HOL/HOL (main)
Session Unsorted/WeitSession
Running WeitSession ...
WeitSession: theory weitPaper
Timing WeitSession (4 threads, 6.041s elapsed time, 8.234s cpu time, 0.375s
GC t
ime, factor 1.36)
Document at
/cygdrive/c/Users/Alfio/Documents/LaTeX/WEIT2013/WeitPaper/WeitSessi
on/output/document.pdf
Finished WeitSession (0:00:35 elapsed time, 0:00:25 cpu time, factor 0.71)
Finished at 27 Nov 2013 10:44:30
0:00:48 elapsed time, 0:00:00 cpu time
Thanks in advance for any enlightenment on this.
Best!
Email Gateway (Aug 19 2022 at 12:43):From: Alfio Martini <alfio.martini@acm.org>
Since my primitive solution mentioned bellow does not to seem to always to
work, I found the following
workaround: force cleaning before running the session again
isabelle build -v -c -D Session
Was this (cleaning) expected to be done (like in the old times of "make
clean" before rerunning the session?
Best!
---------- Forwarded message ----------
From: Alfio Martini <alfio.martini@acm.org>
Date: Wed, Nov 27, 2013 at 10:51 AM
Subject: Isabelle "Identity" Build Sessions
To: isabelle-users <isabelle-users@cl.cam.ac.uk>
Dear Users,
I am having repeatedly problems when running build for
document preparation in Isabelle 2013-1 for Windows.
The program seems not to detect
that I have made (several) editions in the corresponding
.thy file(s) and it process the session by doing "nothing".
$ isabelle build -v -D WeitSession
Started at 27 Nov 2013 10:39:13 (polyml-5.5.1_x86-cygwin on isabelle)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86-cygwin"
ML_HOME="/cygdrive/c/Users/Alfio/Isabelle2013-1/contrib/polyml-5.5.1-1/x86-cygwi
n"
ML_SYSTEM="polyml-5.5.1"
ML_OPTIONS="-H 500"
Session Pure/Pure
Session HOL/HOL (main)
Session Unsorted/WeitSession
Finished at 27 Nov 2013 10:39:30
0:00:17 elapsed time, 0:00:00 cpu time
So, to avoid this, I kind of fake a change in the root.tex file so it
can properly process the entire set of documents:
Started at 27 Nov 2013 10:43:42 (polyml-5.5.1_x86-cygwin on isabelle)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86-cygwin"
ML_HOME="/cygdrive/c/Users/Alfio/Isabelle2013-1/contrib/polyml-5.5.1-1/x86-cygwi
n"
ML_SYSTEM="polyml-5.5.1"
ML_OPTIONS="-H 500"
Session Pure/Pure
Session HOL/HOL (main)
Session Unsorted/WeitSession
Running WeitSession ...
WeitSession: theory weitPaper
Timing WeitSession (4 threads, 6.041s elapsed time, 8.234s cpu time, 0.375s
GC t
ime, factor 1.36)
Document at
/cygdrive/c/Users/Alfio/Documents/LaTeX/WEIT2013/WeitPaper/WeitSessi
on/output/document.pdf
Finished WeitSession (0:00:35 elapsed time, 0:00:25 cpu time, factor 0.71)
Finished at 27 Nov 2013 10:44:30
0:00:48 elapsed time, 0:00:00 cpu time
Thanks in advance for any enlightenment on this.
Best!
--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
www.inf.pucrs.br/alfio
Lattes: http://lattes.cnpq.br/4016080665372277
Associate Professor at Faculty of Informatics (PUCRS)
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
www.inf.pucrs.br/alfio
Lattes: http://lattes.cnpq.br/4016080665372277
Associate Professor at Faculty of Informatics (PUCRS)
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
Email Gateway (Aug 19 2022 at 12:43):From: Makarius <makarius@sketis.net>
Yes, build option -c is the standard way to enforce a clean build.
In any case you should make sure that all add-on tex files are declared in
the 'files' section of the ROOT file -- this is not checked by the system,
and thus reminiscent of the old IsaMakefiles.
The build system also takes changes of the ROOT specification and its
options into account, but not changes of command line options. If you have
run a session already without document or browser_info, but want it now
with -o document=pdf -o browser_info you need to add -c to the command
line to make double-sure.
In some sense, the connection of batch builds with document preparation is
just a historical accident. I would like to see this eventually as part
of the Prover IDE, without funny command line tools to be re-iterated all
the time.
Makarius
Email Gateway (Aug 19 2022 at 12:43):From: Alfio Martini <alfio.martini@acm.org>
In any case you should make sure that all add-on tex files are declared in
the 'files' section of the ROOT file -- this is not checked by the >system,
and thus reminiscent of the old IsaMakefiles.
I have not done that and this might have caused the problem. But the -c
option does the job nicely enough.
best!
Last updated: May 06 2024 at 16:21 UTC