Re: [isabelle] Manual theory loading



On 29/06/18 11:46, Lars Hupel wrote:
>> I would expect both invocations to succeed. It becomes a problem when
>> there are two sessions, where one of them imports another one qualified.
> 
> To answer my own question: It doesn't work with "isabelle console", but
> it does work from Isabelle/Scala, by passing the "all_known = true" flag
> when computing the session base.

all_known = true is the default in "isabelle jedit", but it can be very
slow when AFP is included.

all_known = false in "isabelle console", for reasons of minimality, but
it can lead into situations where certain qualified theory names are
inaccessible.


Instead of "all_known" there is a more recent parameter to specify
"include_sessions" in Isabelle/Scala. I will add options to the above
command-line tools to add sessions selectively: see the emerging
Isabelle2018-RC1.


	Makarius




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