No syntax highlighting at first lauch

[ckeller]

Hi

I am using the master branch of PG with GNU Emacs 26.3. I installed PG following the instructions at the beginning of the INSTALL file.

When opening a first .v file, PG starts normally (Loading /usr/share/emacs/site-lisp/post-el/post.el (source)...done in *Message*), I can process the file, but it is not syntax highlighted. Syntax highlighting starts working again when opening other files.

Thanks!

[Matafou]

Hi, I cannot reproduce with my 26.1. Can you give the complete content of your Messages buffer please?

[ckeller]

Sorry, the line I posted has indeed nothing to do with PG.

• *Messages* after opening a first file (some pieces replaced with ***):

Loading /etc/emacs/site-start.d/00debian.el (source)...done
Loading /etc/emacs/site-start.d/50a2ps.el (source)...done
Loading /etc/emacs/site-start.d/50agda.el (source)...done
Loading /etc/emacs/site-start.d/50auctex.el (source)...
Loading /usr/share/emacs/site-lisp/auctex.el (source)...done
Loading /usr/share/emacs/site-lisp/preview-latex.el (source)...done
Loading /etc/emacs/site-start.d/50auctex.el (source)...done
Loading /etc/emacs/site-start.d/50autoconf.el (source)...done
Loading /etc/emacs/site-start.d/50dictionaries-common.el (source)...
Loading debian-ispell...
Loading /var/cache/dictionaries-common/emacsen-ispell-default.el (source)...done
Loading debian-ispell...done
Loading /var/cache/dictionaries-common/emacsen-ispell-dicts.el (source)...done
Loading /etc/emacs/site-start.d/50dictionaries-common.el (source)...done
Loading /etc/emacs/site-start.d/50latexmk.el (source)...done
Loading /etc/emacs/site-start.d/50lilypond-data.el (source)...done
Loading /etc/emacs/site-start.d/50nethack-el.el (source)...done
Loading /etc/emacs/site-start.d/50ocaml-mode.el (source)...done
Loading /etc/emacs/site-start.d/50post-el.el (source)...done
Loading /etc/emacs/site-start.d/50python-docutils.el (source)...done
Loading /etc/emacs/site-start.d/51tuareg-mode.el (source)...done
Loading /etc/emacs/site-start.d/60agda-stdlib.el (source)...done
Loading quail/latin-ltx...done
Loading ‘ob-ref’: unescaped character literals `?(', `?)' detected!
Loading /usr/share/emacs/site-lisp/post-el/post.el (source)...
../../../../../../../../usr/share/emacs/site-lisp/post-el/post.el: ‘flet’ is an obsolete macro (as of 24.3); use either ‘cl-flet’ or ‘cl-letf’.
Loading /usr/share/emacs/site-lisp/post-el/post.el (source)...done
For information about GNU Emacs and the GNU system, type C-h C-a.
Coq project file detected: ***/_CoqProject
Package pc-select is obsolete!

• Addition after starting processing the file:

Coq project file detected: ***/_CoqProject.
The Coq Proof Assistant, version 8.8.2 (February 2020)
compiled on Feb 10 2020 12:19:45 with OCaml 4.07.1
Coq project file detected: ***/_CoqProject.
The Coq Proof Assistant, version 8.8.2 (February 2020)
compiled on Feb 10 2020 12:19:45 with OCaml 4.07.1
Starting: ***/coqtop -emacs ***
Hit M-x proof-layout-windows to reset layout
M-x proof-prf for goals; M-x proof-layout-windows refreshes [2 times]
Starting coq process... done.

[Matafou]

I cannot see anything that would explain what you are experiencing. I don't think the warning abot pc-select can be the problem but it is worth a try.

@cpitclaudel I know you use cutting edge versions of emacs. Are you using 26.3 version?

[ckeller]

I tried without pc-select and I face the same situation.

[cpitclaudel]

@Matafou I'm using something more recent, but I don't see that issue

[ckeller]

The problem did seem related to something else in my .emacs (removing the yes-or-no question when doing proof-shell-exit).