1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
<?php
require('functions.php3');
small_header("Proof General Projects");
?>
<p>
Here are some proposals for projects connected to Proof General.
</p>
<p>
The projects are designed as fairly self-contained contributions,
involving code development and possibly a portion of supporting
research. They would be ideal projects for interested students
or researchers.
</p>
<p>
The projects are divided into those which are specific to Proof
General, and those which would be useful more widely and do not depend
on Proof General. For more information on a project, click on its
title.
</p>
<h2>A. Projects involving Proof General</h2>
<ol>
<li><?php pgproject("coqpbp","Proof-by-pointing support for Coq") ?></li>
<li><?php pgproject("coqfile","Multiple file handling support for Coq") ?></li>
<li><?php pgproject("isapbp","Proof-by-pointing support for Isabelle") ?></li>
<li><?php pgproject("outline","Integrating block-structured development and outline mode") ?></li>
<li><?php pgproject("thybrowse","A Generic Theory Browser") ?></li>
<li><?php pgproject("pgml","Specification and tools for PGML") ?></li>
<li><?php pgproject("pgip","A New Protocol for Interactive Proof in Proof General") ?></li>
<li><?php pgproject("webreplay","A Web-based Proof Replayer for Proof General") ?></li>
<li><?php pgproject("test","A Test Harness and Test Suite for Proof General") ?></li>
<li><?php pgproject("hol","Proof General for HOL") ?></li>
<li><?php pgproject("acs","Implementing Atomic Command Sequences") ?></li>
</ol>
<h2>B. Projects not directly involving Proof General</h2>
<ol>
<li><?php pgproject("mm","Multiplexed Modes for Emacs") ?></li>
<li><?php pgproject("scrgen","Script General") ?></li>
<li><?php pgproject("corba","An Experimental CORBA binding for ML") ?></li>
<li><?php pgproject("reelcase","A ClearCase-like Configuration Management tool for Linux") ?></li>
</ol>
<p>
Some projects involve Emacs Lisp. This is the embedded programming
language inside Emacs. It is very easy to learn, since it is small,
has a good manual, and has an interactive interpreter. It is easy to
use, not least because of its <i>self-documenting</i> nature: each
variable or function is compiled together with documentation of its
purpose. (Other languages would do well to follow this). It also
has a powerful source-level debugger, <i>edebug</i>.
</p>
<!-- template for project pages -->
<!-- <h2> </h2> -->
<!-- <p> -->
<!-- </p> -->
<!-- <p> -->
<!-- <b>Skills:</b> -->
<!-- </p><p> -->
<!-- <b>Proposer:</b> -->
<!-- <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>. -->
<!-- </p> -->
<p>
If you are interested in working on any of these projects,
feel free to discuss with the project proposer or on the
<?php link_root("devel#develmail","developer's mailing list") ?>.
</p>
<p>
If you would like to use any of these ideas as a formal project
proposal for students at your institution, please feel free
but do <?php hlink("feedback.phtml","let us know ","Feedback form")?>
if some work is begun, to help coordinate efforts.
NB: the proposer of the project does not guarantee to be available for
formal supervision or intensive help with the project (but it may be
possible to find somebody else to do that).
</p>
<p>
If you would like to submit a project proposal
for an improvement or extension of Proof General,
please send an email or write a description on the
<?php hlink("feedback.phtml","web feedback form","Feedback form")?>.
Projects should be significant contributions rather than
incremental improvements (although we welcome the suggestion of those
too).
</p>
<?php
click_to_go_back();
footer();
?>
|
