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 or

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


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,,

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.


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