diff options
Diffstat (limited to 'html/projects/coqfile.html')
| -rw-r--r-- | html/projects/coqfile.html | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/html/projects/coqfile.html b/html/projects/coqfile.html new file mode 100644 index 00000000..03836398 --- /dev/null +++ b/html/projects/coqfile.html @@ -0,0 +1,20 @@ +<h2>Multiple file handling support for Coq</h2> +<p> +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. +</p> +<b>Skills:</b> + Some understanding of Coq implementation, co-operation with + the Coq developers to get any Coq modifications (if any) incorporated. + Some Emacs Lisp knowledge. +</p><p> +<b>Proposer:</b> +<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>. +</p> |