Email Gateway (Aug 22 2022 at 18:45): Email Gateway (Aug 22 2022 at 18:45):From: Dominique Unruh <unruh@ut.ee>
Hello,
I have the following setting:
- In an external program I load an Isabelle theory Test (via
libisabelle). From the Isabelle point of view, this is a call to
Thy_Info.use_thy.
- If Test.thy contains errors, Thy_Info.use_thy will usually fail. This
is desired from my side.
- However, in some cases (e.g., a "by" that fails, or a use of "sorry"
without quick_and_dirty mode), errors occur inside futures (I think). Then
Thy_Info.use_thy will succeed. This is not desired because I want to give
an error message when loading fails.
How can I, on the Isabelle/ML level, force all futures involved in a theory
to finish in order to throw any potential exceptions? (Something like "val
_ = Thy_Info.use_thy "Draft.Test"; val thy = Thy_Info.get_theory
"Draft.Test"; val _ = join_theory thy (* This one does not exist *)")
I believe this should be possible because the build process does give
errors when a proof fails, after all, instead of simply storing a failing
future in the heap image.
To avoid misunderstandings: I am not working in the bootstrap
ML-environment, but the proper Isabelle/ML environment.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 18:45):From: Makarius <makarius@sketis.net>
On 15/11/2018 17:38, Dominique Unruh wrote:
- However, in some cases (e.g., a "by" that fails, or a use of "sorry"
without quick_and_dirty mode), errors occur inside futures (I think). Then
Thy_Info.use_thy will succeed. This is not desired because I want to give
an error message when loading fails.
Thy_Info.use_thy should be strict under normal circumstances. Can you
show an example where it succeeds?
Of course it is possible to fabricate some Isabelle/ML snippets that
hides errors in futures, but I suppose you have used regular proof
language elements here (Isar commands and proof methods)?
Another potential source of problems: using Thy_Info.use_thy in
multithreaded user-space Isabelle/ML; it is only for the raw bootstrap
environment when nothing else is running.
How can I, on the Isabelle/ML level, force all futures involved in a theory
to finish in order to throw any potential exceptions? (Something like "val _ = Thy_Info.use_thy "Draft.Test"; val thy = Thy_Info.get_theory
"Draft.Test"; val _ = join_theory thy (* This one does not exist *)")
Thy_Info.use_thy should to the full join_theory for you. If it does not,
there is something wrong somewhere.
Note that "ML level" is outdated terminology from 20 years ago. Today we
have two main ML environments:
(1) Isabelle/ML: this is regular user-space Isabelle/ML (inside a
theory context).
(2) The ML bootstrap environment (Poly/ML with some add-ons). Normally
only Isabelle system tools use that, but it is also possible do
"isabelle process" invocations, analogously to how "isabelle build".
I believe this should be possible because the build process does give
errors when a proof fails, after all, instead of simply storing a failing
future in the heap image.To avoid misunderstandings: I am not working in the bootstrap
ML-environment, but the proper Isabelle/ML environment.
If you are actually using Thy_Info.use_thy inside regular user-space
Isabelle/ML, this is not going to work. Maybe that is the actual problem
here.
Again the usual questions: What is your greater application context?
What are you trying to do?
The new Isabelle PIDE server might be better for it, but it is still
unused / untested in Isabelle2018. After the release, I have made my own
applications on top of it: to process all of Isabelle + AFP and
overserve resulting theory status and markup. This required some
reworking on the server, and it probably needs more reworking to make it
applicable in even more applications.
Makarius
Email Gateway (Aug 22 2022 at 18:46):From: Dominique Unruh <unruh@ut.ee>
Of course it is possible to fabricate some Isabelle/ML snippets that
hides errors in futures, but I suppose you have used regular proof
language elements here (Isar commands and proof methods)?
I am using libisabelle. So essentially I do is: I instantiate Isabelle
with libisabelle. I issue a command from libisabelle to Isabelle to load a
theory which uses Thy_Info.use_thy. This operation completes (that is, I
know that I get a theory and not a "theory future" back because I do
successfully, e.g., print theorems from it). At some point I am asking for
a proof term, and this leads to a delayed exception. On the level of the
theory that is loaded, however, I don't do weird ML. I can get the error
with something as simple as a "sorry" in quick_and_dirty=false mode.
Thy_Info.use_thy should be strict under normal circumstances. Can you
show an example where it succeeds?
I could, I think, but it would be quite some work. (Since I would have to
rewrite the whole setting involving libisabelle described above from
scratch since the problem is too deeply buried in my application. Including
setting up all the build environment etc. I don't see a way to make it
happen without libisabelle because, as you pointed out, using use_thy
inside a normal Isabelle session does not work.)
Interestingly, when trying to get the same to happen using
"Isabelle2018/bin/isabelle console -l HOL -s" and then entering
Thy_Info.use_thy, the problem does not occur (the theory fails right away).
So it might actually be a problem with libisabelle.
I will ask Lars Hupel, perhaps he knows something about this.
But if you know some hotfix (i.e., some way to force the theory to join
after it has loaded even if we don't understand why it hasn't been fully
joined in the first place) I would be happy. Because this problem looks
like it's going to be confusing to track down.
Again the usual questions: What is your greater application context?
What are you trying to do?
I have a scala application (https://github.com/dominique-unruh/qrhl-tool)
that uses Isabelle as a backend for reasoning about terms. For this,
Isabelle gets loaded via libisabelle, the Isabelle session containing my
theories gets loaded via libisabelle, and then various ML-snippets (e.g.,
for calling the simplifier on a term) are invoked via libisabelle.
The new Isabelle PIDE server might be better for it, but it is still
unused / untested in Isabelle2018. After the release, I have made my own
applications on top of it: to process all of Isabelle + AFP and
overserve resulting theory status and markup. This required some
reworking on the server, and it probably needs more reworking to make it
applicable in even more applications.
I had a look at the PIDE server. While I didn't fully understand the scope
of it, I had the feeling that it was more for "highlevel" operations (like
"build a theory"), and not for things like "simplify this particular term".
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 18:47):From: Lars Hupel <hupel@in.tum.de>
I could, I think, but it would be quite some work. (Since I would have to
rewrite the whole setting involving libisabelle described above from
scratch since the problem is too deeply buried in my application. Including
setting up all the build environment etc. I don't see a way to make it
happen without libisabelle because, as you pointed out, using use_thy
inside a normal Isabelle session does not work.)
I can corroborate this (mostly). When developing the Isabelle
integration with Leon, I used "Goal.parallel_proofs := 0" quite
liberally. In my case the problem was less with loading theories;
rather, running arbitrary ML code that may or may not throw asynchronous
exceptions.
I will ask Lars Hupel, perhaps he knows something about this.
If you can send me a minimal example how I can reproduce the problem, I
could take a look.
Cheers
Lars
Email Gateway (Aug 22 2022 at 18:47):From: Dominique Unruh <unruh@ut.ee>
Hi Lars,
I managed to make a minimal example (attached).
The actual code is in src/main/scala/test/Test.thy, and the bad theory is
TestEx.thy.
The line "val response = ..." is the offending code which fails to give an
error.
Interestingly, a variation of this line (included and commented out) does
raise an error!
You can test the code simply using "sbt run".
Best wishes,
Dominique.
libisabelle-use-thy.zip
Last updated: Nov 21 2024 at 12:39 UTC