Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Startup Error

view this post on Zulip Email Gateway (Aug 09 2022 at 15:33):

From: "M. Baksys" <mb2412@cam.ac.uk>
Hi everyone, recently I've been playing with the Isabelle ROOTS files and this
has in some way resulted in a startup error, which I can't seem to be able to
diagnose and fix. I am on a Windows machine and the error happens on every
startup; it reads:

Cannot start:
*** Bad session root directory (missing ROOT or ROOTS): "/cygdrive/c/Users/
baksy/.isabelle/Isabelle2021-1/ "
*** The error(s) above occurred in session catalog "/cygdrive/c/Users/
baksy/.isabelle/Isabelle2021-1/ROOTS"

I have looked into my ROOTS files and as far as I can tell, I have not
manually altered their contents. My ROOTS file in $ISABELLE_HOME has the
contents:

src/Pure
src/FOL
src/HOL
src/ZF
src/CCL
src/CTT
src/Cube
src/FOLP
src/LCF
src/Sequents
src/Doc
src/Tools

and the ROOTS file in $ISABELLE_HOME_USER has the contents:

Additional session root directories

# * each line contains one directory entry in Isabelle path notation, e.g.

# $ISABELLE_HOME/../AFP/thys

# for a copy of AFP put side-by-side to the Isabelle distribution

# * Isabelle/jEdit provides formal markup for C-hover-click and completion

# * lines starting with "#" are stripped

# * changes require restart of the Isabelle application

#:mode=text:encoding=UTF-8:

#$ISABELLE_HOME/../AFP/thys

Otherwise, I am not aware of other ROOT/ROOTS files which could be causing
this problem, so I am not quite sure what to try next. I have also tried
reinstalling Isabelle but with no success. I would be appreciative to hear any
suggestions on how to fix this error. Thanks!

Mantas Baksys

view this post on Zulip Email Gateway (Aug 09 2022 at 20:34):

From: Valentin Springsklee <uidpn@student.kit.edu>
Hi Mantas,

first of all, I encountered this error message when I was using a
current AFP version with an older Isabelle version. That being said, I
don't think the ISABELLE_HOME env variable should be set to the AFP
location. the AFP components must rather be included with the isabelle components -u $PATH_TO_COMPONENTS command https://www.isa-afp.org/help/
. I hope, I did not miss the point completely. I am not experienced with
the construction of ROOT files.

Best wishes

view this post on Zulip Email Gateway (Aug 09 2022 at 21:04):

From: Makarius <makarius@sketis.net>
I see some extra blanks here, after the final / and before the enclosing
double-quote.

Something odd must have happened somewhere in the (automatic) configuration of
$ISABELLE_HOME_USER

Makarius

view this post on Zulip Email Gateway (Aug 10 2022 at 12:41):

From: Makarius <makarius@sketis.net>
------- Forwarded Message --------
Subject: Re: [isabelle] Startup Error
Date: Wed, 10 Aug 2022 09:10:12 +0000
From: Mantas Baksys <mb2412@cam.ac.uk>
To: Makarius <makarius@sketis.net>

Dear Makarius,

Is there a way to reset this configuration? All was working fine out of the
box but now reinstalling Isabelle does not seem to change anything.

Mantas

From: Makarius <makarius@sketis.net>
Sent: 10 August 2022 00:04
To: Mantas Baksys <mb2412@cam.ac.uk>; cl-isabelle-users@lists.cam.ac.uk
<cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] Startup Error
On 09/08/2022 17:32, M. Baksys wrote:

Cannot start:
*** Bad session root directory (missing ROOT or ROOTS): "/cygdrive/c/Users/
baksy/.isabelle/Isabelle2021-1/                               "

I see some extra blanks here, after the final / and before the enclosing
double-quote.

Something odd must have happened somewhere in the (automatic) configuration of
$ISABELLE_HOME_USER

Makarius

view this post on Zulip Email Gateway (Aug 10 2022 at 12:41):

From: Makarius <makarius@sketis.net>
-------- Forwarded Message --------
Subject: Re: [isabelle] Startup Error
Date: Wed, 10 Aug 2022 12:07:49 +0200
From: Makarius <makarius@sketis.net>
To: Mantas Baksys <mb2412@cam.ac.uk>

From: Makarius <makarius@sketis.net>
On 09/08/2022 17:32, M. Baksys wrote:

Cannot start:
*** Bad session root directory (missing ROOT or ROOTS): "/cygdrive/c/Users/
baksy/.isabelle/Isabelle2021-1/ "

