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

[Andreas Lochbihler]

Dear Isar experts,

I am looking for ways to speed up the processing of some of my Isar proofs. Something I
noticed is that when there are no subgoals left, "done" and "qed" nevertheless take
between 2 and 7 seconds of processing (according to the Isabelle timing panel in jEdit).

I guess that the delays must have something to do with the size of the statement being
proved. They only occur for large proof states. For example, large elimination rules (with
approx. 20 cases) or the cases for induction proves about functions defined with
partial_function. The delays are particularly annoying for the latter case, because each
induction proof has many subcases and the delay occurs for each of the subcases.

Are there any options or tweaks to speed up the processing of qed/done?

As the delays also appear inside proofs (i.e., not for top-level lemma statements), I
suspect that attributes and propagation of facts to locale interpretations are not to be
blamed.

My machine is still the usual one:

Linux lenovoal 3.13.0-91-generic #138-Ubuntu SMP Fri Jun 24 17:00:34 UTC 2016 x86_64
x86_64 x86_64 GNU/Linux
Intel(R) Core(TM) i7-3630QM CPU @ 2.40GHz
16GB of RAM

Thanks in advance,
Andreas

[Makarius]

Post by Andreas Lochbihler
I am looking for ways to speed up the processing of some of my Isar
proofs. Something I noticed is that when there are no subgoals left,
"done" and "qed" nevertheless take between 2 and 7 seconds of processing
(according to the Isabelle timing panel in jEdit).
I guess that the delays must have something to do with the size of the
statement being proved. They only occur for large proof states. For
example, large elimination rules (with approx. 20 cases) or the cases
for induction proves about functions defined with partial_function. The
delays are particularly annoying for the latter case, because each
induction proof has many subcases and the delay occurs for each of the subcases.
Are there any options or tweaks to speed up the processing of qed/done?

There might be various "after_qed" bookkeeping steps that take long,
notably in derived definitional packages like 'function' or
'partial_function'.

Moreover, there could be genuine bottle-necks in the standard export
operations and re-adjustment operations performed at the end of a proof.


If you can point to a concrete example that is particularly slow, I can
take a look at profiling information and make more educated guesses.


Makarius

[Makarius]

I manually changed the appropriate
line for Isabelle2016 and processing got indeed a bit faster.
Unfortunately, abbreviations are no longer contracted as they were if
eta-expanded terms are involved. For example,
abbreviation "rel R ≡ list_all2 (rel_option R)"
term "list_all2 (rel_option undefined)"
term "list_all2 (λx. rel_option undefined x)"
Before the change, both "term" command output "rel undefined". After the
change, the second prints "list_all2 (rel_option undefined)".

This requires more rethinking of the approach.

Net.match_term explicitly says "MUST BE BETA-ETA NORMAL", in contrast to
Net.unify_term.

I am unsure if the net operations can be refined to cope with non-normal
terms.


Makarius

[Lawrence Paulson]

As the author of this code, which is already pretty tricky, I would be surprised if it could be fixed easily. If it were, the penalty might be much more permissive filtering, which would defeat the purpose of this code.

It would be useful to see “got indeed a bit faster” quantified. Did the change make a really big improvement in some situations?

Larry

Post by Makarius

I manually changed the appropriate
line for Isabelle2016 and processing got indeed a bit faster.
Unfortunately, abbreviations are no longer contracted as they were if
eta-expanded terms are involved. For example,
abbreviation "rel R ≡ list_all2 (rel_option R)"
term "list_all2 (rel_option undefined)"
term "list_all2 (λx. rel_option undefined x)"
Before the change, both "term" command output "rel undefined". After the
change, the second prints "list_all2 (rel_option undefined)".

This requires more rethinking of the approach.
Net.match_term explicitly says "MUST BE BETA-ETA NORMAL", in contrast to
Net.unify_term.
I am unsure if the net operations can be refined to cope with non-normal
terms.
Makarius

[Andreas Lochbihler]

Hi Larry,

With the plain matching, the processing times for the qed's and done's got down from about
4.5s to 0.8s on my machine (according to the Timing panel). Since there are dozens of them
in that particular theory, the effect was quite noticeable.

Andreas

Post by Lawrence Paulson
As the author of this code, which is already pretty tricky, I would be surprised if it could be fixed easily. If it were, the penalty might be much more permissive filtering, which would defeat the purpose of this code.
It would be useful to see “got indeed a bit faster” quantified. Did the change make a really big improvement in some situations?
Larry

Post by Makarius

