Coq Proof General does not yet handle script management across file boundaries, as do the LEGO and Isabelle versions. Script management for multiple files means that whenever a file is viewed in the editor, it is locked if it has been loaded into the current Coq session. It may also mean that one can some file-level primitives of Coq, rather than loading each file manually in the interface. This means that complete proof scripts will not usually need to be parsed by Proof General, solving one of the present problems with using Coq Proof General.
Skills: Some understanding of Coq implementation, co-operation with the Coq developers to get any Coq modifications (if any) incorporated. Some Emacs Lisp knowledge.Proposer: David Aspinall.