Re: [isabelle-dev] unable to start Isabelle/jEdit due to error in unused session

[Makarius]

On 18/05/17 11:13, Christian Sternagel wrote:
> 
> I even read the email you are referring to, but apparently this was too
> long ago ;)
> 
> Anyway, what you suggest does in principle work (and shows that all the
> required functionality is already there). With
> 
>   isabelle jedit -R -l HOL
> 
> I end up in Isabelle/HOL's ROOT file and everything after Pure has to be
> loaded.

The option -R has another purpose: it reinterprets -l to refer to the
requirements of that session. It means you actually need to specify the
session that you are going to edit.

There is some extra complication behind -R and -l that might see more
refinement eventually, but it is probably better to move all that
session selection functionality into the IDE.


> I am curious, is there a reason why it would not be a good idea to
> restrict to Session by default whenever
> 
>   isabelle jedit -l Sessions
> 
> is invoked?

Some weeks ago I have started to move into the other direction. This is
all motivated by the session-qualified theory names reform, which has
been postponed several years already.

When that is fully active, it means that the PIDE can edit any source
file you like and know to which session it belongs.

Further fine points might still need polishing. I hope we manage that
during the summer, such that it all works smoothly for the Isabelle2017
release.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] unable to start Isabelle/jEdit due to error in unused session

[Christian Sternagel]

Thanks Lars!

I did not yet try your suggestion (and I am somewhat reluctant to
install "3rd party" software for something I would consider basic
functionality; but anyway, it's good to know that there is an alternative).

Thanks Makarius!

I even read the email you are referring to, but apparently this was too
long ago ;)

Anyway, what you suggest does in principle work (and shows that all the
required functionality is already there). With

  isabelle jedit -R -l HOL

I end up in Isabelle/HOL's ROOT file and everything after Pure has to be
loaded.

I am curious, is there a reason why it would not be a good idea to
restrict to Session by default whenever

  isabelle jedit -l Sessions

is invoked?

Alternatively, something similar to "-R" but where I do not end up in a
ROOT file and the specified session is already built (but none of its
descendants is checked) might be convenient.

cheers

chris

On 05/18/2017 10:34 AM, Makarius wrote:
> On 18/05/17 09:03, Christian Sternagel wrote:
>>
>> I was just about to have a look at the latest and greatest Isabelle (
>> f35abc25d7b1 ) when I noticed the following behavior.
>>
>> I started with
>>
>>   isabelle jedit -bf
>>
>> and then tried
>>
>>   isabelle jedit -l HOL
>>
>> but got an error message about missing files (see PS for details).
>>
>> Now, these missing files are only referenced in IsaFoR's ROOT file (and
>> the reason for the error is that IsaFoR is still running on
>> Isabelle2006-1), which is read since IsaFoR is registered as an Isabelle
>> component in my "etc/settings"
> 
> See
> http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg07321.html
> 
> Quote:
> 
> In current Isabelle/6acb28e5ba41 it is also possible to use something
> like "isabelle jedit -R -l MY_SESSION" to restrict the theory name space
> to the requirements of MY_SESSION.
> 
> 
>   Makarius
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] unable to start Isabelle/jEdit due to error in unused session

[Makarius]

On 18/05/17 09:03, Christian Sternagel wrote:
> 
> I was just about to have a look at the latest and greatest Isabelle (
> f35abc25d7b1 ) when I noticed the following behavior.
> 
> I started with
> 
>   isabelle jedit -bf
> 
> and then tried
> 
>   isabelle jedit -l HOL
> 
> but got an error message about missing files (see PS for details).
> 
> Now, these missing files are only referenced in IsaFoR's ROOT file (and
> the reason for the error is that IsaFoR is still running on
> Isabelle2006-1), which is read since IsaFoR is registered as an Isabelle
> component in my "etc/settings"

See
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg07321.html

Quote:

