I am still under the impression, that we slightly talk cross each
other. Let me therefore elaborate on two points:
1. Differences between Isabelle and coq wrt multiple file
2. Various aspects of multiple file scripting.

1. Differences between Isabelle and coq

Assume file B depends on file A. The main difference is that when
you start scripting B Isabelle reads the sources of A, while
ProofGeneral reads the compiled file A.vo.

Assume you changed something in A and you want now continue the
work in B. For Isabelle it is fine to script file A until the end
and then start scripting B.

For coq, when you switch from A to B you have to retract to a
clean starting state, regardless whether you scripted file A to
the end or not. Then, when you want your changes of A to be
visible in B you have to save and recompile A before the command
"Require A" in B is processed.

Another difference is that in Isabelle the dependencies are in
the theory header. In coq dependencies are expressed with the
"Require", which can appear at arbitrary positions, possibly in
the middle of the file.

2. Aspects of multiple file scripting

Multiple file scripting has certainly several aspects and
features. I believe some bits of confusion come from the fact
that we focus on different features. 

Assume different files A and B, where B might or might not depend
on A.

Feature 1: When you switch from A to B in ProofGeneral the prover
keeps a consistent state.

For coq this means ProofGeneral has to put coq into the starting

Assume now B depends on A, and you are scripting in B.

Feature 2: When you now visit file A, ProofGeneral should lock A
to indicate that the prover has processed its contents.

  I must say I am not really interested in Feature 2. I usually
  know the dependencies of my projects. And for coq, it is not
  important to protect file A against unintended changes,
  because you can always undo in emacs and then continue with the
  previously compiled file A.vo. For Isabelle Feature 2 is more
  important, because you can easily loose half an hour when you
  unintentionally insert a space in A.

Still assuming B depends on A..

Feature 3: When you change A, development in B should be

For coq, Feature 3 is implied by Feature 1.

Still assuming B depends on A..

Feature 4: When the user switches to B after changing A, the
prover should keep a consistent state and the changes in A should
be visible in B.

For coq, switching to B requires to retract into the initial
state, before processing the first line of B. Further, before the
command "Require A" in B is processed, file A.v must be recompiled
into A.vo.

Still assuming B depends on A..

Feature 5: When the user is scripting in B and processes those
lines that establish the dependency on A, then any update of (the
sources of) A is detected and properly processed. (All this
happens regardless of whether file A is opened in ProofGeneral or
has been changed through ProofGeneral.)

   I am mainly interested in Features 4, 5 and also 1. 

Still assuming B depends on A..

Feature 6: When the user is scripting in B changes in the sources
of A (possibly cause by external programs) are detected and
ProofGeneral retracts until before those lines that establish the
dependency on A.

  This feature does not make much sense IMO, I am not even
  thinking about it.

I hope I did not miss any possible features. To clarify, I am
interested in the features 1, 4 and 5 (and 3, which is implied by
1 for coq). 

I am not interested in Feature 2, but maybe we get it as a simple
side effect.

I hope this clarifies the discussion a bit.


ProofGeneral-devel mailing list

Reply via email to