[isabelle-dev] isabelle-dev and ML files
makarius at sketis.net
Fri Oct 23 16:32:45 CEST 2009
On Fri, 23 Oct 2009, Timothy Bourke wrote:
> I'm having some trouble working with ML files in recent dev versions.
> Given, for example, a file test.ML:
> structure Test =
> val s1 = "\<top>";
> val s2 = "\\<top>";
> And two tests:
> ML) Direct ML: isabelle-process < test.ML
> USE) Interactive isabelle: use "test.ML";
> I get the following results for Isabelle 2009 and a recent (yesterday)
> dev version:
> \ version
> test \ 2009 dev
> ML | s1 fails | s1 fails |
> | s2 works | s2 works |
> USE | s1 works | s1 works |
> | s2 works | s2 fails |
> Is the dev behaviour correct?
Shouldn't the status of s1 and s2 be swapped in ML/dev?
Which version are you using anyway? In the face of non-linear distributed
history with time-jumps, only the offical changeset id counts, e.g.
fe29679cabc2 in my case ("hg id" helps to figure this out).
The 'ML' and 'use' commands operate exactly the same way, and invoking the
"use" function from the raw ML toplevel should coincide with that. All of
this treats Isabelle symbols as native content of the ML sources, so there
is no longer that extra escaping (this oddity was occasionally causing
confusion in the past, and had to dissappear altogether when precise
counting of source positions was introduced.)
This means that ML sources with Isabelle symbols cannot be pasted into the
raw ML loop. In practive you need a proper context anyway (for
antiquotations etc.) so it is best to work trough Isar/ML all the time,
unless you do really low-level work on the ML system itself.
More information about the isabelle-dev