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

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

should do the trick.

  -- Lars

Hi Lars, and thanks for your care,

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`).

I have not investigated this issue further, as I'm busy reading the `Imperative_HOL` theory source files for now.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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