Opened 13 years ago
Closed 13 years ago
#384 closed defect (fixed)
Isabelle process killed rudely
| Reported by: | Makarius | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.1 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: | makarius@… |
Description
Exiting the prover is now really fast, but it does not give the process a chance to clean up. Even more importantly, proper commit of a persistent logic session no longer works (it requires closing of stdin and waiting long enough).
Even if there would not be the hard kill of the process, the default proof-shell-quit-timeout 5 is far too low for anything derived from obese Isabelle/HOL. As a workaround, I've forced 45 seconds into one of the "isabelle emacs" startup scripts, ignoring the Emacs user customization at that point (which is also a bit rude).
Change History (5)
comment:1 Changed 13 years ago by
comment:2 Changed 13 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | new → closed |
Committed suggested fix in CVS now, please reopen if this doesn't address problem.
comment:3 Changed 13 years ago by
| Resolution: | fixed |
|---|---|
| Status: | closed → reopened |
This solves the second half of the problem.
The first half is that the process termination itself seems to be too rude from the very start, i.e. Isabelle is killed instantaneously. As a side-effect /tmp/isabelle-johndoe4711/ directories are left behind, for example.
comment:5 Changed 13 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | reopened → closed |
Ah, I see, proof-shell-wait needed to think there was input pending. Fixed in CVS.
How about if we move the setting to be a prover-specific one (i.e., in pg-custom.el) and set a high default for Isabelle?