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
|
<?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>
For more information on a project, click on its title.
</p>
<ul>
<li><?php pgproject("coqpbp","Proof-by-pointing 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("mm","Multiplexed Modes for Emacs") ?></li>
<li><?php pgproject("scrgen","Script General") ?></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>
</ul>
<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).
</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>
Note: the proposer of the project is just that; he or she 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. Contact the project proposer first for more details.
</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.
</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();
?>
|
