Email Gateway (Aug 22 2022 at 17:55): Email Gateway (Aug 22 2022 at 17:55):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
I can't make sense of this. What is a formal theory context? I would
understand that to mean a theory as I've always understood it - but that
is defined in ML code.
Just by way of example - the developments found in the ML file
src/Pure/theory.ML - what is the formal theory context which that
happened in?
In relation to your answers to my other questions: are you seriously
telling me that one can't effectively use Isabelle except by using the
jedit thing? May I be so bold as to ask if there is any good reason for
this?
Jeremy
Email Gateway (Aug 22 2022 at 17:56):From: Lars Hupel <hupel@in.tum.de>
Dear Jeremy,
I can't make sense of this. What is a formal theory context? I would
understand that to mean a theory as I've always understood it - but that
is defined in ML code.Just by way of example - the developments found in the ML file
src/Pure/theory.ML - what is the formal theory context which that
happened in?
let me try to untangle this a bit.
It is very important to distinguish between the bootstrapping of the
system (a bit oversimplified: "everything in src/Pure") from the general
user-space operation of the system (a bit oversimplified: "everything
that happens in a .thy file").
As a user of the system, it is generally not very relevant how ML files
are handled in "src/Pure".
After bootstrapping has happened, you have the full flexibility of
Isabelle/ML, including antiquotations, available by embedding or
referencing ML code from a theory file. This is precisely what is meant
by "formal theory context".
In a more low-level environment this can be done by using the "use_thy"
function to load a theory file. ML code that is embedded there can use
antiquotations. Here's an example:
$ ./bin/isabelle console -l Pure -i HOL
Poly/ML> use_thy "Main";
In relation to your answers to my other questions: are you seriously
telling me that one can't effectively use Isabelle except by using the
jedit thing? May I be so bold as to ask if there is any good reason for
this?
There are other ways to interact with Isabelle too (e.g.
Isabelle/VSCode), or by writing Scala code that sets up a prover in just
the right way. But I'd argue for 95% of users Isabelle/jEdit is indeed
the vastly more convenient environment.
If I remember the history correctly, many of the "old-style"
interactions with Isabelle had to be abolished because of performance
reasons; i.e. to allow full exploitation of multi-core machines.
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:56):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
On 08/15/2018 12:56 AM, Lars Hupel wrote:
$ ./bin/isabelle console -l Pure -i HOL
Poly/ML> use_thy "Main";Hi Lars,
Thanks - but doing this doesn't remember the declarations in the theory
file, or in ML files loaded by ML_file within the theory file.
If I remember the history correctly, many of the "old-style"
interactions with Isabelle had to be abolished because of performance
reasons; i.e. to allow full exploitation of multi-core machines.
Well I've used HOL4 and Coq a lot recently (as well as Isabelle2005 for
many years), performance never seemed to be a problem. Whereas the
sluggishness of Isabelle 2018 is quite noticeable on the same machines
(console isn't too bad, but jedit is much worse, which is one of the
reasons I would much rather not have to use it)
Maybe the complexity of Isabelle is the reason for performance problems,
not the solution to them.
Cheers
Jeremy
Email Gateway (Aug 22 2022 at 17:56):From: Makarius <makarius@sketis.net>
On 14/08/18 16:41, Jeremy Dawson wrote:
Just by way of example - the developments found in the ML file
src/Pure/theory.ML - what is the formal theory context which that
happened in?
There are two different cases:
(1) physical bootstrap from raw Poly/ML: the theory context is the
emerging Pure.thy context under construction, which will be eventually
finished in the "Pure.thy" file.
(2) virtual boostrap in the Prover IDE (e.g. Isabelle/jEdit when
opening src/Pure/ROOT.ML): the theory context starts with
ML_Bootstrap.thy from which a copy of Pure.thy is constructed in the
virtual environment.
At the bottom of this are some interesting implementation techniques,
such as the Thread_Data module:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018-RC4/src/Pure/Concurrent/thread_data.ML
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018-RC4/src/Pure/Concurrent/thread_data_virtual.ML
Apart from that, the main user-relevant point is this: after opening
src/Pure/ROOT.ML in the Prover IDE, the Pure bootstrap sources become
"alive", e.g. with inferred types, indentifier scopes, hyperlinks etc.
This is very important to understand them, and to build tools on top, or
to develop the system itself.
In relation to your answers to my other questions: are you seriously
telling me that one can't effectively use Isabelle except by using the
jedit thing? May I be so bold as to ask if there is any good reason for
this?
Mainly for performance reasons of using the system: without such a
high-end IDE Isabelle applications would not be where they are today.
Investing a little hardware is very cheap: 16 GB memory cost mere
100-200 EUR.
In that respect Isabelle is very old-fashioned: it turns commodity
hardware resources into performance for applications. This rules out
very small devices, but we did that already in 1998, when the minimal
memory requirements were 32-64 MB, IIRC.
Makarius
Email Gateway (Aug 22 2022 at 17:56):From: Makarius <makarius@sketis.net>
We just moved on, as we did many times in the history of Isabelle
front-ends. There was also nobody to step in and maintain obsolete user
interfaces.
In long-term Isabelle development we have always dismantled old things
to make room for new things. This is why the system is still relatively
young and fresh after 32 years.
Makarius
Email Gateway (Aug 22 2022 at 17:56):From: Makarius <makarius@sketis.net>
The complexity of Isabelle and the complexity of Isabelle applications
are co-evolutionary: because applications become more and more advanced
and ambitious, the system needs to catch up. What you see in 2018 is the
result of successful advances in the past, leading to the full glory of
e.g. AFP applications today.
If you don't like this, you are free to ignore Isabelle and should use
HOL4 or Coq. I mean this seriously: we have different systems for
different attitudes.
Makarius
Email Gateway (Aug 22 2022 at 17:57):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
I hope that in the future evolution of Isabelle, some mutation will allows
her to do homotopy type theory. Indeed, this is the more elegant
formulation of algebraic topology ever (real numbers are not required !).
It would be nice to combine it with isar. I think that this reference will
be useful for this purpose: https://github.com/jaycech3n/HoTT
For students which want to know about homotopy type theory, here is an
introductory course:
https://www.youtube.com/watch?v=ISq1xi-mGk8&list=PLo61mJSqK5cXHsnYUAXNea31BCj1u-zln
More advanced staff here: https://www.math.ias.edu/vladimir/Lectures
Jose M.
Email Gateway (Aug 22 2022 at 18:15):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi
I find using isabelle console, when I use a theory file, using use_thy,
seemingly successfully, that declarations in chunks of ML in the theory
file, (in ML{* ... *}) seem to be forgotten.
How do I get access to stuff that was defined in ML in the theory file?
thanks
Jeremy
Email Gateway (Aug 22 2022 at 18:17):From: Makarius <makarius@sketis.net>
By importing the theories with the ML/ML_file uses.
Recall that all Isabelle/ML developments happens inside a formal theory
context, with editor support in the Prover IDE (Isabelle/jEdit).
The raw Poly/ML toplevel is merely the system bootstrap environment.
Compared to a Linux system it would the the Grub prompt of the BIOS, not
the OS shell.
Makarius
Last updated: May 06 2024 at 16:21 UTC