blob: 281c043dc07dd320418e67638cd25eec701fc03b (
plain)
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
|
<?php
require('functions.php3');
small_header("Proof General Project Proposals");
?>
<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 small amount of supporting
research. They would be ideal projects for interested students
or researchers.
</p>
<ul>
<li><b>Proof-by-pointing support for Coq</b>
<p>
Coq already has sophisticated notions of proof-by-pointing,
and old work on support for Proof General may be helpful.
We want to integrate with the latest version of Coq's
proof-by-pointing, possibly improving Proof General's
support along the way.
</p>
<p>
<b>Skills:</b>
Some understanding of Coq implementation, co-operation with
the Coq developers to get any Coq modifications (if any) incorporated.
Minimal Emacs Lisp knowledge.
</p><p>
<b>Proposer:</b>
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
</p>
<li><b>Proof-by-pointing support for Isabelle</b>
<p>
Isabelle has a sophisticated concrete syntax mechanism which makes it
difficult to add annotations to connect the displayed output back to
the internal abstract syntax. This issue needs to be solved to
support proof-by-pointing (and other features) in Isabelle.
A
<a href="http://www.informatik.uni-bremen.de/~bu/isa_contrib/isabelle.html">
patch by Burkhart Wolff</a>
providing term structure annotations for a previous release of
Isabelle may be useful here. To implement proof-by-pointing itself,
tactics using the gesture information must be written.
</p>
<p>
<b>Skills:</b>
Some understanding of Isabelle implementation,
co-operation with the Isabelle developers to get
Isabelle modifications incorporated.
Skill in writing Isabelle tactics.
Minimal Emacs Lisp knowledge.
</p><p>
<b>Proposer:</b>
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
</p>
</li>
</ul>
<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 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();
?>
|
