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
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 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and