Re: [isabelle] Can't generate browser_info



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





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