I see some extra blanks here, after the final / and before the enclosing
double-quote.

Something odd must have happened somewhere in the (automatic) configuration of
$ISABELLE_HOME_USER

On 10/08/2022 11:10, Mantas Baksys wrote:

Dear Makarius,

Is there a way to reset this configuration? All was working fine out of the
box but now reinstalling Isabelle does not seem to change anything.

I will try to make some guesses from a big distance.

The overall Isabelle state is defined by the directory contents of
$ISABELLE_HOME (normally static and unchanged) and $ISABELLE_HOME_USER
(dynamic). The path notation is that of Cygwin, if you want native Windows you
can use "cygpath -w".

To get some ideas, can you run the following in the Cygwin-Terminal.bat within
a fresh Isabelle2021-1 installation?

isabelle env bash
echo "_${ISABELLE_HOME}_"
echo "_${ISABELLE_HOME_USER}_"
echo "_${USER_HOME}_"
echo "_${HOME}_"
echo "_${USERPROFILE}_"

My results are as follows (the underscores help to see spurious blanks):

_/cygdrive/d/wenzelm/Isabelle2021-1_
_/cygdrive/c/Users/wenzelm/.isabelle/Isabelle2021-1_
_/cygdrive/c/Users/wenzelm_
_/home/wenzelm_
_C:\Users\wenzelm_

Makarius

view this post on Zulip Email Gateway (Aug 10 2022 at 12:42):

From: Makarius <makarius@sketis.net>
-------- Forwarded Message --------
Subject: Re: [isabelle] Startup Error
Date: Wed, 10 Aug 2022 10:13:23 +0000
From: Mantas Baksys <mb2412@cam.ac.uk>
To: Makarius <makarius@sketis.net>

Dear Makarius,

I've just run the commands you suggested, and my results are:

_/cygdrive/c/Users/baksy/Isabelle2021-1_
_/cygdrive/c/Users/baksy/.isabelle/Isabelle2021-1_
_/cygdrive/c/Users/baksy_
_/cygdrive/c/Users/baksy_
_C:\Users\baksy_

So only the 4th one seems different to the ones you've posted.

Mantas

From: Makarius <makarius@sketis.net>
Sent: 10 August 2022 13:07
To: Mantas Baksys <mb2412@cam.ac.uk>
Subject: Re: [isabelle] Startup Error

From: Makarius <makarius@sketis.net>

On 09/08/2022 17:32, M. Baksys wrote:
 >>
 >> Cannot start:
 >> *** Bad session root directory (missing ROOT or ROOTS): "/cygdrive/c/Users/
 >> baksy/.isabelle/Isabelle2021-1/                               "

> I see some extra blanks here, after the final / and before the enclosing
 > double-quote.

> Something odd must have happened somewhere in the (automatic)
configuration of
 > $ISABELLE_HOME_USER

On 10/08/2022 11:10, Mantas Baksys wrote:

Dear Makarius,

Is there a way to reset this configuration? All was working fine out of the
box but now reinstalling Isabelle does not seem to change anything.

I will try to make some guesses from a big distance.

The overall Isabelle state is defined by the directory contents of
$ISABELLE_HOME (normally static and unchanged) and $ISABELLE_HOME_USER
(dynamic). The path notation is that of Cygwin, if you want native Windows you
can use "cygpath -w".

To get some ideas, can you run the following in the Cygwin-Terminal.bat within
a fresh Isabelle2021-1 installation?

isabelle env bash
   echo "_${ISABELLE_HOME}_"
   echo "_${ISABELLE_HOME_USER}_"
   echo "_${USER_HOME}_"
   echo "_${HOME}_"
   echo "_${USERPROFILE}_"

My results are as follows (the underscores help to see spurious blanks):

_/cygdrive/d/wenzelm/Isabelle2021-1_
_/cygdrive/c/Users/wenzelm/.isabelle/Isabelle2021-1_
_/cygdrive/c/Users/wenzelm_
_/home/wenzelm_
_C:\Users\wenzelm_

Makarius

view this post on Zulip Email Gateway (Aug 10 2022 at 12:45):

From: Makarius <makarius@sketis.net>
This looks fine, in particular there are no funny extra blanks. I wonder why
we saw them beforehand.

I suggest to purge C:\Users\baksy/Isabelle2021-1 and
C:\Users\baksy/.isabelle\Isabelle2021-1 and run the installer
Isabelle2021-1.exe again.

Thus all persistent state should be back to defaults.

Makarius

Last updated: Jan 04 2025 at 20:18 UTC