The Coq mailing list

[Bruno Barras <Bruno.Barras AT inria.fr>]

Hello,

I had the same problem when formalizing the metatheory of Pure Type
Systems, which is also a heavily parametric developpement. Here is how
I managed the problem:

Everything is in one single module: files are not compiled in modules,
but just included with Load:

Section Main.

  (* The parameters *)
  Variables ....

  (* The whole proof is cut into separate files *)
  Load file1.
  Load file2.
  ...

End Main.

I avoided recompiling the beginning every day by saving the state of the
machine every evenning:

Save State toto.
Write States "titi".

The last command writes a file titi.coq containing a state called toto.
The day after, you can launch Coq with 

coqtop -is titi.coq

Coq reads the file titi.coq and restores the last saved state. So, it is
not necessary to do

Restore State toto.

Then, you can resume your proofs where you stopped the day before.

It worked fine for me. Of course, it would be better if there was
parametric modules. But it requires a lot of work to implement the
proposal of Judicael Courant's PhD in the current implementation of Coq.

> Now my question is "why is it necessary to change variables into
> parameters at global level in compilation?".

A variable at global level would never be discharged because the
discharge operation is performed only when closing a section. That's
why variables at global level are considered as parameters.

In the implementation, module can depend only on other modules. Therefore,
they cannot depend on variables. An evidence of this fact is that you
cannot compile a module when there are not only modules in the context;
Compile Module would complain if you tried to compile a module in an
opened section.

Cheers,

  Bruno.