[isabelle] Fwd: Isabelle "Identity" Build Sessions



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 at acm.org>
Date: Wed, Nov 27, 2013 at 10:51 AM
Subject: Isabelle "Identity" Build Sessions
To: isabelle-users <isabelle-users at 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



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