Email Gateway (Aug 19 2022 at 14:20): Email Gateway (Aug 19 2022 at 14:20):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi,
I wanted to have a look at Simpl. I built it from a local AFP copy. In the
documentation, there is a section titled “User Guide” (I jumped there
nearly immediately). In this section, at “34.3.4 Recursion”, there is a
sample Fac imperative function.
If I type exactly what's exemplified there, I get an error about a type
unification failure. I have to change CALL into PROC in order to make
it work:
theory Test_Simpl
imports "$AFP/Simpl/Simpl"
begin
primrec fac :: "nat ⇒ nat"
where "fac 0 = 1"
| "fac (Suc n) = (Suc n) * (fac n)";
procedures Fac (N :: nat | R :: nat)
"IF ´N = 0 THEN ´R :== 1
ELSE ´R :== PROC Fac(´N - 1);; ´R :== ´N * ´R
FI";
end
If I write CALL instead of PROC (the user guide really says CALL), I
get this:
Type unification failed: Clash of types "⦇A_' :: nat,
B_' :: nat, C_' :: nat,
I_' :: nat, M_' :: nat,
N_' :: nat, R_' :: nat,
S_' :: nat, Arr_' :: nat list,
Abr_' :: char list,
… ::
_⦈" and "⦇locals :: _ ⇒ _,
… :: _⦈"
Type error in application: incompatible operand type
Operator: locals ::
(??'a, ??'b, ??'c, ??'d) stateSP_scheme
⇒ ??'b ⇒ ??'c
Operand: s :: (??'a, ??'e) XVcgEx.vars_scheme
I feel disturbed. First the documentation seems wrong, and then, the
documentation which was generated by a fresh build, should have failed if
there is an error somewhere. Or am I wrong? Do I have to report this as a
bug to the author?
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?
Email Gateway (Aug 19 2022 at 14:20):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Oops, my apologies. The imports was wrong. From the UserGuide.thy source
file, I changed it into the following, and it's OK with CALL:
imports
"$AFP/Simpl/HeapList"
"$AFP/Simpl/Vcg"
"~~/src/HOL/Statespace/StateSpaceSyntax"
"~~/src/HOL/Library/LaTeXsugar"
Email Gateway (Aug 19 2022 at 14:21):From: Lars Noschinski <noschinl@in.tum.de>
Just start from the Simpl session image, then you only have to wait once.
isabelle -d '$AFP' -l Simpl
should do the trick.
-- Lars
signature.asc
Email Gateway (Aug 19 2022 at 14:21):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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.
Email Gateway (Aug 19 2022 at 14:21):From: Lars Noschinski <noschinl@in.tum.de>
On 18.04.2014 22:07, Yannick Duchêne (Hibou57) wrote:
Le Fri, 18 Apr 2014 21:50:41 +0200, Lars Noschinski <noschinl@in.tum.de>
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-loption, 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
signature.asc
Email Gateway (Aug 19 2022 at 14:21):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
You're right, I checked it works (I initially did without -d, after a
thread on the StackOverflow forum). I will edit my Isabelle jEdit launcher
to always have this -d option, as it seems it does not disallow the use of
other heap images, like HOL.
Email Gateway (Aug 19 2022 at 14:21):From: Lars Noschinski <noschinl@in.tum.de>
You can also add the line
$AFP
to a file name ROOTS in $ISABELLE_HOME_USER (i.e. ~/.isabelle/ on Unix).
signature.asc
Email Gateway (Aug 19 2022 at 14:22):From: Makarius <makarius@sketis.net>
Using a ROOTS file in the proper place is indeed the standard way these
days, although that is little known.
Note that $ISABELLE_HOME_USER above only works for unnamed repository
versions. Luckily Isabelle/jEdit already knows $ISABELLE_HOME and
$ISABELLE_HOME_USER in the file browser, so these symbolic names are
univerally accepted (even on Windows in that notation).
Makarius
Email Gateway (Aug 19 2022 at 14:22):From: Lars Noschinski <noschinl@in.tum.de>
One thing that annoys me a little when I set this, is that I lose the
ability to say 'build everything in the distribution' (but not the AFP).
-- Lars
signature.asc
Email Gateway (Aug 19 2022 at 14:22):From: Makarius <makarius@sketis.net>
That is the deeper reason why the $AFP entry point is not imposed on users
by default, even with initialzed AFP component.
You don't have to include all of $AFP in ROOTS, but just the session root
directories you care about (with manually completed dependencies), e.g.
$AFP_BASE/thys/Simpl
Such entries may be also commented out with # in the ROOTS file, when they
are getting in the way at some point.
Makarius
Last updated: Nov 04 2025 at 08:30 UTC