In current Isabelle/6acb28e5ba41 it is also possible to use something
like "isabelle jedit -R -l MY_SESSION" to restrict the theory name space
to the requirements of MY_SESSION.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] unable to start Isabelle/jEdit due to error in unused session

[Lars Hupel]

Dear Chris,

> 2) or there was some easy way (e.g., a flag) to exclude specific
> Isabelle components / sessions / ROOT files from checks (without having
> to edit "etc/settings").

I believe I have a solution for this problem.

For a while now, I've been using a custom Isabelle "launcher" based on
libisabelle [0]. It can be downloaded as a shell script [1]. It acts as
a wrapper for the regular Isabelle tool launcher. The twist is that it
supports on-the-fly registration of components.

In my setup, I've defined these two aliases:

alias isabelle='isabellectl --version 2016-1 --internal --afp --user
/home/lars exec'
alias isabelle-dev='isabellectl --devel --internal --component
/home/lars/work/afp --user /home/lars --home /home/lars/work/isabelle exec'

I can launch Isabelle by typing

$ isabelle jedit ...

or

$ isabelle-dev jedit ...

Note that additional arguments passed to the Isabelle tool need to be
separated by "--", as is standard practice in command-line environments:

$ isabelle-dev jedit -- -d . -l HOL-Library

But you can also pass in more components:

$ isabelle-dev --component /path/to/isafor jedit -- -l IsaFoR

Same thing works for using the stable version.

There are two caveats here:

- If you use the launcher for a stable Isabelle version, it'll download
a fresh copy to your home directory (Linux: "~/.local/share").
- The launcher claims control over your
"$ISABELLE_HOME_USER/etc/components" file. If you already have one, you
need to either delete it, or specify a different "--user" setting in the
alias.

This should work pretty much "out of the box" on Linux and OS X. No
guarantees on Windows.  You might also want to pass "--verbose" to get
informed about what is happening.

Cheers
Lars


[0] 
[1] 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] unable to start Isabelle/jEdit due to error in unused session

[Christian Sternagel]

Dear list,

I was just about to have a look at the latest and greatest Isabelle (
f35abc25d7b1 ) when I noticed the following behavior.

I started with

  isabelle jedit -bf

and then tried

  isabelle jedit -l HOL

but got an error message about missing files (see PS for details).

Now, these missing files are only referenced in IsaFoR's ROOT file (and
the reason for the error is that IsaFoR is still running on
Isabelle2006-1), which is read since IsaFoR is registered as an Isabelle
component in my "etc/settings"

I think it would be convenient if

1) sessions that are not ancestors of "-l Session" are not checked on
startup (or at least there was a way to activate this behavior),

2) or there was some easy way (e.g., a flag) to exclude specific
Isabelle components / sessions / ROOT files from checks (without having
to edit "etc/settings").

What do you think?

cheers

chris

PS: The exact error message was

/home/griff/repos/tools/isabelle/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
Cannot start:
*** No such file:
"/home/griff/repos/tools/isabelle/src/HOL/Library/Fraction_Field.thy"
*** The error(s) above occurred for theory "HOL-Lib.Fraction_Field"
(line 17 of "/home/griff/repos/isafor/thys/ROOT")
*** No such file:
"/home/griff/repos/tools/isabelle/src/HOL/Library/Fundamental_Theorem_Algebra.thy"
*** The error(s) above occurred for theory
"HOL-Lib.Fundamental_Theorem_Algebra" (line 18 of
"/home/griff/repos/isafor/thys/ROOT")
*** No such file:
"/home/griff/repos/tools/isabelle/src/HOL/Library/Polynomial_Factorial.thy"
*** The error(s) above occurred for theory
"HOL-Lib.Polynomial_Factorial" (line 29 of
"/home/griff/repos/isafor/thys/ROOT")
*** The error(s) above occurred in session "HOL-Lib" (line 1 of
"/home/griff/repos/isafor/thys/ROOT")
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev