blob: 35d48eb1c923232499639f4a344f1a2a3826b2ed (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
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>
|
