Proof General gets into a state where it doesn't know what + is.

[walck]

Hi folks,

When using Coq 8.19.1 with Proof General 4.6-git and Emacs 29.3,
I use C-c RET (proof-goto-point) to navigate throughout a .v
file. When I've been editing awesome1.v and then I start editing
awesome2.v, Proof General asks if I want to retract the proving I
did on awesome1.v, and I say yes. Sometimes (but not all the
time) after this, Proof General gets into a state where it
complains that it doesn't understand the first plus + sign in the
file. It gives the error

Error: Syntax error: '.' expected after [gallina] (in [vernac_aux]).

Since the first plus sign is very near the top of a file that had been
loading correctly, it basically won't load anything.

I have tried killing the Coq process with C-u C-c C-x,
but the issue remains until I restart Emacs.

Here is the content of the buffer *coq* if that helps to
understand the problem.

Welcome to Coq 8.19.1

<prompt>Coq < 1 || 0 < </prompt>Add Search Blacklist "Private_" "_subproof". 

<prompt>Coq < 2 || 0 < </prompt>Set Suggest Proof Using. 

<prompt>Coq < 3 || 0 < </prompt>Set Diffs "off". 

<prompt>Coq < 4 || 0 < </prompt>Set Printing Depth 50 . 

<prompt>Coq < 5 || 0 < </prompt>Set Printing Width 135.

<prompt>Coq < 6 || 0 < </prompt>Set Silent. 

<prompt>Coq < 7 || 0 < </prompt>Require Export Nat.

<prompt>Coq < 8 || 0 < </prompt>Theorem t_0_1_1_a : forall m n : nat, m + n = n + m.
Toplevel input, characters 40-41:
> Theorem t_0_1_1_a : forall m n : nat, m + n = n + m.
>                                         ^
Error: Syntax error: '.' expected after [gallina] (in [vernac_aux]).

<prompt>Coq < 8 || 0 < </prompt>

[Matafou]

Thanks for the report!
If the bug remains after coqtop is restarted then it can come only from the coqtop invokation itself.
Can you give the containt of awesome1.v please?
And most importantly the value of coq-prog-args in both buffers?
To get these values:

• go to the buffer
• hit C-h C-v coq-prog-args
• go to other bufffer and do the same

Ideally the containt of coq-prog-name in both buffers would help too (if they are different).

[walck]

The first file is called Nat.v and begins with the following code.

Theorem plus_zero : forall n : nat, n + 0 = n.
Proof.
  intros. induction n.
    reflexivity.
    simpl.  rewrite -> IHn.  reflexivity.
Qed.

The value of coq-prog-name is "coqtop".

The value of coq-prog-args is
("-topfile" "/home/scott/computer/DependentTypes/Coq/MathFromScratch/Nat.v" "-emacs" "-noinit")
Original value was nil

The second file is called Bridger0.v and begins with the following code.

Require Export Nat.

(* 0. Preliminaries *)

(* 0.1 The Natural Numbers *)

(* 0.1.1 Commutative laws *)

Theorem t_0_1_1_a : forall m n : nat, m + n = n + m.
Proof.
  exact add_comm.
Qed.

The value of coq-prog-name is "coqtop".

The value of coq-prog-args is
("-topfile" "/home/scott/computer/DependentTypes/Coq/MathFromScratch/Bridger0.v" "-emacs" "-noinit")
Original value was nil

[Matafou]

The option -noinit in coq-prog-args is passed to coqtop. It causes coqtop to be launched without the standard prelude. Since the notation for + is defined in Coq's standard prelude it explains the error.

Now we have to understand why the option -noinit ends up in your coq-prog-args for the two files.
How do you set this variable? There are several ways to do that:

• by a _CoqProject file
• by hand in emacs before starting coq
• by a file variable

Currently there is a mechanism to restart coqtop when a _CoqProject is detected. That said we could restart it systematically when switching files.

@erikmd @hendriktews do you a reason not to do that?

[Matafou]

The most probable explanation is that the first file needs -noinit and you set it via a _CoqProject, and the second file has no project file so options are left unchanged.

[erikmd]

Thanks @Matafou for your analysis!

That said we could restart it systematically when switching files. (...) a reason not to do that?

Indeed if opening the 2nd file directly succeeds, but not when switching to it from a "-noinit" file, there's something to reset indeed.

[Matafou]

I am not sure what is happening exactly, because -noinit should make the first file fail at first.
@walck we need a bit more investigation :-).

[Matafou]

But we should definitely restart coqtop: this is more robust than retracting as pointed out by Gaetan here.

At least to be correct we need to check if the options have changed (instead of just checking if there is a project fie) and restart coqtop if they have.

[walck]

I am not using a _CoqProject file and I can confirm that the -noinit option is not present when starting Proof General from a fresh Emacs. So I don't know how -noinit gets added to coq-prog-args.

[walck]

Wait I found something.

In .emacs I have

(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.
 '(package-selected-packages
   '(company-coq company magit-section lsp-mode flycheck f calibredb quack geiser markdown-mode mastodon proof-general helm wanderlust org org-edna racket-mode poker ledger-mode haskell-mode gnuplot-mode gnuplot gnugo gap-mode ess chess))
 '(safe-local-variable-values
   '((eval let
	   ((unimath-topdir
	     (expand-file-name
	      (locate-dominating-file buffer-file-name "UniMath"))))
	   (setq fill-column 100)
	   (make-local-variable 'coq-use-project-file)
	   (setq coq-use-project-file nil)
	   (make-local-variable 'coq-prog-args)
	   (setq coq-prog-args
		 `("-emacs" "-noinit" "-indices-matter" "-type-in-type" "-w" "-notation-overridden" "-Q" ,(concat unimath-topdir "UniMath")
		   "UniMath"))
	   (make-local-variable 'coq-prog-name)
	   (setq coq-prog-name
		 (concat unimath-topdir "sub/coq/bin/coqtop"))
	   (make-local-variable 'before-save-hook)

so apparently I am explicitly asking for -noinit.

Now I don't understand why -noinit is missing from the arg list with a fresh Emacs.

[Matafou]

I don't think so. The variable safe-local-variable-values only says that it safe to execute this piece of code.
This piece of code is probably in a file .dir-locals.el or in the file variables declared at the end of a file.

[Matafou]

I mean: this customization alone does not say that the option is set. It only says that it is allowed to do be set automatically by a file variable. It also indicates that you did it at least once.