Re: [isabelle] Bad component catalog file



On Wed, 29 Jan 2014, Walther Neuper wrote:

At a restart by "./bin/isabelle jedit -l HOL &" during work as usual in the repository (i.e. there are "~~/Admin" etc), suddenly Isabelle stopped evaluation of the code:

The editor window shows light-pink background colour for the lines, so does the <Theories> Window; no messages on the command line.

I guess you merely have switched off "Continuous checking" in the Theories panel or Plugin Options / Isabelle. This is persistent in the preferences, so the usual reflex to restart the application does not help. I am sometimes stumbling myself over this snag. Continuous checking off should probably show a flashing icon somewhere to make sure the user sees that off-line state of the system.


On my machine there are several Isabelle versions installed.

Switching to a _fresh_ download of Isabelle2013-2, "Isabelle2013-2$ ./bin/isabelle jedit -l HOL &" causes the error message:

Bad component catalog file: "/usr/local/Isabelle2013-2/Admin/components/main"

Here I guess that you have applied instructions from README_REPOSITORY to a proper release, to insert some init_components line into $ISABELLE_HOME_USER/etc/settigs that does not make sense in this situation.


Some general notes on "work as usual with the repository":

  * Isabelle Professional Edition (aka the current official release) is
    the normal way to do productive work.  It is shipped with everything
    on-board, and hides a lot of complexity of system integration and
    consolidation.

  * Early adopters of arbitrary Isabelle repository clones need to
    understand more technicalities, and the semantic difference to a
    proper release (even though the younger generations no longer grasp
    the purpose of "stable software releases").

You need to have extra time and/or good reasons to engage in repository versions at all. It is not a magic way to get new features earlier than other users, but a way to participate in the ongoing development process towards the next official release.

Discussing particular repository versions only makes sense in conjunction with the relevant changeset ids, and the isabelle-dev mailing list is the place for that.


	Makarius




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