Re: [isabelle] Finishing all proofs in use_thy

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

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.