Email Gateway (Aug 19 2022 at 13:23): Email Gateway (Aug 19 2022 at 13:23):From: Walther Neuper <wneuper@ist.tugraz.at>
Hi,
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.
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"
And I am surprised to see the same message first time for another
version (a distribution without "~~/Admin" etc):
Bad component catalog file:
"/usr/local/Isabelle2013-1/Admin/components/main"
Strange, I never saw cross connections between Isabelle versions before.
What is happening here ?
Walther
Email Gateway (Aug 19 2022 at 13:23):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 13:24):From: Walther Neuper <wneuper@ist.tugraz.at>
On 01/29/2014 02:27 PM, Makarius wrote:
On Wed, 29 Jan 2014, Walther Neuper wrote:
[..] 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.
Your guess is right, thank you!
I had not noticed a devious mouse click of mine.
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.
That is a good idea!
In my workflow the <Theories> window is frequently closed in favour of
<Sidekick>, thus the respective checkbox invisible.
Walther
Last updated: Apr 26 2024 at 08:19 UTC