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
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
|
;; demoisa.el Example Proof General instance for Isabelle
;;
;; Copyright (C) 1999 LFCS Edinburgh.
;;
;; Author: David Aspinall <da@dcs.ed.ac.uk>
;;
;; $Id$
;;
;; =================================================================
;;
;; Isabelle Proof General in 30 setqs
;;
;; This is a whittled down version of Isabelle Proof General, supplied
;; as an (almost) minimal demonstration of how to instantiate Proof
;; General to a particular proof assistant. You can use this as a
;; template to get support for a new assistant going.
;;
;; This mode uses the unadulterated terminal interface of Isabelle, to
;; demonstrate that hacking the proof assistant is not necessary to
;; get basic features working.
;;
;; And it really works! You you get a toolbar, menus, short-cut keys,
;; script management for multiple files, a function menu, ability to
;; run proof assistant remotely, etc, etc.
;;
;; To try it out, set in the shell PROOFGENERAL_ASSISTANTS=demoisa
;; before invoking Emacs. (Of course, you need Isabelle installed).
;;
;; What's missing?
;;
;; 1. A few handy commands (e.g. proof-find-theorems-command)
;; 2. Syntax settings and highlighting for proof scripts
;; 3. Indentation for proof scripts
;; 4. Special markup characters in output for robustness
;; 5. True script management for multiple files (automatic mode is used)
;; 6. Proof by pointing
;;
;; How easy is it to add all that?
;;
;; 1. Trivial. 2. A table specifying syntax codes for characters
;; (strings, brackets, etc) and some regexps; depends on complexity
;; of syntax. 3. A bit of elisp to scan script; depends on
;; complexity of syntax. 4. Needs hacking in the proof assistant:
;; how hard is to hack your assistant to do this? 5. Depends on file
;; management mechanism in the prover, may need hacking there to send
;; messages. But automatic multiple files may be all you need anyway.
;; 6. Non trivial (but worth a go).
;;
;;
;; =================================================================
;;
;;
;; Basic configuration is controlled by one line in `proof-site.el'.
;; It has this line in proof-assistant-table:
;;
;; (demoisa "Isabelle Demo" "\\.ML$")
;;
;; From this it loads this file "demoisa/demoisa.el" whenever
;; a .ML file is visited, and sets the mode to `demoisa-mode'
;; (defined below).
;;
;; (I've called this instance "Isabelle Demo Proof General" just to
;; avoid confusion with the real "Isabelle Proof General" in case the
;; demo gets loaded by accident).
(require 'proof) ; load generic parts
;; ======== User settings for Isabelle ========
;;
;; Defining variables using customize is pretty easy.
;; You should do it at least for your prover-specific user options.
;;
;; proof-site provides us with two customization groups
;; automatically: (based on the name of the assistant)
;;
;; 'isabelledemo - User options for Isabelle Demo Proof General
;; 'isabelledemo-config - Configuration of Isabelle Proof General
;; (constants, but may be nice to tweak)
;;
;; The first group appears in the menu
;; ProofGeneral -> Customize -> Isabelledemo
;; The second group appears in the menu:
;; ProofGeneral -> Internals -> Isabelledemo config
;;
(defcustom isabelledemo-prog-name "isabelle"
"*Name of program to run Isabelle."
:type 'file
:group 'isabelledemo)
(defcustom isabelledemo-web-page
"http://www.cl.cam.ac.uk/Research/HVG/isabelle.html"
"URL of web page for Isabelle."
:type 'string
:group 'isabelledemo-config)
;;
;; ======== Configuration of generic modes ========
;;
(defun demoisa-config ()
"Configure Proof General scripting for Isabelle."
(setq
proof-terminal-char ?\; ; ends every command
proof-comment-start "(*"
proof-comment-end "*)"
proof-goal-command-regexp "^Goal"
proof-save-command-regexp "^qed"
proof-goal-with-hole-regexp "^Goal \\(\\(\"%s\"\\)\\)"
proof-save-with-hole-regexp "^qed \\(\\(\"%s\"\\)\\)"
proof-non-undoables-regexp "undo\\|back"
proof-undo-n-times-cmd "pg_repeat undo %s;"
proof-showproof-command "pr()"
proof-goal-command "Goal \"%s\";"
proof-save-command "qed \"%s\";"
proof-kill-goal-command "Goal \"PROP no_goal_set\";"
proof-assistant-home-page isabelledemo-web-page
proof-auto-multiple-files t))
(defun demoisa-shell-config ()
"Configure Proof General shell for Isabelle."
(setq
proof-shell-annotated-prompt-regexp "^\\(val it = () : unit\n\\)?ML>? "
proof-shell-cd-cmd "cd \"%s\""
proof-shell-prompt-pattern "[ML-=#>]+>? "
proof-shell-interrupt-regexp "Interrupt"
proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
proof-shell-start-goals-regexp "Level [0-9]"
proof-shell-end-goals-regexp "val it"
proof-shell-proof-completed-regexp "\\(\\(.\\|\n\\)*No subgoals!\n\\)"
proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading"
proof-shell-init-cmd ; define a utility function, in a lib somewhere?
"fun pg_repeat f 0 = ()
| pg_repeat f n = (f(); pg_repeat f (n-1));"
proof-shell-quit-cmd "quit();"))
;;
;; ======== Defining the derived modes ========
;;
;; The name of the script mode is always <proofsym>-script,
;; but the others can be whatever you like.
;;
;; The derived modes set the variables, then call the
;; <mode>-config-done function to complete configuration.
(define-derived-mode demoisa-mode proof-mode
"Isabelle Demo script" nil
(demoisa-config)
(proof-config-done))
(define-derived-mode demoisa-shell-mode proof-shell-mode
"Isabelle Demo shell" nil
(demoisa-shell-config)
(proof-shell-config-done))
(define-derived-mode demoisa-response-mode proof-response-mode
"Isabelle Demo response" nil
(proof-response-config-done))
(define-derived-mode demoisa-goals-mode pbp-mode
"Isabelle Demo goals" nil
(proof-goals-config-done))
;; The response buffer and goals buffer modes defined above are
;; trivial. In fact, we don't need to define them at all -- they
;; would simply default to "proof-response-mode" and "pbp-mode".
;; A more sophisticated instantiation might set font-lock-keywords to
;; add highlighting, or some of the proof by pointing markup
;; configuration for the goals buffer.
;; The final piece of magic here is a hook which configures settings
;; to get the proof shell running. Proof General needs to know the
;; name of the program to run, and the modes for the shell, response,
;; and goals buffers.
(add-hook 'proof-pre-shell-start-hook 'demoisa-pre-shell-start)
(defun demoisa-pre-shell-start ()
(setq proof-prog-name isabelledemo-prog-name)
(setq proof-mode-for-shell 'demoisa-shell-mode)
(setq proof-mode-for-response 'demoisa-response-mode)
(setq proof-mode-for-pbp 'demoisa-goals-mode))
(provide 'demoisa)
|
