Email Gateway (Aug 19 2022 at 17:03): Email Gateway (Aug 19 2022 at 17:03):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Joachim,
quick (unrelated) question ;)
How is your "open inductive" related to the AFP entry "Open Induction"?
cheers
chris
Email Gateway (Aug 19 2022 at 17:03):From: Joachim Breitner <breitner@kit.edu>
Hi,
good question. I would assume not at all, as it is not listed in [1] :-)
In "open inductive predicate", you have to associate the words to the
right, i.e. "open (inductive predicates)". The idea is that you can
modularize your inducrive predicates and inductive proofs, something
that I often want to do when working with programming language
semantics. There is not much deep theory, but rather it’s making the
obvious (namely that the cases of inductive proofs are independent)
exploitable. See [1] for more details (motivation, examples, user
guide).
In your entry, if I am not mistaken, "open" refers to topology.
Greetings,
Joachim
[1] http://pp.ipd.kit.edu/uploads/publikationen/molitor15masterarbeit.pdf
signature.asc
Email Gateway (Aug 19 2022 at 17:04):From: Makarius <makarius@sketis.net>
The parallelism is less aggressive in interactive PIDE document processing
than in batch build. This might be a reason for the breakdown of the
forked proof, see als src/Pure/thm.ML function future_result.
Since I can't reproduce the problem, I recommend to insert a different
exception there, e.g. TERM with the relevant arguments for more
information.
Skimming over the sources of open_inductive.ML, there are various points
that look a bit suspicious concerning hyps and context, which might be a
source of such problems. Occasionally it looks like the abstract notion
of goal state -- which happens to be represented as concrete thm, but with
certain implicit policies -- is not properly observed.
I have more to say about the sources, but that has to wait.
Makarius
Email Gateway (Aug 19 2022 at 17:04):From: Joachim Breitner <breitner@kit.edu>
Dear Makarius,
thanks for your reply.
Am Dienstag, den 24.02.2015, 15:50 +0100 schrieb Makarius:
what is usually the cause for the error message
*** exception THM 0 raised (line 532 of "thm.ML"): future_result: bad prop
To reproduce with Isabelle-2014, run
$ git clone https://github.com/gattschardo/open-inductive
$ cd open-inductive
add "Open_Arith_Eval" to "theories" in ROOT
$ isabelle build -D .It does not (seem to) occur in Isabelle/jEdit.
The parallelism is less aggressive in interactive PIDE document processing
than in batch build. This might be a reason for the breakdown of the
forked proof, see als src/Pure/thm.ML function future_result.Since I can't reproduce the problem,
do you meant the problem does not occur for you, or that you were unable
to attempt to reproduce it?
I recommend to insert a different
exception there, e.g. TERM with the relevant arguments for more
information.
Thanks, we’ll try that.
Skimming over the sources of open_inductive.ML, there are various points
that look a bit suspicious concerning hyps and context, which might be a
source of such problems. Occasionally it looks like the abstract notion
of goal state -- which happens to be represented as concrete thm, but with
certain implicit policies -- is not properly observed.I have more to say about the sources, but that has to wait.
A review of that code would be highly appreciated – you can probably
tell that it was not written with a great lot of experience with and
comprehensive knowledge of the Isabelle internals.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 17:05):From: Makarius <makarius@sketis.net>
It is fine as a first project to implement an Isabelle "package". I can
offer a standard pencil-review on the sources, with scanned results sent
back (privately). This could help to make one more round of refinement,
and then proceed to more deeper points.
I suppose this work is meant for AFP?
Makarius
Email Gateway (Aug 19 2022 at 17:05):From: Makarius <makarius@sketis.net>
I tried the batch build 3 times, and it worked 3 times (on 6 cores). I
did not try further, but only looked a bit through the sources.
Makarius
Email Gateway (Aug 19 2022 at 17:18):From: Joachim Breitner <breitner@kit.edu>
Dear list,
what is usually the cause for the error message
*** exception THM 0 raised (line 532 of "thm.ML"): future_result: bad prop
To reproduce with Isabelle-2014, run
$ git clone https://github.com/gattschardo/open-inductive
$ cd open-inductive
add "Open_Arith_Eval" to "theories" in ROOT
$ isabelle build -D .
It does not (seem to) occur in Isabelle/jEdit.
Thanks,
Joachim
signature.asc
Last updated: Apr 25 2024 at 20:15 UTC