54 %specifically designed a 'meta language' (ML) |
54 %specifically designed a 'meta language' (ML) |
55 %http://en.wikipedia.org/wiki/ML\_(programming\_language) |
55 %http://en.wikipedia.org/wiki/ML\_(programming\_language) |
56 %\cite{pl:milner97} |
56 %\cite{pl:milner97} |
57 %for developing CTP |
57 %for developing CTP |
58 \subsubsection{Standard ML} |
58 \subsubsection{Standard ML} |
59 Standard ML is a general-purpose, modular, functional programming language. \cite{pl:milner97} |
59 Standard ML is a general-purpose, modular, functional programming language \cite{pl:milner97}. |
60 Programs written in Standard ML consist of expressions to be evaluated, as opposed to statements or commands. |
60 Programs written in Standard ML consist of expressions to be evaluated, as opposed to statements or commands. |
61 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. |
61 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. |
62 %http://en.wikipedia.org/wiki/Standard_M |
62 %http://en.wikipedia.org/wiki/Standard_M |
63 \subsubsection{Coq} |
63 \subsubsection{Coq} |
64 Coq is an interactive theorem prover, developed in France. |
64 Coq is an interactive theorem prover, developed in France. |
65 It is programmed in Objective Caml, an ML based programming language. |
65 It is programmed in Objective Caml, an ML based programming language. |
66 It has the ability to express mathematical assertions and check proof of mathematical assertions. |
66 It has the ability to express mathematical assertions and check proof of mathematical assertions. |
67 Furthermore Coq includes automatic theorem proving tactics and decision procedures. |
67 Furthermore Coq includes automatic theorem proving tactics and decision procedures. |
68 Properties, programs and proofs are written a functional programming language called the Calculus of Inductive Constructions (CIC). |
68 Properties, programs and proofs are written a functional programming language called the Calculus of Inductive Constructions (CIC). |
69 Proof development in Coq is done through a language of tactics that allows a user-guided proof process.\cite{coq1999} |
69 Proof development in Coq is done through a language of tactics that allows a user-guided proof process \cite{coq1999}. |
70 |
|
71 Another feature of Coq is “that it can automatically extract executable programs from specifications, as either Objective Caml |
70 Another feature of Coq is “that it can automatically extract executable programs from specifications, as either Objective Caml |
72 or Haskell source code.“ |
71 or Haskell source code.“ |
73 |
|
74 There are many easy-to-read introductions to Coq \footnote{http://coq.inria.fr/a-short-introduction-to-coq} on the internet. |
72 There are many easy-to-read introductions to Coq \footnote{http://coq.inria.fr/a-short-introduction-to-coq} on the internet. |
75 \subsubsection{Isabelle} |
73 \subsubsection{Isabelle} |
76 Isabelle is an interactive theorem proving framework for high-level natural deduction proofs \cite{Paulson:Isa94}, written in Standard ML. |
74 Isabelle is an interactive theorem proving framework for high-level natural deduction proofs \cite{Paulson:Isa94}, written in Standard ML. |
77 Isabelle is developed at University of Cambridge (Larry Paulson), Technische Universit\"at M\"unchen |
75 Isabelle is developed at University of Cambridge (Larry Paulson), Technische Universit\"at M\"unchen |
78 and Université Paris-Sud. Isabelle is called a framework, because it implements serveral object logics. |
76 and Université Paris-Sud. Isabelle is called a framework, because it implements serveral object logics. |
79 The most widespread logic of Isabelle is Isabelle/HOL, short for higher-order logic. |
77 The most widespread logic of Isabelle is Isabelle/HOL, short for higher-order logic. |
80 Isabelle/HOL includes several specification tools, e.g. for datatypes, inductive definitions and functions with complex pattern matching. |
78 Isabelle/HOL includes several specification tools, e.g. for datatypes, inductive definitions and functions with complex pattern matching. |
81 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. |
79 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. |
82 Isabelle provides notational support: new notations can be introduced, using normal mathematical symbols. |
80 Isabelle provides notational support: new notations can be introduced, using normal mathematical symbols. |
83 Definitions and proofs may include LaTeX source, from which Isabelle can automatically generate typeset documents. |
81 Definitions and proofs may include LaTeX source, from which Isabelle can automatically generate typeset documents. |
84 Isabelle/HOL allows to turn executable specifications directly into code in SML, OCaml, and Haskell.\cite{Haftmann-Nipkow:2010:code} |
82 Isabelle/HOL allows to turn executable specifications directly into code in SML, OCaml, and Haskell \cite{Haftmann-Nipkow:2010:code}. |
85 (http://www.cl.cam.ac.uk/research/hvg/Isabelle/overview.html) |
83 %(http://www.cl.cam.ac.uk/research/hvg/Isabelle/overview.html) |
86 \subsection{Userinterfaces for CTP: Coq and Isabelle}\label{gui-coq-isa} |
84 \subsection{Userinterfaces for CTP: Coq and Isabelle}\label{gui-coq-isa} |
87 % CoqIDE, .. |
85 % CoqIDE, .. |
88 % http://coq.inria.fr/what-is-coq?q=node/57\\ |
86 % http://coq.inria.fr/what-is-coq?q=node/57\\ |
89 % earlier than Isabelle/jEdit |
87 % earlier than Isabelle/jEdit |
90 % |
88 % |
91 % ProofGeneral for Isabelle |
89 % ProofGeneral for Isabelle |
92 % http://proofgeneral.inf.ed.ac.uk/\\ |
90 % http://proofgeneral.inf.ed.ac.uk/\\ |
93 % emacs stone age ? |
91 % emacs stone age ? |
94 \subsubsection{Coq Integrated Development Environment} |
92 \subsubsection{Coq Integrated Development Environment} |
95 CoqIde is a graphical interface for Coq. It is written in Ocaml. (http://coq.inria.fr/cocorico/CoqIde) |
93 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. |
96 Its main purpose is to allow the user to navigate forward and backward into a Coq vernacular file, |
94 Its main purpose is to allow the user to navigate forward and backward into a Coq vernacular file, |
97 executing corresponding commands or undoing them respectively. |
95 executing corresponding commands or undoing them respectively. |
98 There are several buffers for helping to write proof scripts. |
96 There are several buffers for helping to write proof scripts. |
99 Among all these buffers, there is always one which is the current running buffer, whose name is displayed on a green background, |
97 Among all these buffers, there is always one which is the current running buffer, whose name is displayed on a green background, |
100 which is the one where Coq commands are currently executed. |
98 which is the one where Coq commands are currently executed. |
101 Buffers may be edited as in any text editor, and classical basic editing commands (Copy/Paste, ...) are available. |
99 CoqIDE provides also a feedback system for the user. |
102 CoqIde provides also a feedback system for the user. |
|
103 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. |
100 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. |
104 CoqIDE offers only basic editing commands, therefore it is possible to launch another more sophisticated text editor. |
101 CoqIDE offers only basic editing commands, therefore it is possible to launch another more sophisticated text editor. |
105 Furthermore CoqIde provides a proof wizard “for automatically trying to solve the current goal using simple tactics.” |
102 Furthermore CoqIde provides a proof wizard “for automatically trying to solve the current goal using simple tactics.” |
106 Another features of this IDE are the customization options, which can be accessed by the Edit menu. |
103 Another features of this IDE are the customization options, which can be accessed by the Edit menu. |
107 This allows the user to change the apeareance of the IDE. |
104 This allows the user to change the apeareance of the IDE. |
113 \includegraphics[scale=0.25]{fig/coqide} |
110 \includegraphics[scale=0.25]{fig/coqide} |
114 \caption{CoqIDE main screen} |
111 \caption{CoqIDE main screen} |
115 \end{figure} |
112 \end{figure} |
116 |
113 |
117 |
114 |
118 (http://coq.inria.fr/V8.1/refman/Reference-Manual016.html) |
115 %(http://coq.inria.fr/V8.1/refman/Reference-Manual016.html) |
119 \subsubsection{Proof General for Isabelle} |
116 \subsubsection{Proof General for Isabelle} |
120 Proof General is a generic front-end for proof assistants, based on the customizable text editor Emacs. |
117 Proof General is a generic front-end for proof assistants \cite{aspinall}, based on the text editor Emacs. |
121 It has been developed at the University of Edinburgh with contributions from other sites. |
118 It has been developed at the University of Edinburgh with contributions from other sites. |
122 Proof General comes ready-to-go for these proof assistants: Isabelle, Coq, PhoX, LEGO. |
119 Proof General supports the following proof assistants: Isabelle, Coq, PhoX, LEGO. |
123 Proof General is used to write proof scripts. A Proof Script is a sequence of commands sent to theorem prover. |
120 It is used to write proof scripts. A Proof Script is a sequence of commands sent to theorem prover. |
124 The communication between the user and the theorem prover takes place via two or more Emacs text widgets. |
121 The communication between the user and the theorem prover takes place via two or more Emacs text widgets. |
125 Therefore the user sees only the output from the latest proof step.(proofgeneral.ps.gz) |
122 Therefore the user sees only the output from the latest proof step. |
126 |
123 |
127 |
124 |
128 Isabelle/Isar Proof General has full support for multiple file scripting, with dependencies between theories communicated between Isabelle and Proof General. |
125 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. |
129 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 |
126 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 |
130 and it's easy to add to your own theories. |
127 and it's easy to add to your own theories. |
131 (http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=releases%2FProofGeneral%2Fisar%2FREADME) |
128 %(http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=releases%2FProofGeneral%2Fisar%2FREADME) |
132 \begin{figure}[htbp] |
129 \begin{figure}[htbp] |
133 \centering |
130 \centering |
134 \includegraphics[scale=0.5]{fig/pgisabelle} |
131 \includegraphics[scale=0.25]{fig/pgisabelle} |
135 \caption{Proof General for Isabelle}% |
132 \caption{Proof General for Isabelle}% |
136 \end{figure} |
133 \end{figure} |
|
134 \newpage |
137 \subsubsection{Isabelle/Jedit} |
135 \subsubsection{Isabelle/Jedit} |
138 jEdit is a text editor for programmers, written in Java. |
136 jEdit is a text editor for programmers, written in Java. |
139 Compared to fully-featured IDEs, such as Eclipse or Netbeans, jEdit is much |
137 Compared to fully-featured IDEs, such as Eclipse or Netbeans, jEdit is much |
140 smaller and better focused on its primary task of text editing. |
138 smaller and better focused on its primary task of text editing. |
141 The general look of the Isabelle/jEdit plugin is similar to existing Java IDEs. |
139 The general look of the Isabelle/jEdit plugin is similar to existing Java IDEs \cite{makarius:isa-scala-jedit}. |
142 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 |
140 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. |
143 proof document editing. |
|
144 Isabelle/jEdit integrates the jEdit 4.3.2 framework and some further jEdit plugins. |
141 Isabelle/jEdit integrates the jEdit 4.3.2 framework and some further jEdit plugins. |
145 It also implements custom-made IsabelleText Unicode font that actually contains the usual Isabelle symbols that users expect from long |
142 It also implements custom-made IsabelleText Unicode font that actually contains the usual Isabelle symbols that users expect from long |
146 years of Proof General X-Symbol support. |
143 years of Proof General X-Symbol support. |
147 The editor provides useful feedback, via semantic information from the processed document in the background. |
144 The editor provides useful feedback, via semantic information from the processed document in the background. |
148 This achieves continuous proof checking based on |
145 A lot of information can be directly attached |
149 asynchronous prover toplevel. A lot of information can be directly attached |
|
150 to the source text, via coloring, tooltips, popups etc. |
146 to the source text, via coloring, tooltips, popups etc. |
151 |
147 |
152 \subsection{Upcoming requirements for userinterfaces in CTP}\label{gui-requir} |
148 \subsection{Upcoming requirements for userinterfaces in CTP}\label{gui-requir} |
153 % @ interaction close to tty (Telegraph)\\ |
149 % @ interaction close to tty (Telegraph)\\ |
154 % BUT: separate parts in {\em one} proof could be processed in parallel |
150 % BUT: separate parts in {\em one} proof could be processed in parallel |
156 % @ http://www.informatik.uni-bremen.de/uitp/ |
152 % @ http://www.informatik.uni-bremen.de/uitp/ |
157 % |
153 % |
158 % @ ... see\\ |
154 % @ ... see\\ |
159 % http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\ |
155 % http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\ |
160 % http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf |
156 % http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf |
161 After several decades, most proof assistants are still centered around TTY-based(Fußnote) interaction in a |
157 "After several decades, most proof assistants are still centered around TTY-based interaction in a |
162 tight read-eval-print loop. All Emacs-based GUI's for CTPs follow this synchronous |
158 tight read-eval-print loop. |
|
159 All Emacs-based GUI's for CTPs follow this synchronous |
163 model based on single commands with immediate response, meaning that the editor waits for the |
160 model based on single commands with immediate response, meaning that the editor waits for the |
164 prover after each command. As to multicore politics of leading semiconductor chip manufacturer, parallelism in software technology has become very popular. |
161 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. |
165 Therefore the support of parallelism in CTP technology could improve the performance and the multiuser support. |
162 Therefore the support of parallelism in CTP technology improves the performance and multiuser support. |
166 So it is necessary to use proof documents instead of proof scripts. |
163 %So it is necessary to use proof documents instead of proof scripts. |
167 Proof scripts are sequences of commands however proof documents are structured texts. |
164 %Proof scripts are sequences of commands however proof documents are structured texts. |
168 So the proof document idea seems to guarantee the perfect support for parallelism in the CTP technology. |
165 %So the proof document idea seems to guarantee the perfect support for parallelism in the CTP technology. |
169 (MW async-isabelle-scala.pdf) |
166 Prooflanguage Isar is strutured such, that different parts can be interpreted in parallel. For instance, some might employ an |
|
167 an automated prover for some minutes, while the user wants to proceed with other parts of the same proof. |
|
168 A well-established concept able to cope with such parallel processing in actors, as introduced by Erlang. |
|
169 This will be discussed in more detail in Sect. \ref{actors} |
|
170 |
170 \newpage |
171 \newpage |
171 %Andreas |
172 %Andreas |
172 \section{Isabelle's plans for new user-interfaces}\label{gui-plans} |
173 \section{Isabelle's plans for new user-interfaces}\label{gui-plans} |
173 % http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\ |
174 % http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\ |
174 % http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf |
175 % http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf |