search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 88 forks source link

Why retracting before restarting coqtop? #770

Open Matafou opened 5 months ago

Matafou commented 5 months ago

Following a remark by @SkySkimmer.

Currently when the user asks for scripting a different file than the current one PG does the following things:

  1. ask for retracting the current one (which is ok),
  2. then retract the file (which may be costly or even fail as shown by the initial remark),
  3. and finally kills coqtop and restarts it on the new file (re-detecting options etc).

Step 2. seems fragile and useless. Asking before changing the scripting buffer (step 1) is of course important, but then jumping to step 3 seems ok. In particular step 3 removes all locks on buffers and relaunching scripting mode re-locks what is needed.

Any reason not to propose a PR in this direction?

hendriktews commented 5 months ago

I introduced killing coqtop with multiple file support around 2012, because at that time required files could not be unloaded. I would guess retracting is generic behavior, maybe caused by killing all spans in the current buffer. I don't see any reason for not shortcutting the procedure. Does coqtop reliably unload all required stuff (including ML plugins) nowadays? If yes, since when? May we can even abandon the killing.

Matafou commented 5 months ago

Actually as explained by @SkySkimmer there are reasons to kill coqtop. Requires are still not correctly unloaded.

https://coq.zulipchat.com/#narrow/stream/304019-Proof-General-users/topic/Restarting.20ProofGeneral/near/442904710

Hence my suggestion is the opposite: since we need to kill coqtop why first try to retract the file?

hendriktews commented 5 months ago

I don't see a reason to retract before kill. I have not investigated why this is happening at all.