1.1 --- a/doc-src/isac/CTP-userinterfaces.tex Tue Jan 11 08:10:06 2011 +0100
1.2 +++ b/doc-src/isac/CTP-userinterfaces.tex Tue Jan 11 13:35:03 2011 +0100
1.3 @@ -56,9 +56,9 @@
1.4 %\cite{pl:milner97}
1.5 %for developing CTP
1.6 \subsubsection{Standard ML}
1.7 -Standard ML is a general-purpose, modular, functional programming language. \cite{pl:milner97}
1.8 +Standard ML is a general-purpose, modular, functional programming language \cite{pl:milner97}.
1.9 Programs written in Standard ML consist of expressions to be evaluated, as opposed to statements or commands.
1.10 -Functional programming languages constitude a ???? very differnt of object orientated languages, see Sect. \ref{ml-users}. ML originated from the LCF-project(Logic for Computable Functions)\cite{meta-Ml}, where it had been developed as a meta language. Since ML has been standardised this family of language is called Standard ML. Important for the logical foundation of SML is the $\lambda$-calculus.
1.11 +Functional programming languages constitude a family very differnt of object orientated languages, see Sect. \ref{ml-users}. ML originated from the LCF-project(Logic for Computable Functions)\cite{meta-Ml}, where it had been developed as a meta language. Since ML has been standardised this family of language is called Standard ML. Important for the logical foundation of SML is the $\lambda$-calculus.
1.12 %http://en.wikipedia.org/wiki/Standard_M
1.13 \subsubsection{Coq}
1.14 Coq is an interactive theorem prover, developed in France.
1.15 @@ -66,11 +66,9 @@
1.16 It has the ability to express mathematical assertions and check proof of mathematical assertions.
1.17 Furthermore Coq includes automatic theorem proving tactics and decision procedures.
1.18 Properties, programs and proofs are written a functional programming language called the Calculus of Inductive Constructions (CIC).
1.19 -Proof development in Coq is done through a language of tactics that allows a user-guided proof process.\cite{coq1999}
1.20 -
1.21 +Proof development in Coq is done through a language of tactics that allows a user-guided proof process \cite{coq1999}.
1.22 Another feature of Coq is “that it can automatically extract executable programs from specifications, as either Objective Caml
1.23 or Haskell source code.“
1.24 -
1.25 There are many easy-to-read introductions to Coq \footnote{http://coq.inria.fr/a-short-introduction-to-coq} on the internet.
1.26 \subsubsection{Isabelle}
1.27 Isabelle is an interactive theorem proving framework for high-level natural deduction proofs \cite{Paulson:Isa94}, written in Standard ML.
1.28 @@ -78,11 +76,11 @@
1.29 and Université Paris-Sud. Isabelle is called a framework, because it implements serveral object logics.
1.30 The most widespread logic of Isabelle is Isabelle/HOL, short for higher-order logic.
1.31 Isabelle/HOL includes several specification tools, e.g. for datatypes, inductive definitions and functions with complex pattern matching.
1.32 -Proofs are written in the structured proof language Isar.\cite{wenzel:isar} Isabelle implements several tools, e.g. a reasoner, a simplifier and powerful automatic provers(Slegehammer), increase the user's productivity in theorem proving.
1.33 +Proofs are written in the structured proof language Isar \cite{wenzel:isar}.Isabelle implements several tools, e.g. a reasoner, a simplifier and powerful automatic provers(Sledgehammer), increase the user's productivity in theorem proving.
1.34 Isabelle provides notational support: new notations can be introduced, using normal mathematical symbols.
1.35 Definitions and proofs may include LaTeX source, from which Isabelle can automatically generate typeset documents.
1.36 -Isabelle/HOL allows to turn executable specifications directly into code in SML, OCaml, and Haskell.\cite{Haftmann-Nipkow:2010:code}
1.37 -(http://www.cl.cam.ac.uk/research/hvg/Isabelle/overview.html)
1.38 +Isabelle/HOL allows to turn executable specifications directly into code in SML, OCaml, and Haskell \cite{Haftmann-Nipkow:2010:code}.
1.39 +%(http://www.cl.cam.ac.uk/research/hvg/Isabelle/overview.html)
1.40 \subsection{Userinterfaces for CTP: Coq and Isabelle}\label{gui-coq-isa}
1.41 % CoqIDE, ..
1.42 % http://coq.inria.fr/what-is-coq?q=node/57\\
1.43 @@ -92,14 +90,13 @@
1.44 % http://proofgeneral.inf.ed.ac.uk/\\
1.45 % emacs stone age ?
1.46 \subsubsection{Coq Integrated Development Environment}
1.47 -CoqIde is a graphical interface for Coq. It is written in Ocaml. (http://coq.inria.fr/cocorico/CoqIde)
1.48 +CoqIDE\footnote{http://coq.inria.fr/V8.1/refman/Reference-Manual016.html}, short for Coq Integrated Development Environment, is a graphical interface for Coq. It is written in Ocaml.
1.49 Its main purpose is to allow the user to navigate forward and backward into a Coq vernacular file,
1.50 executing corresponding commands or undoing them respectively.
1.51 There are several buffers for helping to write proof scripts.
1.52 Among all these buffers, there is always one which is the current running buffer, whose name is displayed on a green background,
1.53 -which is the one where Coq commands are currently executed.
1.54 -Buffers may be edited as in any text editor, and classical basic editing commands (Copy/Paste, ...) are available.
1.55 -CoqIde provides also a feedback system for the user.
1.56 +which is the one where Coq commands are currently executed.
1.57 +CoqIDE provides also a feedback system for the user.
1.58 Therefore the background is green when a command succeeds, otherwise an errormessage is displayed in the message window and the error location is underlined red.
1.59 CoqIDE offers only basic editing commands, therefore it is possible to launch another more sophisticated text editor.
1.60 Furthermore CoqIde provides a proof wizard “for automatically trying to solve the current goal using simple tactics.”
1.61 @@ -115,38 +112,37 @@
1.62 \end{figure}
1.63
1.64
1.65 -(http://coq.inria.fr/V8.1/refman/Reference-Manual016.html)
1.66 +%(http://coq.inria.fr/V8.1/refman/Reference-Manual016.html)
1.67 \subsubsection{Proof General for Isabelle}
1.68 -Proof General is a generic front-end for proof assistants, based on the customizable text editor Emacs.
1.69 -It has been developed at the University of Edinburgh with contributions from other sites.
1.70 -Proof General comes ready-to-go for these proof assistants: Isabelle, Coq, PhoX, LEGO.
1.71 -Proof General is used to write proof scripts. A Proof Script is a sequence of commands sent to theorem prover.
1.72 -The communication between the user and the theorem prover takes place via two or more Emacs text widgets.
1.73 -Therefore the user sees only the output from the latest proof step.(proofgeneral.ps.gz)
1.74 +Proof General is a generic front-end for proof assistants \cite{aspinall}, based on the text editor Emacs.
1.75 +It has been developed at the University of Edinburgh with contributions from other sites.
1.76 +Proof General supports the following proof assistants: Isabelle, Coq, PhoX, LEGO.
1.77 +It is used to write proof scripts. A Proof Script is a sequence of commands sent to theorem prover.
1.78 +The communication between the user and the theorem prover takes place via two or more Emacs text widgets.
1.79 +Therefore the user sees only the output from the latest proof step.
1.80
1.81
1.82 -Isabelle/Isar Proof General has full support for multiple file scripting, with dependencies between theories communicated between Isabelle and Proof General.
1.83 +Isabelle/Isar\footnote{http://proofgeneral.inf.ed.ac.uk/} Proof General has full support for multiple file scripting, with dependencies between theories communicated between Isabelle and Proof General.
1.84 There is full support for Unicode Tokens, using the Isabelle print mode for X Symbol tokens. Many Isabelle theories have X Symbol syntax already defined
1.85 and it's easy to add to your own theories.
1.86 -(http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=releases%2FProofGeneral%2Fisar%2FREADME)
1.87 +%(http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=releases%2FProofGeneral%2Fisar%2FREADME)
1.88 \begin{figure}[htbp]
1.89 \centering
1.90 -\includegraphics[scale=0.5]{fig/pgisabelle}
1.91 +\includegraphics[scale=0.25]{fig/pgisabelle}
1.92 \caption{Proof General for Isabelle}%
1.93 \end{figure}
1.94 +\newpage
1.95 \subsubsection{Isabelle/Jedit}
1.96 jEdit is a text editor for programmers, written in Java.
1.97 Compared to fully-featured IDEs, such as Eclipse or Netbeans, jEdit is much
1.98 smaller and better focused on its primary task of text editing.
1.99 -The general look of the Isabelle/jEdit plugin is similar to existing Java IDEs.
1.100 -The main Isabelle/jEdit plugin consists of ten small Scala files that augment some key jEdit components in order to provide a metaphor of asynchronous
1.101 -proof document editing.
1.102 +The general look of the Isabelle/jEdit plugin is similar to existing Java IDEs \cite{makarius:isa-scala-jedit}.
1.103 +The main Isabelle/jEdit plugin consists of ten small Scala files that augment some key jEdit components in order to provide a metaphor of asynchronous proof document editing.
1.104 Isabelle/jEdit integrates the jEdit 4.3.2 framework and some further jEdit plugins.
1.105 It also implements custom-made IsabelleText Unicode font that actually contains the usual Isabelle symbols that users expect from long
1.106 -years of Proof General X-Symbol support.
1.107 +years of Proof General X-Symbol support.
1.108 The editor provides useful feedback, via semantic information from the processed document in the background.
1.109 -This achieves continuous proof checking based on
1.110 -asynchronous prover toplevel. A lot of information can be directly attached
1.111 +A lot of information can be directly attached
1.112 to the source text, via coloring, tooltips, popups etc.
1.113
1.114 \subsection{Upcoming requirements for userinterfaces in CTP}\label{gui-requir}
1.115 @@ -158,15 +154,20 @@
1.116 % @ ... see\\
1.117 % http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\
1.118 % http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
1.119 -After several decades, most proof assistants are still centered around TTY-based(Fußnote) interaction in a
1.120 -tight read-eval-print loop. All Emacs-based GUI's for CTPs follow this synchronous
1.121 +"After several decades, most proof assistants are still centered around TTY-based interaction in a
1.122 +tight read-eval-print loop.
1.123 +All Emacs-based GUI's for CTPs follow this synchronous
1.124 model based on single commands with immediate response, meaning that the editor waits for the
1.125 -prover after each command. As to multicore politics of leading semiconductor chip manufacturer, parallelism in software technology has become very popular.
1.126 -Therefore the support of parallelism in CTP technology could improve the performance and the multiuser support.
1.127 -So it is necessary to use proof documents instead of proof scripts.
1.128 -Proof scripts are sequences of commands however proof documents are structured texts.
1.129 -So the proof document idea seems to guarantee the perfect support for parallelism in the CTP technology.
1.130 -(MW async-isabelle-scala.pdf)
1.131 +prover after each command", according to \cite{makarius:isa-scala-jedit}. As to multicore politics of leading semiconductor chip manufacturer, parallelism in software technology has become an issue.
1.132 +Therefore the support of parallelism in CTP technology improves the performance and multiuser support.
1.133 +%So it is necessary to use proof documents instead of proof scripts.
1.134 +%Proof scripts are sequences of commands however proof documents are structured texts.
1.135 +%So the proof document idea seems to guarantee the perfect support for parallelism in the CTP technology.
1.136 +Prooflanguage Isar is strutured such, that different parts can be interpreted in parallel. For instance, some might employ an
1.137 +an automated prover for some minutes, while the user wants to proceed with other parts of the same proof.
1.138 +A well-established concept able to cope with such parallel processing in actors, as introduced by Erlang.
1.139 +This will be discussed in more detail in Sect. \ref{actors}
1.140 +
1.141 \newpage
1.142 %Andreas
1.143 \section{Isabelle's plans for new user-interfaces}\label{gui-plans}