Stream: Coq users

Topic: Proof General freezes after I-search


view this post on Zulip Yosuke Ito (Mar 19 2021 at 12:18):

Dear Coq users,
I'm using Proof General on emacs, and facing a problem. If I do "proof-assert-next-command-interactive" C-c C-n after using "I-search" C-s, then the proof process gets stuck and never ends. Does anyone experienced the same problem? I hope to get some tips to fix it.
I use macOS Big Sur, GNU Emacs 27.1, Proof General Version 4.5-git, Company-Coq.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 19 2021 at 15:14):

Dear @Yosuke Ito , I have no such problem, seems strange. Emacs is a bit tricky due to user-config, I'd suggest you report the issue at https://github.com/ProofGeneral/PG/issues where they should be able to help you debug it

view this post on Zulip Yosuke Ito (Mar 20 2021 at 00:12):

OK. I'll send a bug report. Thank you very much for your help!


Last updated: Feb 06 2023 at 11:03 UTC