Hi,
is anybody working on getting multiple file scripting to work for
coq?
>From my naive point it shouldn't be too difficult:
- proofgeneral catches Require commands and sends Locate Library
instead
- proofgeneral then checks if the returned file name and its
dependencies are up-to-date, possibly asking the user whether
to recompile
- when finished proofgeneral retracts the Locate Library and
issues the original Require command
A different possibility would be to patch coqtop to ask for
confirmation, whenever it is loading a library file.
Bye,
Hendrik
=================================================================
Hendrik Tews Postdoc in the Operating Systems Group
at TU Dresden, Germany
Telefon: +49 351 46338350
www: www.askra.de
e-mail: t...@os.inf.tu-dresden.de
=================================================================
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
