Why retracting before restarting coqtop?

[Matafou]

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]

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]

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]

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