Re: [isabelle] qed and done take long for large goal states



Hi Makarius,

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
  document content.

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 top-level statements.

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.

Andreas

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.


	Makarius





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