Re: [isabelle] qed and done take long for large goal states
I had thought that results are printed asynchronously already. At least, the Isabelle NEWS
file for 2013-1 says
* Support for asynchronous print functions, as overlay to existing
If results do not take part in that so far, I think this would be a good time to do so.
I am not so sure about the context option. I usually ignore the output "solved goal by
exported rule ...", so I would not miss that. However, I usually do look at the result of
By the way, I remember two particular "lemmas" commands in JinjaThreads
(Compiler/J1JVMBisim around line 1055) which manipulate induction rules for inductively
defined bisiumlation relations (especially "split_format (complete)"). Their processing
took ages back then with ProofGeneral because of the pretty printing. I haven't checked
how bad it is nowadays on better hardware and with Isabelle/jEdit. When I worked on these
proofs, I wished that I could have disabled the printing of results.
On 10/08/16 14:34, Makarius wrote:
On 10/08/16 13:29, Lawrence Paulson wrote:
That is a major gain and certainly worth keeping.
I am not terribly bothered by the presentation of abbreviations, but nevertheless, perhaps we can get the best of both? After all, no abbreviations are printed when you type qed.
The overall result is printed, and thus all abbreviations of the context
are potentially applied to some potentially large term.
This relative verbosity of the system goes back to the 1990s and TTY
mode / Proof General. In early PIDE versions, it was not done due to
confusion with the remaining Proof General setup. After that was
deleted, printing in the old way was mostly restored.
So maybe instead of tweaking low-level data structures, it is better to
change something in the general policies. E.g.
* A context option like "show_results" to control printing of results.
* Asynchronous printing of results.
This archive was generated by a fusion of
Pipermail (Mailman edition) and