Email Gateway (Aug 19 2022 at 11:58): Email Gateway (Aug 19 2022 at 11:58):From: Makarius <makarius@sketis.net>
First of all, as the author of Isabelle/Isar and Isabelle/ML, I claim the
natural authority to determine the name and title of the work.
I do care about such things, and spend a long time thinking and rethinking
what any of the Isabelle/XYZ aspects really are, and if they are used with
proper terminology. Complexity in the system and its concepts needs to be
kept in check. Sloppy or obsolete terminology does not help to understand
the true structure of the system, but prevents people discovering how the
system really works (and what great and still explored things may be done
with it).
When I read somethink like "on the ML level of Isabelle/HOL" or "to do
XYZ, I have to go down to the ML level" it sounds very strange and alien
to me, someone speaking about a different system, or a system from a
different era.
Isabelle/ML is not a cold and damp cellar where you go down occasionally
to poke around. Instead it is the main implementation and extension
language of Isabelle, which is fully integrated with the logical
environment and the Prover IDE. See also
https://www.lri.fr/~wenzel/Isabelle_Orleans_2012/slides.pdf how I explain
the languages of Isabelle these days to beginners. At Edinburgh this
spring, we even started with Isabelle/ML programming first, before doing
any Isabelle/HOL specifications or proofs, or showing how the Isabelle/HOL
code generator allows to go from Isabelle/HOL back to Isabelle/ML again.
Moreover Isabelle/ML is now the most advanced implementation of Standard
ML, with substantial IDE support, efficient parallel programming etc. It
just happens to ship with a massive theorem proving environment by
default, which is its main application. (At the bottom, all the hard work
is done by Poly/ML thanks to David Matthews.)
IIRC, the tentative term "ML level of Isabelle" came up when the main mass
of old-style ML tactic scripts were converted into "apply-scripts" in the
Isar source language. Of course, Isar is much more than a language for
non-ML proof scripts. You are a user from that pre-Isar era of Isabelle.
Are you still doing ML proof scripts these days?
Since you never got acquainted with Proof General, and its non-ML mode of
scripting, you should try now Isabelle/jEdit. It allows direct editing of
Isabelle sources (any of its many embedded languages) with direct feedback
in the editor, without the strange locking of the buffer due to Proof
General. Thus it is closer to old TTY mode, but you no longer have to
manage the prover state in your head as you type.
This is how Isabelle is exposed to the professional user today. And in
fact, what you see in the front is the jEdit editor framework that uses
Isabelle/Scala to access semantic content provided by the prover. So the
outermost "layer" of Isabelle2013 happens to be Isabelle/Scala, with
everything else in the background.
Note that the former expression "Isabelle/Scala layer" is no longer used,
since Isabelle/Scala can be accessed from Isabelle/ML already since
Isabelle2011-1, and I hope to get more interconnection of Isabelle/Scala
vs. Isabelle/ML, similar to the way other Isabelle languages may be
embedded into each other. If this is madness, there is method in it ...
Makarius
Email Gateway (Aug 19 2022 at 11:58):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
On 09/06/2013 10:49 PM, Makarius wrote:
IIRC, the tentative term "ML level of Isabelle" came up when the main
mass of old-style ML tactic scripts were converted into
"apply-scripts" in the Isar source language. Of course, Isar is much
more than a language for non-ML proof scripts. You are a user from
that pre-Isar era of Isabelle. Are you still doing ML proof scripts
these days?Yes - for the reasons I discussed in the email thread entitled Length of
Proofs, see eg
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-November/msg00167.html
The whole thread is rather long - but it includes my words
I think this email thread is getting too long - my first post was of
stuff that I asserted (and still do) that you can't imagine how to
do it sensibly other than in Standard ML.
Here's another example, from what I'm doing right now
fun ctxt_tac sg state =
(atac ORELSE' (resolve_tac (tl ctxt.intrs) THEN' ctxt_tac)) sg state ;
fun perm_msde_tac' sg = FIRST' [ etac keepFD, (* was atac *)
(resolve_tac [msde.seqs, msde_commas, msde_commas_rev]
THEN_ALL_NEW perm_msde_tac'),
rtac refl_msde',
eresolve_tac msde_commas_empty] sg ;
val perm_msde_tac = (REPEAT o ematch_tac [keepF_thin]) THEN'
perm_msde_tac' ;
In saying that no-one has made any suggestion as to how to do this other
than in Standard ML I should acknowledge that the suggestion has been
made that one can do this and wrap it up in Isar - but my experience -
as described in the email below made this a worst option
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2008-February/msg00007.html
(quote)
In fact I'm working on a project now where it is demanded that
everything is in Isar, so I have to try to work in this way. And it is
incredibly frustrating, because things seem to sometimes work, and
sometimes not, with no apparent reason, seemingly randomly.
Mostly my problems are something do to with theories. I don't know if
the problems I've faced today are because of theories or not, but I
think it is quite likely. But I waste an enormous amount of time trying
to cope with things that don't work as expected. What is a simple job
when I'm doing proofs using "the raw interactive ML toplevel" becomes
slow and frustrating when I try to use Isar as much as possible, while
using ML for the things not available in Isar.
(end quote)
Since you never got acquainted with Proof General, and its non-ML mode
of scripting, you should try now Isabelle/jEdit. It allows direct
editing of Isabelle sources (any of its many embedded languages) with
direct feedback in the editor, without the strange locking of the
buffer due to Proof General. Thus it is closer to old TTY mode, but
you no longer have to manage the prover state in your head as you type.Are you saying it Isabelle/jEdit works with ML files? Or with
Isabelle2005? I've read enough on this email list to doubt that very
much. And as I've mentioned in other messages the work I'm doing now
rests upon work I've done in the past. Unless I can mix theories and
proofs that work in Isabelle2005 with Isabelle2013 code then I can't use
Isabelle2013. It's as simple as that.
Incidentally you recently wrote "I am myself involved in Isabelle only
since 1993, but I've never seen a commitment to "backwards
compatibility"." If "commitment" means an absolute guarantee you may be
right, but there certainly was a time when developers cared about it -
see the reference to Asm_lr_simp_tac in the NEWS file
Jeremy
Email Gateway (Aug 19 2022 at 11:59):From: Makarius <makarius@sketis.net>
On Sat, 7 Sep 2013, Jeremy Dawson wrote:
Mostly my problems are something do to with theories. I don't know if
the problems I've faced today are because of theories or not, but I
think it is quite likely. But I waste an enormous amount of time trying
to cope with things that don't work as expected. What is a simple job
when I'm doing proofs using "the raw interactive ML toplevel" becomes
slow and frustrating when I try to use Isar as much as possible, while
using ML for the things not available in Isar.
This thread is again endangered to become a discussion about really
ancient Isabelle versions that hardly anybody will understand on the
isabelle-users mailing list in 2013.
When you say "theories" you probably mean the add-on feature of Isabelle93
to generate ML source from some concrete syntax of specifications. The
use_thy ML function was loading that into the ML session, then you would
continue with theorems and proofs in raw ML. (In 2013, use_thy is hardly
ever seen in practice, since isabelle build and isabelle jedit handle that
implicitly.)
Today, but starting already in 1998, everything is centered around
Isabelle theory files. It is very hard to escape from that, and there is
no point to do it, apart from extreme forms of nostalgy.
Are you saying it Isabelle/jEdit works with ML files?
Isabelle/jEdit mainly supports Isabelle theory files, where ML is
included. I recommend to use the Isar command 'ML' as a start, inside a
theory.
You can also use 'ML_file' in Isar, but the extern file will lack Prover
IDE markup, and is not integrated into the continous checking process at
the moment (you would have to initiate a reload a bit indirectly by hand,
by editing the ML_file command somehow).
Or with Isabelle2005?
Definitely not. Why are you still using Isabelle2005? Because it happens
to be the last Isabelle release with obsolete stuff from 10 years earlier?
And as I've mentioned in other messages the work I'm doing now rests
upon work I've done in the past. Unless I can mix theories and proofs
that work in Isabelle2005 with Isabelle2013 code then I can't use
Isabelle2013.
That is hopeless. The very idea of Isabelle as I know it since 1993 has
been to continously upgrade old things, such that everybody moves on. AFP
greatly helps to do that, already since 2003.
Incidentally you recently wrote "I am myself involved in Isabelle only
since 1993, but I've never seen a commitment to "backwards
compatibility"." If "commitment" means an absolute guarantee you may be
right, but there certainly was a time when developers cared about it -
see the reference to Asm_lr_simp_tac in the NEWS file
The amount of care has actually increased in recent years -- care about
getting forwards, and removing old things of no other value than history.
The example about Asm_lr_simp_tac merely tells that Stefan Berghofer
improved the Simplifier, then he found that the new scheme broke some very
old unstructured proof scripts (99 subgoals becoming 101), so he made a
workaround to preserve that old material. Getting rid of obsolete things
takes a lot of extra time, and one always needs to get at a realistic
balance what to do and what not.
If we would preserve old things by default, we could compete with
Sun/Oracle about cruft in the Java standard libraries, and that code base
is actually a bit younger than Isabelle.
Makarius
Email Gateway (Aug 19 2022 at 11:59):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
On 09/10/2013 10:37 PM, Makarius wrote:
On Sat, 7 Sep 2013, Jeremy Dawson wrote:
Mostly my problems are something do to with theories. I don't know
if the problems I've faced today are because of theories or not, but
I think it is quite likely. But I waste an enormous amount of time
trying to cope with things that don't work as expected. What is a
simple job when I'm doing proofs using "the raw interactive ML
toplevel" becomes slow and frustrating when I try to use Isar as much
as possible, while using ML for the things not available in Isar.This thread is again endangered to become a discussion about really
ancient Isabelle versions that hardly anybody will understand on the
isabelle-users mailing list in 2013.When you say "theories" you probably mean the add-on feature of
Isabelle93 to generate ML source from some concrete syntax of
specifications. The use_thy ML function was loading that into the ML
session, then you would continue with theorems and proofs in raw ML.
(In 2013, use_thy is hardly ever seen in practice, since isabelle
build and isabelle jedit handle that implicitly.)No, I meant theory as a concept (as returned by the function
theory_of_thm) - my understanding was that in Isar it keeps changing,
and that that was often the source of my problems. Whatever the reason,
though, I found that mixing ML and Isar, as a modus operandi, simply
didn't work.
Today, but starting already in 1998, everything is centered around
Isabelle theory files. It is very hard to escape from that, and there
is no point to do it, apart from extreme forms of nostalgy.
If "escape from that" includes using ML outside a theory file, my last
email just explained the point to it.Are you saying it Isabelle/jEdit works with ML files?
Isabelle/jEdit mainly supports Isabelle theory files, where ML is
included. I recommend to use the Isar command 'ML' as a start, inside
a theory.You can also use 'ML_file' in Isar, but the extern file will lack
Prover IDE markup, and is not integrated into the continous checking
process at the moment (you would have to initiate a reload a bit
indirectly by hand, by editing the ML_file command somehow).Or with Isabelle2005?
Definitely not. Why are you still using Isabelle2005? Because it
happens to be the last Isabelle release with obsolete stuff from 10
years earlier?Well there was certainly stuff in Isabelle2005 which wasn't in
Isabelle2007. I'm not sure what you mean by "obsolete" - I was using it
(and still do). I don't know how long it had been in Isabelle then.And as I've mentioned in other messages the work I'm doing now rests
upon work I've done in the past. Unless I can mix theories and
proofs that work in Isabelle2005 with Isabelle2013 code then I can't
use Isabelle2013.That is hopeless. The very idea of Isabelle as I know it since 1993
has been to continously upgrade old things, such that everybody moves
on. AFP greatly helps to do that, already since 2003.I was given to understand it doesn't take ML proofs.
Incidentally you recently wrote "I am myself involved in Isabelle
only since 1993, but I've never seen a commitment to "backwards
compatibility"." If "commitment" means an absolute guarantee you may
be right, but there certainly was a time when developers cared about
it - see the reference to Asm_lr_simp_tac in the NEWS fileThe amount of care has actually increased in recent years -- care
about getting forwards, and removing old things of no other value than
history.The example about Asm_lr_simp_tac merely tells that Stefan Berghofer
improved the Simplifier, then he found that the new scheme broke some
very old unstructured proof scripts (99 subgoals becoming 101), so he
made a workaround to preserve that old material. Getting rid of
obsolete things takes a lot of extra time, and one always needs to get
at a realistic balance what to do and what not.That's exactly what caring about backwards compatibility means -
recognising that something that is used in users' proofs has, for that
reason, value other than history.
If we would preserve old things by default, we could compete with
Sun/Oracle about cruft in the Java standard libraries, and that code
base is actually a bit younger than Isabelle.
I'm afraid I don't know Java, but the extent of the stability seen in C
or Standard ML standard libraries, while not absolute, would be a useful
comparison.
Regards,
Jeremy
Makarius
Email Gateway (Aug 19 2022 at 11:59):From: Makarius <makarius@sketis.net>
What you get via theory_of_thm is merely a certificate of the background
theory context of some derived entity. You should hardly ever access that
in your ML at all (the main exception is to use Thm.cterm_of or
Thm.ctyp_of to re-certify things according to a given certificate).
Historically, the theory of a theorem was at some point used as "the
context", e.g. for parsing or printing. That has long been replaced by an
explicit proof context of type Proof.context. If you don't have the
proper context around in your ML function that's bad luck: you must pass
it in as explicit argument. The system always provides you a proper
context where you need it, and you just pass on what you've got in the
canonical way.
When experimenting with the 'ML' command in Isar, you can use the
antiquotation @{context} to refer to the context of the ML compiler
invocation at that point. It is important to understand the distinction
between static compile-time and dynamic run-time, though. I.e. you should
not hardwire some @{context} into your Isabelle/ML, unless it is really
meant to stick to a particular context for later use with proof tools.
Makarius
Email Gateway (Aug 19 2022 at 11:59):From: Makarius <makarius@sketis.net>
I don't think there was a point, just historical reasons to have done
certain things a certain way at some point. It does not mean there is
never a way beyond accidental points in history.
All Isabelle/ML is inside some theory file, either directly via 'ML' or
indirectly via 'ML_file'. You are never outside.
Moreover, there are language elements like the Isar proof method called
"tactic" that allows to use Isabelle/ML expressions inside Isar proof
text.
Makarius
Email Gateway (Aug 19 2022 at 11:59):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Makarius wrote:
On Tue, 10 Sep 2013, Jeremy Dawson wrote:
Today, but starting already in 1998, everything is centered around
Isabelle theory files. It is very hard to escape from that, and
there is no point to do it, apart from extreme forms of nostalgy.
If "escape from that" includes using ML outside a theory file, my
last email just explained the point to it.I don't think there was a point, just historical reasons to have done
certain things a certain way at some point. It does not mean there is
never a way beyond accidental points in history.All Isabelle/ML is inside some theory file, either directly via 'ML'
or indirectly via 'ML_file'. You are never outside.What I am referring to is the use of ML as described in section 1.4
"Reading theories" of the reference manual (or at least, of the relevant
versions of it)
Jeremy
Moreover, there are language elements like the Isar proof method
called "tactic" that allows to use Isabelle/ML expressions inside Isar
proof text.Makarius
Email Gateway (Aug 19 2022 at 12:00):From: Makarius <makarius@sketis.net>
For several years already that manual with the internal identifier "ref"
has been called "Old Isabelle Reference Manual", with the following note
at the start:
Note: this document is part of the earlier Isabelle documentation and is
mostly outdated. Fully obsolete parts of the original text have already
been removed. The remaining material covers some aspects that did not
make it into the newer manuals yet.
Going back some years, e.g. to Isabelle2008 there is still a section 1.4,
but it is obsolete for quite a long time already. In Isabelle2013 that
section is already removed, and in the coming Isabelle2013-1 the whole
"ref" manual will no longer be there. (At last -- after 5 years of
refurbishing its content for the newer manuals, notably "isar-ref" and
"implementation".)
Makarius
Email Gateway (Aug 19 2022 at 12:00):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Makarius,
I'm sorry for the confusion, I thought it was apparent from my earlier
emails that I am using Isabelle2005
Cheers,
Jeremy
Makarius wrote:
Last updated: Nov 21 2024 at 12:39 UTC