cannot change buffer when Flycheck Error Messages is shown

[fpvandoorn]

Steps to reproduce:

0. Make sure the file standard.lean is not opened in a buffer in Emacs
1. Create a file test.lean in the library folder, containing

variable P : nat → Type

example : P (nat.of_num 1000) :=
begin
  esimp [nat.of_num]
end

2. In Emacs, move your point over end so that the *Flycheck Error Messages* buffer is shown.
3. Try to open standard.lean using C-x C-f standard.lean.
   Result: The buffer standard.lean is opened, but the current buffer has not changed to standard.lean (it is still test.lean)
4. Executing C-x C-f standard.lean again works as expected, because standard.lean is now open.

(The fact that you open a .lean/.hlean file seems to matter, opening other files seems to work normally).

Jakob and I noticed this behavior already for a while, but we couldn't consistently reproduce it before.

[leodemoura]

@soonhokong I managed to reproduce the problem. It is super weird.
If we try multiple times, it eventually succeeds (at least for me).
If we close *Flycheck Error Messages* buffer, it also succeeds.
Any ideas?

[soonhokong]

@fpvandoorn and @leodemoura, I'll take a look at this one.

[soonhokong]

I can reproduce the problem as well. I believe this is an upstream problem because the same problem happens when I try to open a C++ file. I will open an issue in flycheck repository.

[soonhokong]

I opened an issue at flycheck/flycheck#648.

[soonhokong]

@fpvandoorn and @leodemoura, I have struggled with this issue. Today, I found a way to reproduce with a fresh emacs (emacs -q) and reported it to the flycheck author. I'll keep you posted the response.

He also suggested many points for improvements. I'll update lean-flycheck.el file by following them.

[leodemoura]

@soonhokong Should we close this one?

[soonhokong]

@leodemoura, I believe that this is an upstream issue. I just sent this video to the author of flycheck-mode. I hope this help him fix the problem.

[leodemoura]

Thanks!

[soonhokong]

@leodemoura and @fpvandoorn, flycheck team confirmed that they can reproduce this problem without Lean-mode. See flycheck/flycheck#648 (comment). However, it seems that it will take some time for them to fix it.

@leodemoura, please feel free to close this issue here. I'll re-open it when I hear anything from the flycheck team

[leodemoura]

@soonhokong Thanks for investigating this issue!

[soonhokong]

The problem is fixed by the flycheck team. I'll write another comment when the patch is arrived at MELPA.

[fpvandoorn]

Great! Thanks for your efforts to create an upstream example!

[soonhokong]

@fpvandoorn, the latest version of flycheck (20151216) is now available via MELPA. Please upgrade your flycheck and check you don't have this problem anymore.

[fpvandoorn]

I updated flycheck and the problem is indeed solved. Thanks!