indentation takes a long time, maybe forever

[jonleivent]

Apparently, some recent change has made indentation take a very long time to do a single tab or newline-and-indent. I'm not even sure how long -as I have to stop it. It might just be looping forever.

The problem doesn't always occur, only after certain constructs. I will attempt to isolate it.

I'm using version c480238 with emacs 24.4.1.

[jonleivent]

Here's a simple example:

Require Import List.

Variable A : Type.

Lemma lnenil : forall (d : A)(lf rf : list A), (lf++d::rf)%list <> nil. Proof. intros. intro H. eapply app_eq_nil in H as [? ?]. discriminate. Qed.

Go to the end (line after the Qed) and hit tab.

[jonleivent]

The problem does not exist in 22c3951.

So, apparently Pierre's "Speeding up indentation code (smie lexer)" change is to blame?

[Matafou]

Mmh strangely enough I don't have the problem at the same line...

I am currently working on speeding up indentation so I will try to fix tonight. Otherwise I will backtrack my previous "fix".

That code is definitely extremely fragile.

P.

2015-12-04 21:11 GMT+01:00 Jonathan Leivent notifications@github.com:

The problem does not exist in 22c3951 https://github.com/ProofGeneral/PG/commit/22c3951cfdf4938fa6df7368daed7bead05e4592 .

So, apparently Pierre's "Speeding up indentation code (smie lexer)" change is to blame?

— Reply to this email directly or view it on GitHub https://github.com/ProofGeneral/PG/issues/15#issuecomment-162069824.

[jonleivent]

That is surprising - my .emacs is very minimal:

(load-file "/home/jil/git/PG/generic/proof-site.elc") (custom-set-variables ;; custom-set-variables was added by Custom. ;; If you edit it by hand, you could mess it up, so be careful. ;; Your init file should contain only one such instance. ;; If there is more than one, they won't work right. '(case-fold-search nil) '(confirm-kill-emacs (quote y-or-n-p)) '(coq-auto-adapt-printing-width nil) '(coq-compile-before-require t) '(coq-compiler "/home/jil/git/coq/bin/coqc") '(coq-dependency-analyzer "/home/jil/git/coq/bin/coqdep") '(coq-prog-name "/home/jil/git/coq/bin/coqtop") '(coq-toolbar-entries (quote ((retract "Retract Buffer" "Retract (undo) whole buffer" t t) (interrupt "Interrupt Prover" "Interrupt the proof assistant" t t) (undo "Undo Step" "Undo the previous proof command" t t) (delete "Delete Step" "Delete the last proof command" nil t) (next "Next Step" "Process the next proof command" t t) (use "Use Buffer" "Process whole buffer" t t) (goto "Goto Point" "Process or undo to the cursor position" t t) (home "Goto Locked End" "Goto end of the last command processed" t t) (find "Find Theorems" "Find theorems" t proof-find-theorems-command) (info "Identifier Info" "Information about identifier" t proof-query-identifier-command) (command "Issue Command" "Issue a non-scripting command" t t) (restart "Restart Scripting" "Restart scripting (clear all locked regions)" t t) (visibility "Toggle Visibility" "Show or hide hidden proofs" nil t) (help nil "Proof General manual" t t)))) '(proof-multiple-frames-enable t) '(proof-script-fly-past-comments t) '(proof-splash-enable nil) '(recentf-mode t) '(show-paren-mode t) '(uniquify-buffer-name-style nil nil (uniquify))) (custom-set-faces ;; custom-set-faces was added by Custom. ;; If you edit it by hand, you could mess it up, so be careful. ;; Your init file should contain only one such instance. ;; If there is more than one, they won't work right. '(default ((t (:family "Inconsolata" :foundry "unknown" :slant normal :weight normal :height 120 :width normal)))) '(coq-question-mark-face ((t (:background "yellow" :foreground "magenta" :box (:line-width 1 :color "grey75" :style pressed-button))))))

I have just switched back to c480238, and can replicate the problem easily with the test case.

[jonleivent]

I put emacs into the mode where it enters the debugger on ^G, and got the stack below when hitting tab after that last Qed line. I had to delete a lot of the binary info in the stack in order for it to be pastable - hopefully it is still useful.

Debugger entered--Lisp error: (quit) coq-dot-friend-p("forall") coq-smie-search-token-forward(("." ":=") nil (("with" ":=" "signature") ("let" . "in"))) coq-lonely-:=-in-this-command() coq-smie-detect-goal-command() coq-smie-.-deambiguate() smie-next-sexp smie-backward-sexp(".") smie-indent-keyword() run-hook-with-args-until-success(smie-indent-keyword) smie-indent-calculate() smie-indent-virtual() smie-indent-after-keyword() run-hook-with-args-until-success(smie-indent-after-keyword) smie-indent-calculate() smie-indent-line() indent-for-tab-command(nil) call-interactively(indent-for-tab-command nil nil) command-execute(indent-for-tab-command)

[Matafou]

this should be fixed by commit 4a4a8c5. Please try and reopen if you see something wrong.

Some slowdowns that used to happen when indenting big files (and big comments) should also be fixed. Some slowdowns are still there but need heavy redesign of the indentation code.

FTR there are two solutions for having something reasonable for indentation: either rely on coq and its ide protocol (but then no indentation without coqtop running), either have a 2-layers (or maybe 3-layers) smie design. Indenting first lines of a command, first line of a tactic and inside a tacitc/commands are 3 different jobs and we should use 3 different grammars. With some help of Stefan Monnier that would not be so difficult I guess. Especially because detecting tactics is easy: they start with lower cases.

[jonleivent]

The fix appears to work - at least in the limited cases I've tried so far. Thanks!

By the way - tactics don't always start with lower cases:

Ltac Mytac := ....

[Matafou]

2015-12-07 16:54 GMT+01:00 Jonathan Leivent notifications@github.com:

The fix appears to work - at least in the limited cases I've tried so far. Thanks!

By the way - tactics don't always start with lower cases:

Ltac Mytac := ....

Yes, we should try to be robust to this. P.