Email Gateway (Aug 19 2022 at 10:12): Email Gateway (Aug 19 2022 at 10:12):From: Alessandro Coglio <coglio@kestrel.edu>
Hello,
I've just installed Isabelle 2013 on my Mac and I'd like to generate theory
browsing information for the library.
Following page 28 of the system manual, I tried
isabelle build -o browser_info -v -c HOL
but I get
Started at Thu Feb 14 17:59:37 PST 2013 (polyml-5.5.0_x86-darwin on
HAL9000.local)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86-darwin"
ML_HOME="/Applications/Isabelle2013.app/Contents/Resources/Isabelle2013/contrib/polyml-5.5.0-3/x86-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="-H 500"
Session Pure
Session HOL (main)
Finished at Thu Feb 14 17:59:40 PST 2013
0:00:03 elapsed time, 0:00:04 cpu time
and nothing under ~/.isabelle/Isabelle2013/browser_info/HOL.
The second line of the output suggests that '-o browser_info' may not make it
to the build options.
Any idea of what could be wrong?
Thank you in advance!
smime.p7s
Email Gateway (Aug 19 2022 at 10:12):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Alessandro,
On 02/15/2013 11:06 AM, Alessandro Coglio wrote:
Following page 28 of the system manual, I tried
isabelle build -o browser_info -v -c HOL
but I get
Started at Thu Feb 14 17:59:37 PST 2013 (polyml-5.5.0_x86-darwin on
HAL9000.local)
ISABELLE_BUILD_OPTIONS=""
Just to clarify: these are the default build options that should always
be added when calling "isabelle build" (you can set them in your
~/.isabelle/etc/settings). However, they are not related to what you
wrote on the command line above. Sorry, that doesn't answer your actual
question.
ML_PLATFORM="x86-darwin"
ML_HOME="/Applications/Isabelle2013.app/Contents/Resources/Isabelle2013/contrib/polyml-5.5.0-3/x86-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="-H 500"Session Pure
Session HOL (main)
Just to make sure that everything is the same as on my machine. At this
point there are many lines of output starting with
Cleaning HOL ...
Cleaning HOLCF ...
Running HOL ...
HOL: theory Code_Generator
HOL: theory HOL
HOL: theory Orderings
right? If not, it seems the "-c" flag did not work properly.
Finished at Thu Feb 14 17:59:40 PST 2013
0:00:03 elapsed time, 0:00:04 cpu time
On my machine the whole output ends with
Timing HOL (4 threads, 95.510s elapsed time, 261.987s cpu time, 22.639s
GC time, factor 2.74)
Browser info at /home/griff/.isabelle/Isabelle2013/browser_info/HOL
Finished HOL (0:01:36 elapsed time, 0:04:22 cpu time, factor 2.72)
Finished at Fri Feb 15 12:14:16 JST 2013
0:01:40 elapsed time, 0:04:27 cpu time, factor 2.67
which indicates where browser_info was written. (And it was indeed written.)
Still, no real answer, but again, it seems that "-c" did not work properly.
cheers
chris
Email Gateway (Aug 19 2022 at 10:12):From: Makarius <makarius@sketis.net>
On Thu, 14 Feb 2013, Alessandro Coglio wrote:
I've just installed Isabelle 2013 on my Mac and I'd like to generate theory
browsing information for the library.
If you just want to get the generated browser_info you can get it from
http://isabelle.in.tum.de/dist/library/index.html or
http://isabelle.in.tum.de/dist/Isabelle2013_library.tar.gz
Following page 28 of the system manual, I tried
isabelle build -o browser_info -v -c HOL
but I get
Started at Thu Feb 14 17:59:37 PST 2013 (polyml-5.5.0_x86-darwin on
HAL9000.local)
ISABELLE_BUILD_OPTIONS=""ML_PLATFORM="x86-darwin"
ML_HOME="/Applications/Isabelle2013.app/Contents/Resources/Isabelle2013/con
trib/polyml-5.5.0-3/x86-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="-H 500"Session Pure
Session HOL (main)
Finished at Thu Feb 14 17:59:40 PST 2013
0:00:03 elapsed time, 0:00:04 cpu time
Here the build system did not change anything, because the sessions were
considered to be up-to-date.
This potential for confusion is due to build option -s "system mode" that
is hardwired into the auto-build wrappers for the main Isabelle2013 entry
points: Isabelle2013/Isabelle, Isabelle2013.app, Isabelle2013.app.
Thus the pre-built HOL image ends up in the belly of the Isabelle
distribution (ISABELLE_HOME). Working on it later without option -s will
not update that again, but refer to ISABELLE_HOME_USER as output, while
using ISABELLE_HOME as fall-back for input.
When composing the distribution I was occasionally hesitating about
exactly these two build modes. It would be better to have just one mode.
Makarius
Last updated: Apr 30 2024 at 16:19 UTC