+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. +
++Skills: + Some understanding of Coq implementation, co-operation with + the Coq developers to get any Coq modifications (if any) incorporated. + Minimal Emacs Lisp knowledge. +
+Proposer: +David Aspinall. +
diff --git a/html/projects/isapbp.html b/html/projects/isapbp.html new file mode 100644 index 00000000..c08ea85e --- /dev/null +++ b/html/projects/isapbp.html @@ -0,0 +1,25 @@ ++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 + +patch by Burkhart Wolff +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. +
++Skills: + 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. +
+Proposer: +David Aspinall. +
+ diff --git a/html/projects/mm.html b/html/projects/mm.html new file mode 100644 index 00000000..d7bf6954 --- /dev/null +++ b/html/projects/mm.html @@ -0,0 +1,23 @@ ++Emacs has a mechanism for customizing the editing behaviour of buffers +based on their major mode. A buffer can only have one major +mode, but in literate styles of programming and proving we want to mix +program text with documentation in a single file. A way of +multiplexing major modes is needed, so that different regions of a +buffer can be edited in different modes. One approach may be to use +"views" onto untangled buffers, although it isn't clear how search and +replace, etc, should behave in this case. +
+Emacs hackers may already have worked on this problem and solved it +sufficiently well (does anybody know?), in which case this project +might degenerate into applying the work for Coq and Isabelle/Isar, as +a feasibility demonstration. +
+Skills: +A passion for Emacs and Emacs Lisp. +
+Proposer: +David Aspinall. +
+ diff --git a/html/projects/outline.html b/html/projects/outline.html new file mode 100644 index 00000000..67680b8f --- /dev/null +++ b/html/projects/outline.html @@ -0,0 +1,26 @@ ++Emacs already provides powerful outline facilities (cf. the +outl-minor-mode setup for the well-known auc-tex package). +Similarly, proof systems such as Isabelle/Isar are inherently based on +block-structured proof texts, with compositional proof checking. +
+But Proof General currently offers a mostly linear model of +incremental script management. The aim of this project is to extend that +model to a hierarchic one: e.g. sub-proofs could be suppressed in the +presentation, or even temporarily suspended (to achieve top-down +development). +
+Outline support would be useful for the large scale structure of formal +developments as well, e.g. support the basic arrangement into logical +section (cf. Coq), or even just traditional layout-based ones (cf. LaTeX). +
++Skills: +Some understanding of the workings of Emacs outline mode and Proof +General script management. Good portion of Emacs lisp knowledge. +
+Proposer: +Markus Wenzel. +
+ diff --git a/html/projects/pgip.html b/html/projects/pgip.html new file mode 100644 index 00000000..22cc654b --- /dev/null +++ b/html/projects/pgip.html @@ -0,0 +1,21 @@ ++PGIP is a protocol for interactive proof to be used in the next +version of Proof General. It is based around the present protocol, +but implemented with a standard collection of messages rather than +different messages for different proof assistants. An outline of PGIP +is given in the white paper. A +first implementation of PGIP will consist of (1) a filter (or +modification of the output routines) for an existing proof assistant, +which could be implemented in perl or some other language; and (2) a +new backend for Proof General in Emacs, which configures it for PGIP. +
++Skills: +Interest in interactive proof and basic understanding +of interaction mechanisms with at least one of +LEGO, Coq, Isabelle. Programmming in Emacs Lisp. +
+Proposer: +David Aspinall. +
diff --git a/html/projects/pgml.html b/html/projects/pgml.html new file mode 100644 index 00000000..52b3d3f1 --- /dev/null +++ b/html/projects/pgml.html @@ -0,0 +1,24 @@ ++PGML is the proposed logical markup language for future versions of +Proof General. The basic version legitimizes the present markup +scheme which is used by Proof General (based on 8-bit characters). +Ideas for PGML are described in the white paper +here, but no complete description or +DTD is given there. This project is to specify PGML using XML or SGML, +and develop some tools for using it. Various tools are desirable, +including: (1) a display tool which displays PGML inside Emacs, or +converts it to HTML for display by a web browser; (2) a filter or +revised version of LEGO which converts its 8-bit markup into PGML, for +testing purposes. +
++Skills: +Understanding of markup languages and tools for using and specifying them. +Interest in representation of mathematical content. +Necessary programming skills. +
+Proposer: +David Aspinall. +
+ diff --git a/html/projects/scrgen.html b/html/projects/scrgen.html new file mode 100644 index 00000000..d65b477f --- /dev/null +++ b/html/projects/scrgen.html @@ -0,0 +1,26 @@ ++Proof General is based around a core system of script management +for proof scripts. But the idea of script management is not +restricted to proof assistants, it makes sense for many interactive +scripting languages. It deserves to be better known and used. +A worthwhile project would be to rewrite the core script management +features of Proof General so that they could work for arbitrary +interactive scripting languages, and instantiate to Proof General as +well as languages such as ML, Haskell, LISP, Scheme, Python, and +even Emacs Lisp itself. +
++An alternative version of this project is to implement a +generic basis for script management which does not depend on +Emacs, but uses a similar protocol to communicate with other +text editors or display widgets. This could be implemented in +SML, OCaml, Java, C++, or any other suitable language. +
+Skills: +Proficient Emacs Lisp (or other programming language), +knowledge of scripting languages desirable. +
+Proposer: +David Aspinall. +
diff --git a/html/projects/test.html b/html/projects/test.html new file mode 100644 index 00000000..f9d5ecf0 --- /dev/null +++ b/html/projects/test.html @@ -0,0 +1,24 @@ ++As Proof General becomes a more complex system, we badly need some way +of performing automatic functional testing, to ensure that changes and +extensions preserve functional correctness. Although classical +testing of interfaces involves manually following a checklist of +actions and observations, it should be straightforward to automate +this using Emacs Lisp. Interactive actions can be simulated by +certain function calls, and their results can be determined by +examining the contents of the edit buffers. This project proposes the +design and implementation of a test harness and accompanying test +suite to test some of the core functions of Proof General. +Ultimately, the tests should be run as part of the build process +before each development release is allowed to go ahead. +
++Skills: +An interesting in testing user interfaces. +Basic knowledge of Emacs Lisp. +
+Proposer: +David Aspinall. +
+ diff --git a/html/projects/thybrowse.html b/html/projects/thybrowse.html new file mode 100644 index 00000000..bb081fc0 --- /dev/null +++ b/html/projects/thybrowse.html @@ -0,0 +1,32 @@ ++Proof General has very limited mechanisms for helping the user find +theorems and definitions during a proof. It has notion of displaying +a "current context" for a proof, and configuration with a proof +engine command for searching for theorems. It would be useful to +extend these facilities with a theory browser for investigating +the theories currently defined in a running proof assistant. This +involves designing a small protocol to communicate with the proof +assistant and a generic way of displaying theories which have +different aspects from system to system. A way which would +fit in well with Emacs would be to use a dired-like +buffer. +
++An alternative version of this project would be to write a standalone +theory browser which uses an extension of the forthcoming Proof +General standardized protocol for interaction (see white paper here). This could be implemented in +Java, or in a functional language, Perl, C or C++, so long as a nice +toolkit is chosen (Qt or GTK). +
++Skills: +Interface programming skills. +Basic understanding of what theories are for several different proof +assistants. +
+Proposer: +David Aspinall. +
+ diff --git a/html/projects/webreplay.html b/html/projects/webreplay.html new file mode 100644 index 00000000..1754e2df --- /dev/null +++ b/html/projects/webreplay.html @@ -0,0 +1,24 @@ ++One of the nice features of Proof General is that it is very easy to +replay existing proofs, by mouse clicks alone. No low-level +understanding of a proof assistant is needed to step through proofs. +We would like to have a web-based version of Proof General which +allowed for this proof replay (at least), perhaps running a proof +assistant remotely. The main aspect is to implement an engine for +script management (colouring of lines of files), displaying in a web +browser, sending lines to a proof assistant process, and displaying the +results. Ideally, the ideas for new standard protocols for Proof +General in the white paper would +be followed. +
++Skills: +Strong web programming skills using scripting languages, +dynamic HTML, etc. +
+Proposer: +David Aspinall. +
+ + -- cgit v1.2.3