I manually changed the appropriate
line for Isabelle2016 and processing got indeed a bit faster.
Unfortunately, abbreviations are no longer contracted as they were if
eta-expanded terms are involved. For example,
abbreviation "rel R ≡ list_all2 (rel_option R)"
term "list_all2 (rel_option undefined)"
term "list_all2 (λx. rel_option undefined x)"
Before the change, both "term" command output "rel undefined". After the
change, the second prints "list_all2 (rel_option undefined)".

This requires more rethinking of the approach.
Net.match_term explicitly says "MUST BE BETA-ETA NORMAL", in contrast to
Net.unify_term.
I am unsure if the net operations can be refined to cope with non-normal
terms.
Makarius

[Lawrence Paulson]

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.

Larry Paulson

Post by Andreas Lochbihler
Hi Larry,
With the plain matching, the processing times for the qed's and done's got down from about 4.5s to 0.8s on my machine (according to the Timing panel). Since there are dozens of them in that particular theory, the effect was quite noticeable.
Andreas

Post by Lawrence Paulson
As the author of this code, which is already pretty tricky, I would be surprised if it could be fixed easily. If it were, the penalty might be much more permissive filtering, which would defeat the purpose of this code.
It would be useful to see “got indeed a bit faster” quantified. Did the change make a really big improvement in some situations?
Larry

Post by Makarius

I manually changed the appropriate
line for Isabelle2016 and processing got indeed a bit faster.
Unfortunately, abbreviations are no longer contracted as they were if
eta-expanded terms are involved. For example,
abbreviation "rel R ≡ list_all2 (rel_option R)"
term "list_all2 (rel_option undefined)"
term "list_all2 (λx. rel_option undefined x)"
Before the change, both "term" command output "rel undefined". After the
change, the second prints "list_all2 (rel_option undefined)".

This requires more rethinking of the approach.
Net.match_term explicitly says "MUST BE BETA-ETA NORMAL", in contrast to
Net.unify_term.
I am unsure if the net operations can be refined to cope with non-normal
terms.
Makarius

[Makarius]

Post by Lawrence Paulson
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

[Andreas Lochbihler]

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

Post by Makarius

Post by Lawrence Paulson
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

[Makarius]

Post by Andreas Lochbihler
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.

The asynchronous printing of 2013 only applies to official command
transaction states, i.e. the subsequent proof state.

We are talking about unofficial side-results here: verbosity produced by
certain commands on their own account.

To make this asynchronous requires some care, because the order of
results should remain stable.

Post by Andreas Lochbihler
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 can imagine that the system spends a good portion of time on
"potentially useful output", often more than performing proof steps.


Makarius

[Andreas Lochbihler]

Hi Larry,

I do care very much about abbreviations. Especially when I work inside a locales, I want
the constants defined in the locale to be printed without all the arguments, i.e.,

foo x

rather than

l.foo p1 p2 p3 x

And if for some reason, any of the parameters p_i gets eta-expanded (e.g., due to
congruence rules or unification), I still want to see "foo x".

Andreas

Post by Lawrence Paulson
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.
Larry Paulson

Post by Andreas Lochbihler
Hi Larry,
With the plain matching, the processing times for the qed's and done's got down from about 4.5s to 0.8s on my machine (according to the Timing panel). Since there are dozens of them in that particular theory, the effect was quite noticeable.
Andreas

Post by Lawrence Paulson
As the author of this code, which is already pretty tricky, I would be surprised if it could be fixed easily. If it were, the penalty might be much more permissive filtering, which would defeat the purpose of this code.
It would be useful to see “got indeed a bit faster” quantified. Did the change make a really big improvement in some situations?
Larry

Post by Makarius

I manually changed the appropriate
line for Isabelle2016 and processing got indeed a bit faster.
Unfortunately, abbreviations are no longer contracted as they were if
eta-expanded terms are involved. For example,
abbreviation "rel R ≡ list_all2 (rel_option R)"
term "list_all2 (rel_option undefined)"
term "list_all2 (λx. rel_option undefined x)"
Before the change, both "term" command output "rel undefined". After the
change, the second prints "list_all2 (rel_option undefined)".

This requires more rethinking of the approach.
Net.match_term explicitly says "MUST BE BETA-ETA NORMAL", in contrast to
Net.unify_term.
I am unsure if the net operations can be refined to cope with non-normal
terms.
Makarius

[Makarius]

I have eta contraction enabled for printing as is the default.

This probably refers to the "eta_contract" attribute. It happens much
later when abstractions are pretty printed.

Abbreviations see the original, independently of this option.


Makarius