diff options
Diffstat (limited to 'html/projects/coqfile.html')
| -rw-r--r-- | html/projects/coqfile.html | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/html/projects/coqfile.html b/html/projects/coqfile.html new file mode 100644 index 00000000..35d48eb1 --- /dev/null +++ b/html/projects/coqfile.html @@ -0,0 +1,22 @@ +<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 mean that Proof General can make use of the file-level primitives +of Coq, so that the user doesn't have to escape the interface, +or carefully load each file and its dependencies. This also means that +complete proof scripts will not so often need to be interpreted by +Proof General, solving one of the present bottlenecks with using +Coq Proof General. +</p> +<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> |