Email Gateway (Aug 19 2022 at 17:04): Email Gateway (Aug 19 2022 at 17:04):From: Makarius <makarius@sketis.net>
I have refined that here, so it is likely to be in the coming release:
http://isabelle.in.tum.de/repos/isabelle/rev/fdc03c8daacc
There is also some updated documentation in the same changeset.
Makarius
Email Gateway (Aug 19 2022 at 17:15):From: Christian Sternagel <c.sternagel@gmail.com>
Dear experts,
in src/Pure/goal.ML there is the Goal.prove_future variant of
Goal.prove. However I couldn't find a "future" variant of Goal.prove_multi.
In complete ignorance of implementation details I have two questions:
Is it just an interface-omission that there is no
Goal.prove_multi_future or are there technical reasons for not having
such a variant of Goal.prove_multi?
Why isn't Goal.prove implicitly "futurized"? (So that the standard
behavior allows for implicit parallelization; I guess that's not always
a good thing.)
cheers
chris
Email Gateway (Aug 19 2022 at 17:15):From: Makarius <makarius@sketis.net>
On Tue, 17 Feb 2015, Christian Sternagel wrote:
in src/Pure/goal.ML there is the Goal.prove_future variant of Goal.prove.
However I couldn't find a "future" variant of Goal.prove_multi.Is it just an interface-omission that there is no
Goal.prove_multi_future or are there technical reasons for not having
such a variant of Goal.prove_multi?
Yes, as far as I can say on the spot, there could be
Goal.prove_multi_future, but it was never used so far. The Goal.prove
variants are relatively pragmatic, e.g. legacy things like
Goal.prove_global are there, because some packages still need them, and
thus their implementation is simplified a bit.
In most situations, a plain "map" of Goal.prove should do the same job.
You mainly need Goal.prove_multi for simultaneous induction.
If you do have a convincing application, I can nonetheless add the missing
variant for the next release.
Why isn't Goal.prove implicitly "futurized"? (So that the standard
behavior allows for implicit parallelization; I guess that's not always
a good thing.)
In Isabelle/ML programming there is often a situation where some tool uses
Goal.prove ... handle ERROR _ => to react on a failed attempt, i.e. there
is an implicit assumption of strictness of this operation.
There is an ancient Isabelle tradition to change semantics only together
with the name of an operation, so I left Goal.prove unchanged and added
Goal.prove_future. It should be easy to upgrade tools that cope with
forked proofs by searching for Goal.prove and making educated guesses if
it can be replaced by Goal.prove_future.
Makarius
Email Gateway (Aug 19 2022 at 17:16):From: René Thiemann <rene.thiemann@uibk.ac.at>
That would indeed be nice. The application we have in mind are the datatype order/show/... generators.
We just recently got a request from Dmitriy to use the Goal.prove_..._future variants, since the invocation
of the generator on some particular datatype took over 3 minutes which was blocking the further proceeding
of the theory file. This is now fixed for the current generators which work on the (old) datatypes and do not require
Goal.prove_multi. However, we are in the process of also providing these generators for the BNF-based (new) datatypes, where the usage
of Goal.prove_multi is essential since the first step is an simultaneous induction.
To summarize, without Goal.prove_multi_future we have to wait over a minute for the new generators on Dmitriys datatype,
but with it(*) the generator returns immediately.
Best regards,
René
(*): Here is our diff in Pure/goal.ML:
(in signature)
val prove_multi_future: Proof.context -> string list -> term list -> term list ->
({prems: thm list, context: Proof.context} -> tactic) -> thm list
(in implementation)
val prove_multi_future = prove_common false ~1;
Last updated: May 06 2024 at 08:19 UTC