Proof General complaining script incomplete if running 2 scripts at the same time

Question

It seems like PG doesn't allow running 2 scripts at the same time. The moment attempting to do this, Emacs will prompt and ask to retract the other file. Sometimes, scripts are nontrivial to rerun. Is there any way to actually run 2(or more) scripts in a single Emacs instance? I don't think the coqide gui shipped with coq has no such problem.

Answer 1

It does not seem possible with the current version of PG. Here is an excerpt from the Proof General manual:

However, you cannot have more than one buffer where only a fraction of the proof script contains a locked region. Before you can employ script management in another proof script buffer, you must either fully assert or retract the current script buffer.

Answer 2

My understanding is that the current Proof General has too many global variables in use to allow multiple script instances to be executed simultaneously. Apparently there is some work in progress to fix this by encapsulating the global state, but I have no idea when it might be completed.