Re: [isabelle] Issue with `Simpl` user guide `Fac` example

On 18.04.2014 22:07, Yannick Duchêne (Hibou57) wrote:
> Le Fri, 18 Apr 2014 21:50:41 +0200, Lars Noschinski <noschinl at>
> a écrit:
>> On 18.04.2014 03:22, Yannick Duchêne (Hibou57) wrote:
>>> Also, a question aside: is it mandatory to import `$AFP/Simpl/Simpl`? It
>>> takes long to load for me, near to ten minutes. Is there an alternative
>>> sufficient subset?
>> Just start from the Simpl session image, then you only have to wait once.
>>    isabelle -d '$AFP' -l Simpl

This should have been

      isabelle jedit -d '$AFP' -l Simpl
>> should do the trick.

> That's what I first did, I built an image, but it did not show up in the
> jEdit theories list and launching Isabelle from the command line with
> the `-l` option, thrown a dialogue complaining the cession was not
> found: “Undefined session(s): "Simpl"”. I've checked the heap image was
> built in the same directory as others (along with HOL, HOL-BNF and and
> al). As far as I can tell, Isabelle was properly configured for the use
> of the AFP (path specified in `~/.isabelle/etc/components`).

Since some time, the '-l' parameter does not specify a logic image
anymore, but a session. Even if you have the AFP configured as a
component, you need to pass "-d '$AFP'" to tell the session where the
Simpl session is found.

  -- Lars

Attachment: signature.asc
Description: OpenPGP digital signature

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