displaying a large-ish hypothesis above the line is much slower than displaying it below the line
samuelgruetter opened this issue · 8 comments
Here's a goal of the form P -> False, where P is somewhat (but not insanely) large.
Axiom f_seven: nat -> nat -> nat.
Axiom name_fa5ad9a8557e5a84cf23e52d3d3adf77: nat.
Axiom name_f78217cf5d6a5b1929afde: nat.
Axiom name_fa5f557702b144ffde1014e: nat.
Axiom name_ff542fae7e0c4267e45740a12c9a0: nat.
Axiom name_fa93ed2d37b4c5da9f2f87fd: nat.
Axiom name_4adc8224eb736aa10e168390ac8cc251: nat.
Axiom name_e3e13013b74d872953e2a1225c2b5cd0: nat.
Axiom name_f8a5ff693c0: nat.
Axiom name_f1c598e2a3c06c0d60057: nat.
Axiom name_ed9c7d5a52a8aca1e3da7b3e59928b2a: nat.
Axiom name_ff36a4d691713df590ba6738b87: nat.
Axiom name_f0f88e9c6539376ad71202b753: nat.
Axiom name_f194fa089: nat.
Axiom name_fae393b3df0df3290b5cd543171e42: nat.
Axiom name_ff79fa6efb5016a000ce2b9b721b: nat.
Axiom name_a370cd703d0d045abe9e40525e7badda: nat.
Axiom name_f7cb1ad7742c55d9dffb24c55fcc2: nat.
Axiom name_fd2d5d76e3a9fdd1dfee82dc75dfa0: nat.
Axiom name_f434f6e57d48777af56c27969c3090: nat.
Goal
f_seven name_fa5ad9a8557e5a84cf23e52d3d3adf77 (
f_seven name_f78217cf5d6a5b1929afde (
f_seven name_fa5f557702b144ffde1014e (
f_seven name_ff542fae7e0c4267e45740a12c9a0 (
f_seven name_fa93ed2d37b4c5da9f2f87fd (
f_seven name_4adc8224eb736aa10e168390ac8cc251 (
f_seven name_e3e13013b74d872953e2a1225c2b5cd0 (
f_seven name_f8a5ff693c0 (
f_seven name_f1c598e2a3c06c0d60057 (
f_seven name_ed9c7d5a52a8aca1e3da7b3e59928b2a (
f_seven name_ff36a4d691713df590ba6738b87 (
f_seven name_f0f88e9c6539376ad71202b753 (
f_seven name_f194fa089 (
f_seven name_fae393b3df0df3290b5cd543171e42 (
f_seven name_ff79fa6efb5016a000ce2b9b721b (
f_seven name_a370cd703d0d045abe9e40525e7badda (
f_seven name_f7cb1ad7742c55d9dffb24c55fcc2 (
f_seven name_fd2d5d76e3a9fdd1dfee82dc75dfa0 (
f_seven name_f434f6e57d48777af56c27969c3090 (
20
))))))))))))))))))) = 0 -> False.
Proof.
idtac. (* <-- immediate *)
intros. (* <-- keeps the emacs process busy for 11 seconds *)
Displaying P in the conclusion works very fast. However, when I move it above the line using intros, this keeps the emacs process busy for 11 seconds.
If I comment out the line (add-hook 'coq-mode-hook #'company-coq-mode) in my ~/.emacs and restart emacs, the intros completes immediately, so I assume it's a company-coq problem rather than a PG problem.
OS version: Fedora 29
emacs version: 26.1
coq version: 8.9.0
PG version: git master 8f90ac961c22099a615c03ed07576aaef820e06d of Tue Feb 12 2019
company-coq version: updated from MELPA today, got 1.0
In case this problem triggers only above a certain term size which varies from machine to machine, here's the Python script I used to create the above goal:
import hashlib
def makename(i):
s = hashlib.md5(i.to_bytes(8, 'big', signed=True)).hexdigest()
i = s.find('f')
if i >= 0:
return s[i:]
else:
return s
def go(n):
print("Axiom f_seven: nat -> nat -> nat.")
for i in range(1, n):
print("Axiom name_{}: nat. ".format(makename(i)))
print("Goal ")
for i in range(1, n):
print("f_seven name_{} (".format(makename(i)))
print(n)
for i in range(1, n):
print(")", end="")
print(" = 0 -> False.")
print("Proof.\n idtac.\n intros.")
go(20)
Thanks. Can you show a profile? M-x profiler-start RET cpu RET, then run the slow code a few times, then M-x profiler-report and M-x profiler-report-write-profile.
Just ran it 5 times, and the interactive unfoldable buffer looks as follows if I follow the most expensive call:
- scomint-output-filter 52120 99%
- run-hook-with-args 52120 99%
- proof-shell-filter-wrapper 52120 99%
- proof-shell-filter 52120 99%
- proof-shell-filter-manage-output 52119 99%
- proof-shell-handle-delayed-output 52108 99%
- run-hooks 52101 99%
- company-coq-maybe-proof-output-reload-things 52081 99%
- company-coq-maybe-reload-context 52078 99%
- company-coq--parse-context-and-goal 52078 99%
- company-coq--collect-hypotheses 52076 99%
company-coq--bounded-re-search-forward 52076 99%
+ company-coq--collect-subgoals 1 0%
generate-new-buffer 1 0%
+ run-with-timer 2 0%
+ company-coq-shell-output-is-error 1 0%
+ coq-show-first-goal 17 0%
+ company-coq-features/alerts--handle-output 1 0%
+ coq-update-minor-mode-alist 1 0%
+ #<compiled 0x12c901d> 1 0%
+ pg-goals-display 7 0%
+ proof-shell-exec-loop 10 0%
+ command-execute 97 0%
+ ... 63 0%
+ redisplay_internal (C function) 30 0%
+ timer-event-handler 19 0%
+ undo-auto--add-boundary 1 0%
Very nice, thanks! Now can you share a copy of the contents of the goals buffer after the call to intros?
Here it is:
1 subgoal (ID 4)
H : f_seven name_fa5ad9a8557e5a84cf23e52d3d3adf77
(f_seven name_f78217cf5d6a5b1929afde
(f_seven name_fa5f557702b144ffde1014e
(f_seven name_ff542fae7e0c4267e45740a12c9a0
(f_seven name_fa93ed2d37b4c5da9f2f87fd
(f_seven name_4adc8224eb736aa10e168390ac8cc251
(f_seven name_e3e13013b74d872953e2a1225c2b5cd0
(f_seven name_f8a5ff693c0
(f_seven name_f1c598e2a3c06c0d60057
(f_seven name_ed9c7d5a52a8aca1e3da7b3e59928b2a
(f_seven name_ff36a4d691713df590ba6738b87
(f_seven name_f0f88e9c6539376ad71202b753
(f_seven name_f194fa089
(f_seven name_fae393b3df0df3290b5cd543171e42
(f_seven name_ff79fa6efb5016a000ce2b9b721b
(f_seven name_a370cd703d0d045abe9e40525e7badda
(f_seven name_f7cb1ad7742c55d9dffb24c55fcc2
(f_seven
name_fd2d5d76e3a9fdd1dfee82dc75dfa0
(f_seven
name_f434f6e57d48777af56c27969c3090
20)))))))))))))))))) = 0
============================
False
The === line is displayed as a single line, but when I copy paste it it becomes ===. I'm a bit surprised as to why you need this, does it mean you can't reproduce it on your own machine?
I'm a bit surprised as to why you need this, does it mean you can't reproduce it on your own machine?
Exactly. Both are instantaneous here :/
Switching from MELPA stable to MELPA solved the problem for me! I have version 20190222.1904 now.
Turns out the version of company-coq which is on MELPA stable is 1.0, which is over 3 years old. Might be worth tagging a more recent commit so that MELPA stable users don't get such an outdated version.
Good idea. Done :)