Open walck opened 1 month ago
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:
C-h C-v coq-prog-args
Ideally the containt of coq-prog-name
in both buffers would help too (if they are different).
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
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:
_CoqProject
fileCurrently 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?
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.
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.
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 :-).
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.
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
.
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.
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.
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.
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
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.