Email Gateway (Aug 23 2022 at 08:43): Email Gateway (Aug 23 2022 at 08:43):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Still somewhat lagging behind in testing Isabelle2020-RC2 -- going well so far, but there is one slightly odd thing that I noticed: the timing information at the end of a session build is printed twice for "build -v” (only once without “-v”).
E.g. with the AFP Word_Lib entry:
~/afp/devel$ isabelle build -bv -d . Word_Lib
Started at Fri Mar 20 20:50:32 GMT+8 2020 (polyml-5.8.1_x86_64_32-darwin on pluto)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86_64_32-darwin"
ML_HOME="/Users/kleing/.isabelle/contrib/polyml-5.8.1-20200228/x86_64_32-darwin"
ML_SYSTEM="polyml-5.8.1"
ML_OPTIONS="-H 2000"
Session Pure/Pure
Session FOL/FOL
Session Tools/Tools
Session HOL/HOL (main)
Session HOL/HOL-Library (main timing)
Session HOL/HOL-Computational_Algebra (main timing)
Session HOL/HOL-Analysis (main timing)
Session HOL/HOL-Eisbach
Session HOL/HOL-Word (main timing)
Session AFP/Word_Lib (AFP)
Building Word_Lib ...
Word_Lib: theory HOL-Eisbach.Eisbach
Word_Lib: theory HOL-Library.Sublist
Word_Lib: theory Word_Lib.Hex_Words
Word_Lib: theory Word_Lib.Signed_Words
Word_Lib: theory Word_Lib.Word_Type_Syntax
Word_Lib: theory Word_Lib.Enumeration
Word_Lib: theory Word_Lib.Norm_Words
Word_Lib: theory Word_Lib.WordBitwise_Signed
Word_Lib: theory Word_Lib.Word_Syntax
Word_Lib: theory HOL-Eisbach.Eisbach_Tools
Word_Lib: theory Word_Lib.HOL_Lemmas
Word_Lib: theory Word_Lib.More_Divides
Word_Lib: theory Word_Lib.Word_Lib
Word_Lib: theory Word_Lib.Word_Enum
Word_Lib: theory Word_Lib.Aligned
Word_Lib: theory Word_Lib.Word_Setup_32
Word_Lib: theory Word_Lib.Word_Setup_64
Word_Lib: theory Word_Lib.Word_Next
Word_Lib: theory Word_Lib.Word_EqI
Word_Lib: theory Word_Lib.Word_Lemmas
Word_Lib: theory Word_Lib.Word_Lemmas_32
Word_Lib: theory Word_Lib.Word_Lemmas_64
Timing Word_Lib (4 threads, 30.786s elapsed time, 82.532s cpu time, 4.802s GC time, factor 2.68)
Timing Word_Lib (4 threads, 30.786s elapsed time, 82.532s cpu time, 4.802s GC time, factor 2.68)
Finished Word_Lib (0:00:41 elapsed time, 0:01:42 cpu time, factor 2.45)
Finished at Fri Mar 20 20:51:24 GMT+8 2020
0:00:51 elapsed time, 0:01:42 cpu time, factor
Note the duplicate “Timing Word_Lib” line. There is also a noticeable time lag between the two lines being printed. Presumably this is roughly when polyml is dumping the image to disk, although I do not see significant CPU or disk activity in that time on a system monitor (the lag is significantly longer for larger sessions).
The line is printed only once in Isabelle2019. There probably is lag before it is printed there as well, but it is harder to tell because it’s unclear whether Isabelle is still busy with the last theory file or already (probably) constructing the disk image.
Cheers,
Gerwin
Email Gateway (Aug 23 2022 at 08:44):From: Makarius <makarius@sketis.net>
This is just an accident of too aggressive "debugging" that somehow got
committed: there is first a progress_stderr output and then a final err_lines,
when the process has terminated.
In https://isabelle.sketis.net/repos/isabelle-release/rev/f55222fbeae3 we are
back to the status-quo of Isabelle2019, i.e. no "Timing" for non-verbose mode,
and only one "Timing" for verbose mode.
Makarius
Email Gateway (Aug 23 2022 at 08:45):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Thanks, at least that was an easy one.
Cheers,
Gerwin
Last updated: Apr 24 2024 at 20:16 UTC