Email Gateway (Aug 18 2022 at 11:14): Email Gateway (Aug 18 2022 at 11:14):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Using Isabelle2007, and doing
use_thy "MSA"
this seems to work but when I've done it I get the following behaviour,
which I've never noticed before:
the_context () refers to an ancestor theory, not to MSA
theory "MSA" ;
gives the following error message:
Exception- ERROR "Theory loader: undefined theory entry for \"MSA\"" raised
Note - at the stage of loading MSA.ML, I also got the message
*** Theory loader: unresolved dependencies of theory "MSA" on file(s):
"SatEx1_mk.ML"
because "SatEx1_mk.ML" was a file that I had "use"d before reloading MSA.
What is happening here?
Jeremy
Email Gateway (Aug 18 2022 at 11:14):From: Stefan Berghofer <berghofe@in.tum.de>
Jeremy Dawson wrote:
Hi Jeremy,
this error probably occurs because you have declared in the theory header that
MSA depends on "SatEx1_mk.ML", e.g. by writing
theory MSA
imports ...
uses
("SatEx1_mk.ML")
...
begin
but there is no corresponding "use" command in the theory that actually loads
"SatEx1_mk.ML". To fix this, you can either add the missing "use" command,
or remove the parentheses around "SatEx1_mk.ML", i.e. write
theory MSA
imports ...
uses
"SatEx1_mk.ML"
...
begin
This causes "SatEx1_mk.ML" to be loaded immediately at the beginning of the
theory. Note that this option might not be possible if "SatEx1_mk.ML" depends
on theorems or constants introduced later in MSA.
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 11:15):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Florian Haftmann wrote:
Dear Jeremy,
Using Isabelle2007, and doing
use_thy "MSA"
this seems to work but when I've done it I get the following behaviour,
which I've never noticed before:the_context () refers to an ancestor theory, not to MSA
theory "MSA" ;
gives the following error message:
Exception- ERROR "Theory loader: undefined theory entry for \"MSA\"" raised
you should use the ML antiquotation
@{theory}
which binds the theory context statically. "the_context ()" is
evaluated dynamically and may return unexpected results.Dear Florian and Stefan,
thanks for your replies. But I find that these ML antiquotations are
fine when
they are in a theory file or ML file which I load, but don't work when
I'm entering
code at the keyboard, which I do when I am developing complex procedures.
(for that matter, when I'm entering code at the keyboard, presumably
there is no difference between static and dynamic - or have I
misunderstood these terms?)
Note - at the stage of loading MSA.ML, I also got the message
*** Theory loader: unresolved dependencies of theory "MSA" on file(s):
"SatEx1_mk.ML"because "SatEx1_mk.ML" was a file that I had "use"d before reloading MSA.
What is happening here?
Dependencies of theory files on ML files should be declared explicitly
in the theory header:theory MSA
imports ...
uses ("SatEx1_mk.ML")
begin...
use "SatEx1_mk.ML"
end
Hope this helps,
FlorianThe theory MSA doesn't depend in the file SatEx1_mk.ML, rather the other
way around:
"SatEx1_mk.ML" contains code I want to run in the context of the theory MSA
As Stefan's email suggests, if I put
uses
"SatEx1_mk.ML" into the theory file, then it doesn't work if I
don't have a
corresponding "use" command in the theory to load "SatEx1_mk.ML"
So, given that I want to load the theory MSA, and then, subsequently,
sometimes, maybe,
use a file containing some ML procedure, how should I do this?
Thanks,
Jeremy
Email Gateway (Aug 18 2022 at 11:15):From: Amine Chaieb <chaieb@in.tum.de>
Dear Jeremy,
thanks for your replies. But I find that these ML antiquotations are
fine when
they are in a theory file or ML file which I load, but don't work when
I'm entering
code at the keyboard, which I do when I am developing complex procedures.(for that matter, when I'm entering code at the keyboard, presumably
there is no difference between static and dynamic - or have I
misunderstood these terms?)
I am not sure about what you mean by "entering code at the keyboard",
but You can use antiquotations when you program (I do it all the time).
You just need to make sure that your file (or piece of Code) is loaded
by Isar and not by ML. Antiquotations make no since without
Isar-context. Technically, there is an interpreter of these
Antiquotations that generates the lengthy Code you would write, when you
want to refer to logical entities.
In interactive theory development, you can start an ML section inside
Isar by
ML{*
your code with antiquotations and X-symbols etc..
*}
You can run this code just like other theory elements, and will be
interpreted with respect to the Isar context at that point.
ML antiquotations that depend on the context, with use that context,
at compile time. This is in contrast with calls like the_context(),
which takes place when called (which again depends -- might be the
compile time context or run time depending on the call's position).
If you like more details, see [1].
So, given that I want to load the theory MSA, and then, subsequently,
sometimes, maybe,
use a file containing some ML procedure, how should I do this?
You must declare this dependency as Stefan pointed out.
theory Foo
imports ...
uses bar
begin
Now if you want your file to be used before starting the theory, you
must set bar = "yourfilename". If you want the file to be loaded
afterwards you must set bar = ("yourfilename") --- Note the
parentheses. At any point in the theory you can do
use "yourfilename"
Hope it helps.
Amine.
[1]: Makarius Wenzel and Amine Chaieb. SML with antiquotations embedded
into Isabelle/Isar. In Jacques Carette and Freek Wiedijk, editors,
Workshop on Programming Languages for Mechanized Mathematics (part of
CALCULEMUS 2007). Hagenberg, Austria, June 2007
Email Gateway (Aug 18 2022 at 11:15):From: Amine Chaieb <chaieb@in.tum.de>
I do not see the problem clearly any more I must confess. Look at
HOL/Presburger.thy. There you have a dependency on two sorts of ML files
: those loaded before, and those loaded during the theory. The second
ones contain antiquotations.
Btw ML{* *}. You can write pages of code in between, so you would have
to type ML{* *} only when Proofs and ML code "alterate" or interact.
Usually you prove some theorems and then want to write a procedure to
manipulate these. To switch back to "theorems" or proof mode, on reason
would be to use the developped proof procedure. Do you such a extremely
coupled and interdependent bott-strapping process?
Maybe I misunderstand the issue.
Amine.
Jeremy Dawson wrote:
Email Gateway (Aug 18 2022 at 11:15):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Amine Chaieb wrote:
Dear Jeremy,
thanks for your replies. But I find that these ML antiquotations are
fine when
they are in a theory file or ML file which I load, but don't work
when I'm entering
code at the keyboard, which I do when I am developing complex
procedures.(for that matter, when I'm entering code at the keyboard, presumably
there is no difference between static and dynamic - or have I
misunderstood these terms?)I am not sure about what you mean by "entering code at the keyboard",
but You can use antiquotations when you program (I do it all the time).
Dear Amine,
What I mean is something like this
val a = .... ; (entered interactively, so I can look at the result
before proceeding)
val b = ... ; (ditto)
val c = ... ; (ditto)
val d = the_context () (or whatever)
Now if I start up Isar, none of the above works.
I gather I could do the following
ML {* val a = .... ; *}
ML {* val b = ... ; *}
ML {* val c = ... ; *}
ML {* val d = the_context () ; *}
or for that matter
ML {* val d = @{context} ; *}
Is this what you mean? Forever typing an additional " ML {* _ *}" ?
You just need to make sure that your file (or piece of Code) is loaded
by Isar and not by ML. Antiquotations make no since without
Isar-context. Technically, there is an interpreter of these
Antiquotations that generates the lengthy Code you would write, when
you want to refer to logical entities.
In interactive theory development, you can start an ML section inside
Isar byML{*
your code with antiquotations and X-symbols etc..
*}
You can run this code just like other theory elements, and will be
interpreted with respect to the Isar context at that point.
ML antiquotations that depend on the context, with use that context,
at compile time. This is in contrast with calls like the_context(),
which takes place when called (which again depends -- might be the
compile time context or run time depending on the call's position).
If you like more details, see [1].So, given that I want to load the theory MSA, and then, subsequently,
sometimes, maybe,
use a file containing some ML procedure, how should I do this?You must declare this dependency as Stefan pointed out.
theory Foo
imports ...
uses bar
beginNow if you want your file to be used before starting the theory, you
must set bar = "yourfilename". If you want the file to be loaded
afterwards you must set bar = ("yourfilename") --- Note the
parentheses. At any point in the theory you can do
use "yourfilename"This doesn't work - and if I understood correctly, Stefan explained why,
the theory file doesn't contain use bar. I want to load the theory
file, do some work interactively (eg, involving development or changes
to bar), then use bar. This is what
seemed to be related to the failure I reported earlier
Thanks.
Jeremy
Hope it helps.
Amine.[1]: Makarius Wenzel and Amine Chaieb. SML with antiquotations
embedded into Isabelle/Isar. In Jacques Carette and Freek Wiedijk,
editors, Workshop on Programming Languages for Mechanized Mathematics
(part of CALCULEMUS 2007). Hagenberg, Austria, June 2007
Email Gateway (Aug 18 2022 at 11:16):From: Alexander Krauss <krauss@in.tum.de>
Hi Jeremy, hi all,
Jeremy Dawson wrote:
What I mean is something like this
val a = .... ; (entered interactively, so I can look at the result
before proceeding)
val b = ... ; (ditto)
val c = ... ; (ditto)
val d = the_context () (or whatever)
Amine Chaieb wrote:
Btw ML{* *}. You can write pages of code in between, so you would have
to type ML{* *} only when Proofs and ML code "alterate" or interact.
Maybe the misunderstanding is that Jeremy is used to working at the
interactive terminal, typing ML expressions and getting responses. When
developing proof procedures, I used to work like this, too, but now I
have switched completely to an "Isar-centric" style of working,
primarily since the antiquotations are so useful.
What I usually do nowadays, when I develop ML code interactively is this:
In ProofGeneral, set up a theory:
| theory Scratch
| imports WhateverYouNeed
| begin
Then, I open up an ML section, and type term a:
| ML {*
| val a = ...;
| *}
To see what happens, I step over this section (using PG). And then I fix
it until it typechecks :-).
Now I want to keep editing, so I step back in PG and add the new
declaration:
| ML {*
| val a = ...;
| val b = ...;
| *}
This is a bit like working on a tty, but you get all the benefits of
having a "true context" around that you can refer to using
antiquotations. E.g. I write
Const (@{const_name "wf"}, ...)
instead of
Const ("Wellfounded_Recursion.wf", ...)
and if I mistype the name I get a useful error instead of some
unpredictable garbage. The same for theorems @{thm ...} and so on.
Also, with this style of working, I have the development inside a file
that I can save. And when the development is finished, the theory can be
imported in some other developments, with all the contexts and
dependencies managed correctly, and you always know statically, what
@{context} refers to.
Maybe this helps solving your problems with "the_context ()": Avoid it. :-)
Alex
Email Gateway (Aug 18 2022 at 11:16):From: Amine Chaieb <chaieb@in.tum.de>
Dear Jeremy,
Jeremy Dawson wrote:
Dear Amine,
I am referring to files I want to load _after_ loading the theory. Not
before the theory, not during the theory. That is to say, I want to
load the theory (without loading the ML file). I want to load the ML
file _later_, at some subsequent time. If I understand the file
Assume we have bar.thy and file.ML, and you want to load file.ML after
bar.thy. Choose a name, wlo. bar2.thy, and import bar.thy in the header
and use file.ML -- doesn't this do the job?
As I understand you want to use theories and ML files from the ML
toplevel. Combining this with Antiquotations is painful. I have tried it
once, since I used to develop everything on the ML toplevel. By the
advent of antiquotations and other means, I left ML toplevel and only
develop as Alex presented. Antiquotations and Co not only make *no
sense* without Isar context, but turn against you without it.
As Makarius says, this is the Context penalty.
that if I were to type in
ML {*
val a = .... ;
val b = ... ;
val c = ... ;
*}
then I wouldn't see the result for a before b is calculated, and so on.
This is therefore not what I need.
This is indeed an Issue. Especially if a takes long.
By the way, In emacs there is a way to make shortcut for these, but I
don't know exactly how. Cc Ca Ca gives you the antiquotation @{text ""}
with cursor ready inside the quotes, so there must be a way for ML{* *}
Amine.
Email Gateway (Aug 18 2022 at 11:16):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Amine Chaieb wrote:
I do not see the problem clearly any more I must confess. Look at
There you have a dependency on two sorts of ML files : those loaded
before, and those loaded during the theory. The second ones contain
antiquotations.Dear Amine,
I am referring to files I want to load _after_ loading the theory. Not
before the theory, not during the theory. That is to say, I want to
load the theory (without loading the ML file). I want to load the ML
file _later_, at some subsequent time. If I understand the file
HOL/Presburger.thy correctly, it loads some files before loading the
theory, and some files during the loading of the theory. I do not see
how it declares files so as to permit them to be loaded afterwards.
Btw ML{* *}. You can write pages of code in between, so you would have
to type ML{* *} only when Proofs and ML code "alterate" or interact.
In my experience the code between the ML {* and the *} is executed all
at once. I am referring to a situation where I am developing the ML
code, and where I do so by entering some ML code, having it run, viewing
the result on the screen, and then writing some more ML code, and so
on. Eventually there may well be lots of ML code which can no doubt be
enclosed by a single ML {* and *}. But while I am developing it, or
debugging it, I want to view the output of small parts of it. This is
why I gave the following as the example:
val a = .... ; (entered interactively, so I can look at the result
before proceeding)
val b = ... ; (ditto)
val c = ... ; (ditto)
val d = the_context () (or whatever)
Now I understand (and this is how it works for me, anyway)
that if I were to type in
ML {*
val a = .... ;
val b = ... ;
val c = ... ;
*}
then I wouldn't see the result for a before b is calculated, and so on.
This is therefore not what I need.
Regards,
Jeremy
Usually you prove some theorems and then want to write a procedure to
manipulate these. To switch back to "theorems" or proof mode, on
reason would be to use the developped proof procedure. Do you such a
extremely coupled and interdependent bott-strapping process?Maybe I misunderstand the issue.
Amine.
Dear Amine,
What I mean is something like this
val a = .... ; (entered interactively, so I can look at the result
before proceeding)
val b = ... ; (ditto)
val c = ... ; (ditto)
val d = the_context () (or whatever)
the theory file doesn't contain use bar. I want to load the theory
file, do some work interactively (eg, involving development or
changes to bar), then use bar. This is what
seemed to be related to the failure I reported earlierThanks.
Jeremy
Email Gateway (Aug 18 2022 at 11:16):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Amine Chaieb wrote:
Dear Jeremy,
Jeremy Dawson wrote:
Dear Amine,
I am referring to files I want to load _after_ loading the theory.
Not before the theory, not during the theory. That is to say, I want
to load the theory (without loading the ML file). I want to load the
ML file _later_, at some subsequent time. If I understand the fileAssume we have bar.thy and file.ML, and you want to load file.ML
after bar.thy. Choose a name, wlo. bar2.thy, and import bar.thy in
the header and use file.ML -- doesn't this do the job?Dear Amine,
I haven't tried it but I imagine it would. I have in the past used
"dummy" theories to
load an ML file and (in Isabelle2005) it worked.
As I understand you want to use theories and ML files from the ML
toplevel. Combining this with Antiquotations is painful. I have tried
it once, since I used to develop everything on the ML toplevel. By the
advent of antiquotations and other means, I left ML toplevel and only
develop as Alex presented. Antiquotations and Co not only make *no
sense* without Isar context, but turn against you without it.
As Makarius says, this is the Context penalty.OK, well supposing I used @{theory} instead of the_context () in an ML file.
Now it was said earlier that @{theory} is evaluated statically, and
the_context () is evaluated dynamically. I take it this means that
the_context () is evaluated at the point where the code is encountered.
When is @{theory} evaluated? Is it immediately before the ML file is
loaded? Or is it before the theory file, in which the ML file is
declared, is loaded?
Likewise if I use @{theory} in an ML {* ... *} portion of a .thy file.
In this event,
what is the point where @{theory} is evaluated? Is it before the .thy
file is loaded, or is it at the point where the "ML {*" is encountered,
or where?
Thanks,
Jeremy
Email Gateway (Aug 18 2022 at 11:16):From: Alexander Krauss <krauss@in.tum.de>
Jeremy Dawson wrote:
OK, well supposing I used @{theory} instead of the_context () in an ML
file.
Now it was said earlier that @{theory} is evaluated statically, and
the_context () is evaluated dynamically. I take it this means that
the_context () is evaluated at the point where the code is encountered.
Worse: When the code is run. Suppose you are defining a function:
fun f x =
let
...
val thy = the_context ()
Now the context will be evaluated (to the value of some global
reference) whenever you apply the function. This is almost never what
you want.
When is @{theory} evaluated? Is it immediately before the ML file is
loaded? Or is it before the theory file, in which the ML file is
declared, is loaded?
The former.
Likewise if I use @{theory} in an ML {* ... *} portion of a .thy file.
In this event,
what is the point where @{theory} is evaluated? Is it before the .thy
file is loaded, or is it at the point where the "ML {*" is encountered,
or where?
The latter.
Alex
Email Gateway (Aug 18 2022 at 11:17):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Jeremy Dawson wrote:
This is also the way I develop things for Isabelle. I haven't yet moved
to ML in antiquotations.
I use the following to reliably get a specific theory context....
use_thy "MyTheory";
val thry = Theory.begin_theory "test" [theory "MyTheory"];
(* sometime I then use:
ML_Context.set_context (SOME (Context.Theory thry)); *)
I then usually use the variable "thry". If I finally want to publish the
code in a theory, I abstract over "thry" using the antiquotations, or
use the ML loading mechanisms from the theory that needs the ML code -
in which case I can drop the header from my development file.
It's interesting to see theory development at the ML level - the need to
do this depends on what level of programming you are doing. I quite like
to be able to automate the making of definitions, and other theory-level
changes. Thus I work at the ML level for two reasons:
However, I haven't really played seriously with the antiquotations, so
perhaps I'm just out of date with the latest and best coding fashions :)
lucas
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
iD8DBQFHlTuRogMqU4edHsMRAnfFAKCM8enLaiPJAGpmKKubJ4b/Y0Q0IQCgkYBc
PMK4V1NxXrsGNqU/2Hc4DXU=
=HATY
-----END PGP SIGNATURE-----
Last updated: May 03 2024 at 12:27 UTC