Email Gateway (Aug 22 2022 at 17:48): Email Gateway (Aug 22 2022 at 17:48):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi,
if I have a file called test (simplified for the purposes of this
email), containing
length (String.explode ("Meta_Language.\\")) ;
length (String.explode ("Meta_Language.\\<M>_type.Type")) ;
and I type use "test" into the console process
(ie, isabelle console)
it gives the following error (relating to the second of the two
non-empty lines above)
SML lexical error: bad escape character in string (line 6 of "test") at
\<M>_type.Typ ...
On the other hand, if I paste those lines into the console process, they
work fine,
What is happening here?
Cheers,
Jeremy
Email Gateway (Aug 22 2022 at 17:48):From: Makarius <makarius@sketis.net>
See again the "implementation" manual, about text and Isabelle symbols.
In Isabelle/ML you should hardly ever use Char and String operations
from SML'97, they are semantically wrong and cause unexpected behaviour.
Makarius
Email Gateway (Aug 22 2022 at 17:49):From: Makarius <makarius@sketis.net>
See specifically "implementation", sections 0.6, 0.7.1, 0.7.2, and note
that "isabelle console" and "isabelle process" don't give you an
Isabelle/ML toplevel, only the raw Poly/ML bootstrap environment.
Normally you use the latter only to invoke things in a proper Isabelle
context, say via use_thy with Isabelle/ML inside it.
The most relevant operation on Isabelle symbol strings is Symbol.explode.
Side-remark: if you want to work with embedded languages in Isabelle,
the cartouche notation provides more flexibility. It corresponds to type
Input.source with main operation Input.explode_source, e.g.
ML ‹val inp = Input.source_explode ‹abcαβγ›;›
This gives you Isabelle symbols with precise position information. You
can use that with Isabelle scanner combinators to build a parser that
works with the Prover IDE, e.g. see ~~/src/Pure/Tools/rail.ML
People attending FLoC 2018 at Oxford can hear more about this at my talk
on Saturday, at the F-IDE workshop (Formal IDE).
Makarius
Email Gateway (Aug 22 2022 at 17:49):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Well, thanks - I gather from all of this that
val s = "\\<M>" ;
String.explode s ;
Symbol.explode s ;
the string s is treated as a single symbol in Isabelle.
However in the sections you quote I don't find anything to explain why I
can enter the text above into the console, but when the above code is
put into a file which I then use, it causes an error.
Incidentally, re your remark about "isabelle console", there used to be
Isar.loop () which would get you into an Isar parser - what has happened
to that? Is there an equivalent to that now?
Regards,
Jeremy
Email Gateway (Aug 22 2022 at 17:49):From: Makarius <makarius@sketis.net>
On 11.07.2018 02:45, Jeremy Dawson wrote:
Well, thanks - I gather from all of this that
val s = "\\<M>" ;
String.explode s ;
Symbol.explode s ;the string s is treated as a single symbol in Isabelle.
However in the sections you quote I don't find anything to explain why I
can enter the text above into the console, but when the above code is
put into a file which I then use, it causes an error.
This is due to a subtle difference (explained in the manual) how
Isabelle treats text, with its own notation for infinitely many symbol.
This also applies to Isabelle/ML as one of the many sublanguages of
Isabelle.
On the "isabelle console" you get the raw SML environment of Poly/ML,
but Isabelle/ML is not SML. It is better to avoid that -- you only need
it for rare invocations of use_thy in exotic debugging situations.
Normal Isabelle/ML development happens always in the Prover IDE -- it
saves a lot of time.
Incidentally, re your remark about "isabelle console", there used to be
Isar.loop () which would get you into an Isar parser - what has happened
to that? Is there an equivalent to that now?
Isar.loop has become a historic footnote, see the blog entry from
31-Oct-2014:
https://sketis.net/2014/discontinuation-of-isabelle-proof-general
There is no equivalent of it left: it has been superseded by the PIDE
document model in all respects.
If you need quasi-command-line access to PIDE, you can use the new
Isabelle server of Isabelle2018, see the blob entry
https://sketis.net/2018/the-isabelle-server-responsive-control-of-prover-sessions
Note that this is mainly relevant for accessing Isabelle from other
programs, alternative front-ends etc.
Makarius
Email Gateway (Aug 22 2022 at 17:50):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
On 07/12/2018 08:13 AM, Makarius wrote:
On 11.07.2018 02:45, Jeremy Dawson wrote:
Well, thanks - I gather from all of this that
val s = "\\<M>" ;
String.explode s ;
Symbol.explode s ;the string s is treated as a single symbol in Isabelle.
However in the sections you quote I don't find anything to explain why I
can enter the text above into the console, but when the above code is
put into a file which I then use, it causes an error.This is due to a subtle difference (explained in the manual) how
Isabelle treats text, with its own notation for infinitely many symbol.
This also applies to Isabelle/ML as one of the many sublanguages of
Isabelle.Hi Makarius,
Which bit of the manual, exactly, explains this?
I understand that it treats \<M> as a single symbol, but here we have
that it is simply rejected. I don't see any explanation of that.
Cheers,
Jeremy
On the "isabelle console" you get the raw SML environment of Poly/ML,
but Isabelle/ML is not SML. It is better to avoid that -- you only need
it for rare invocations of use_thy in exotic debugging situations.Normal Isabelle/ML development happens always in the Prover IDE -- it
saves a lot of time.Incidentally, re your remark about "isabelle console", there used to be
Isar.loop () which would get you into an Isar parser - what has happened
to that? Is there an equivalent to that now?Isar.loop has become a historic footnote, see the blog entry from
31-Oct-2014:
https://sketis.net/2014/discontinuation-of-isabelle-proof-generalThere is no equivalent of it left: it has been superseded by the PIDE
document model in all respects.If you need quasi-command-line access to PIDE, you can use the new
Isabelle server of Isabelle2018, see the blob entry
https://sketis.net/2018/the-isabelle-server-responsive-control-of-prover-sessionsNote that this is mainly relevant for accessing Isabelle from other
programs, alternative front-ends etc.Makarius
Email Gateway (Aug 22 2022 at 17:50):From: Makarius <makarius@sketis.net>
The normal Isabelle text representation of lists of symbols means that
\\<M> is a backslash followed by \<M> but that is not a valid escape
sequence for ML string-literals.
In contrast, the raw Standard ML toplevel loop of "isabelle console"
treats it as escaped backslash followed by < M > characters.
Normally you can work uniformly with the Isabelle symbol text view, and
there is no need to refer to the raw toplevel loop, apart from invoking
something like use_thy from there.
Makarius
Last updated: Apr 25 2024 at 08:20 UTC