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
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
1518
1519
1520
1521
1522
1523
1524
1525
1526
1527
1528
1529
1530
1531
1532
1533
1534
1535
1536
1537
1538
1539
1540
1541
1542
1543
1544
1545
1546
1547
1548
1549
1550
1551
1552
1553
1554
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
1592
1593
1594
1595
1596
1597
1598
1599
1600
1601
1602
1603
1604
1605
1606
1607
1608
1609
1610
1611
1612
1613
1614
1615
1616
1617
1618
1619
1620
1621
1622
1623
1624
1625
1626
1627
1628
1629
1630
1631
1632
1633
1634
1635
1636
1637
1638
1639
1640
1641
1642
1643
1644
1645
1646
1647
1648
1649
1650
1651
1652
1653
1654
1655
1656
1657
1658
1659
1660
1661
1662
1663
1664
1665
1666
1667
1668
1669
1670
1671
1672
1673
1674
1675
1676
1677
1678
1679
1680
1681
1682
1683
1684
1685
1686
1687
1688
1689
1690
1691
1692
1693
1694
1695
1696
1697
1698
1699
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
1710
1711
1712
1713
1714
1715
1716
1717
1718
1719
1720
1721
1722
1723
1724
1725
1726
1727
1728
1729
1730
1731
1732
1733
1734
1735
1736
1737
1738
1739
1740
1741
1742
1743
1744
1745
1746
1747
1748
1749
1750
1751
1752
1753
1754
1755
1756
1757
1758
1759
1760
1761
1762
1763
1764
1765
1766
1767
1768
1769
1770
1771
1772
1773
1774
1775
1776
1777
1778
1779
1780
1781
1782
1783
1784
1785
1786
1787
1788
1789
1790
1791
1792
1793
1794
1795
1796
1797
1798
1799
1800
1801
1802
1803
1804
1805
1806
1807
1808
1809
1810
1811
1812
1813
1814
1815
1816
1817
1818
1819
1820
1821
1822
1823
1824
1825
1826
1827
1828
1829
1830
1831
1832
1833
1834
1835
1836
1837
1838
1839
1840
1841
1842
1843
1844
1845
1846
1847
1848
1849
1850
1851
1852
1853
1854
1855
1856
1857
1858
1859
1860
1861
1862
1863
1864
1865
1866
1867
1868
1869
1870
1871
1872
1873
1874
1875
1876
1877
1878
1879
1880
1881
1882
1883
1884
1885
1886
1887
1888
1889
1890
1891
1892
1893
1894
1895
1896
1897
1898
1899
1900
1901
1902
1903
1904
1905
1906
1907
1908
1909
1910
1911
1912
1913
1914
1915
1916
1917
1918
1919
1920
1921
1922
1923
1924
1925
1926
1927
1928
1929
1930
1931
1932
1933
1934
1935
1936
1937
1938
1939
1940
1941
1942
1943
1944
1945
1946
1947
1948
1949
1950
1951
1952
1953
1954
1955
1956
1957
1958
1959
1960
1961
1962
1963
1964
1965
1966
1967
1968
1969
1970
1971
1972
1973
1974
1975
1976
1977
1978
1979
1980
1981
1982
1983
1984
1985
1986
1987
1988
1989
1990
1991
1992
1993
1994
1995
1996
1997
1998
1999
2000
2001
2002
2003
2004
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
2015
2016
2017
2018
2019
2020
2021
2022
2023
2024
2025
2026
2027
2028
2029
2030
2031
2032
2033
2034
2035
2036
2037
2038
2039
2040
2041
2042
2043
2044
|
\input texinfo @c -*-texinfo-*-
@c
@c $Id$
@c
@c %**start of header
@setfilename ProofGeneral.info
@settitle Proof General
@setchapternewpage odd
@paragraphindent 0
@iftex
@afourpaper
@end iftex
@c %**end of header
@c FIXME: screenshots for this info file would be nice!
@set version 2.0
@set xemacsversion 20.4
@set fsfversion 20.2
@set last-update October 1998
@ifinfo
@format
START-INFO-DIR-ENTRY
* ProofGeneral::Organize your proofs with Emacs!
END-INFO-DIR-ENTRY
@end format
@end ifinfo
@c merge functions and variables into concept index.
@syncodeindex fn cp
@syncodeindex vr cp
@finalout
@titlepage
@title Proof General
@subtitle Organise your proofs with Emacs!
@subtitle Proof General @value{version}
@subtitle @value{last-update}
@image{ProofGeneral}
@author D. Aspinall, H. Goguen, T. Kleymann and D. Sequeira
@page
@vskip 0pt plus 1filll
This manual and the program Proof General are
Copyright @copyright{} 1998 Proof General team, LFCS Edinburgh.
@c
@c COPYING NOTICE
@c
@ignore
Permission is granted to process this file through TeX and print the
results, provided the printed document carries copying permission notice
identical to this one except for the removal of this paragraph (this
paragraph not being relevant to the printed manual).
@end ignore
@sp 2
Permission is granted to make and distribute verbatim copies of this
manual provided the copyright notice and this permission notice are
preserved on all copies.
@sp 2
This manual documents Proof General, Version @value{version}, for use
with XEmacs @value{xemacsversion} and FSF GNU Emacs @value{fsfversion}
or later versions.
@end titlepage
@page
@ifinfo
@node Top
@top Proof General
This file documents version @value{version} of @b{Proof General}, a
generic Emacs interface for proof assistants.
Proof General @value{version} has been tested with XEmacs
@value{xemacsversion} and FSF GNU Emacs @value{fsfversion}. It is
supplied ready customized for the proof assistants Coq, Lego, and
Isabelle.
@menu
* Introducing Proof General::
* Basic Script Management::
* Advanced Script Management::
* Support for other Packages::
* Customizing Proof General::
* LEGO Proof General::
* Coq Proof General::
* Isabelle Proof General::
* Adapting Proof General to New Provers::
* Internals of Proof General::
* Credits and References::
* Obtaining and Installing Proof General::
* Known bugs and workarounds::
* Plans and ideas::
* Variable Index::
* Function Index::
* Concept Index::
@end menu
@detailmenu --- The Detailed Node Listing ---
Introducing Proof General
--- The Detailed Node Listing ---
Introducing Proof General
* Quick start guide::
* Features of Proof General::
* Supported proof assistants::
Basic Script Management
* Proof scripts::
* The buffer model::
* Regions in a proof script::
* Script editing commands::
* Script processing commands::
* Toolbar commands::
* Other commands::
* Walkthrough example in LEGO::
Proof scripts
* Goals and saves::
Advanced Script Management
* Switching between proof scripts::
* View of processed files ::
* Retracting across files::
* Asserting across files::
* Working directly with the proof shell::
Support for other Packages
* Support for function menus::
Customizing Proof General
* Easy customization::
* Setting user options::
* Running on another machine::
* Tweaking configuration settings::
LEGO Proof General
* LEGO specific commands::
* LEGO customizations::
Coq Proof General
* Coq specific commands::
* Coq customizations::
Isabelle Proof General
* Isabelle specific commands::
* Isabelle customizations::
Adapting Proof General to New Provers
* Skeleton example::
* Proof script settings::
* Proof shell settings::
Proof shell settings
* Special annotations::
Internals of Proof General
* Proof Script Mode::
* Proof Shell Mode::
* Handling Multiple Files::
Credits and References
* Credits::
* References::
Obtaining and Installing Proof General
* Obtaining Proof General::
* Installing Proof General from tarball::
* Installing Proof General from RPM package::
* Notes for syssies::
@end detailmenu
@end ifinfo
@node Introducing Proof General
@chapter Introducing Proof General
@c maybe not in TeX, just put on title page.
@c not in info, it can't deal with images.
@c Maybe in HTML because it doesn't appear in titles?
@ifhtml
@image{ProofGeneral}
@end ifhtml
@dfn{Proof General} is a generic Emacs interface for proof assistants,
developed at the LFCS in the University of Edinburgh.
Proof General works best under XEmacs, but can also be used with FSF GNU
Emacs.
You do not have to be an Emacs militant to use Proof General! @*
The interface is designed to be very easy to use. You develop your
proof script in place rather than line-by-line in a shell using
cut-and-paste to reassemble the pieces. Proof General keeps track of
which proof steps have been processed by the prover, and prevents you
editing them accidently. You can undo steps as usual.
@menu
* Quick start guide::
* Features of Proof General::
* Supported proof assistants::
@end menu
@node Quick start guide
@section Quick start guide
Proof General may have been installed for you already. If so, when you
visit a proof script file for your proof assistant, you'll find commands
to process the proof script are available from the toolbar, menus, and
keyboard. Type @kbd{C-h m} to get a list of keys for the current mode.
The proof assistant is automatically started inside Emacs when you ask
for some of the proof script to be processed. To follow an example use
of Proof General on a LEGO proof, see @pxref{Walkthrough example in LEGO}.
If Proof General has not already been installed, you should insert the
line:
@lisp
(load "@var{ProofGeneral}/generic/proof-site.el")
@end lisp
into your @file{~/.emacs} file, where @var{ProofGeneral} is the
top-level directory that was created when Proof General was unpacked.
For more details on obtaining and installing Proof General,
see @pxref{Obtaining and Installing Proof General}.
@node Features of Proof General
@section Features of Proof General
Here is an outline of the main features of Proof General.
@itemize @bullet
@item @i{Simplified communication}@*
The proof assistant's shell is normally hidden from the user.
Communication takes place via two or three buffers. The @dfn{script
buffer} holds input, the commands to construct a proof. The @dfn{goals
buffer} displays the current list of subgoals to be solved. The
@dfn{response buffer} displays other output from the proof assistants.
This means that the user only sees the output from the most recent proof
step, rather than a screen full of output from the proof assistant.
@c Optionally, the goals buffer and script buffer can be identified.
For more details, see @pxref{The buffer model}.
@item @i{Script management}@*
Proof General colours proof script regions blue when they have already
been processed by the prover, and colours regions red when the prover is
currently processing them. The appearance of Emacs buffers always
matches the proof assistant's state.
For more details, see @pxref{Basic Script Management}
and @pxref{Advanced Script Management}.
@item @i{Script editing mode}@*
Proof General provides useful facilities for editing proof scripts,
including syntax hilighting and a menu to jump to particular goals.
Special editing functions send lines of proof script to the proof
assistant, or undo previous proof steps.
For more details, see @pxref{Script editing commands}
and @pxref{Script processing commands}.
@item @i{Toolbar and menus}@*
A script buffer has a toolbar with navigation buttons for processing
parts of the proof script. A menu provides further functions for
operations in the proof assistant, as well as customization of Proof
General.
For more details, see @pxref{Toolbar commands}, @pxref{Other commands},
and @pxref{Customizing Proof General}.
@c not yet
@c @item @i{Proof by pointing}
@end itemize
@node Supported proof assistants
@section Supported proof assistants
Proof General comes ready-customised for these proof assistants:
@itemize @bullet
@item
@b{LEGO Proof General} for LEGO Version 1.3.1@*
@c written by Thomas Kleymann and Dilip Sequeira.
LEGO Proof General supports all of the generic features of Proof
General.
See @pxref{LEGO Proof General} for more details.
@item
@b{Coq Proof General} for Coq Version 6.2@*
@c written by Healfdene Goguen.
Coq Proof General supports all of the generic features of Proof General
except multiple files.
See @pxref{Coq Proof General} for more details.
@item
@b{Isabelle Proof General} for Isabelle 98-1@*
@c written by David Aspinall.
Isabelle Proof General supports all of the generic features of
Proof General, excepting the external tags program. It handles
theory files as well as ML (proof script files), and has
an extensive theory file editing mode taken from Isamode.
See @pxref{Isabelle Proof General} for more details.
@end itemize
Proof General is designed to be generic, so you can adapt it to other
proof assistants if you know a little bit of Emacs Lisp.
See @pxref{Adapting Proof General to New Provers} for more details
of how to do this.
@node Basic Script Management, Advanced Script Management, Introducing Proof General, Top
@chapter Basic Script Management
@menu
* Proof scripts::
* The buffer model::
* Regions in a proof script::
* Script editing commands::
* Script processing commands::
* Toolbar commands::
* Other commands::
* Walkthrough example in LEGO::
@end menu
@node Proof scripts, The buffer model, Basic Script Management, Basic Script Management
@section Proof scripts
A @dfn{proof script} is a sequence of commands to a proof assistant used
to construct a proof. Proof General is designed to work with
@i{interactive} proof assistants, where the mode of working is usually a
dialogue between the user and the proof assistant.
Primitive interfaces for proof assistants simply present a shell-like
view of this dialogue: the user repeatedly types commands to the shell
until the proof is completed. The system responds at each step, maybe
with a new list of subgoals to be solved, or maybe with a failure
report.
Often we want to keep a record of the proof commands used to prove a
theorem, in the form of a proof script kept in a file. Then we can
@dfn{replay} the proof later on to reprove the theorem, without having
to type in all the commands again.
@c Re-playing a proof script is a non-interactive procedure,
@c since it is supposed to succeed.
Using only a primitive shell interface, it can be tedious to construct
proof scripts with cut-and-paste. Proof General helps organize
interactive proofs by issuing commands directly from a proof script
file, while it is written and edited.
@c developing them in proof script files.
@menu
* Goals and saves::
@end menu
@node Goals and saves, , Proof scripts, Proof scripts
@unnumberedsubsec Goals and saves
A proof script contains a sequence of commands used to prove one or more
theorems. In general we assume that for each proved theorem, a proof
script contains a goal .. save pair of commands which appear something
like this:
@lisp
goal T is G
...
save theorem T
@end lisp
Proof General recognizes goal .. save pairs in proof scripts.
The name T can appear in the definitions menu for the proof
script (see Support for function menus), and once
a goal .. save pair is completed it is treated
as atomic when undoing proof steps (see Undo).
@node The buffer model, Regions in a proof script, Proof scripts, Basic Script Management
@section The buffer model
@c FIXME: fix this in the light of what gets implemented.
Proof General runs your proof assistant in a shell buffer in Emacs.
This @dfn{proof shell buffer} is usually hidden from view,
@pxref{Working directly with the proof shell} for further details.
When Proof General sees an error in the shell buffer, it will
highlight the error and display the buffer automatically.
Communication with the proof shell takes place via two or three
intermediate buffers.
The @dfn{script buffer} holds input destined for the proof shell, in the
form of a @i{proof script}. Normally this is a buffer visiting a file,
which can be later loaded directly by the prover to replay the proof.
The @dfn{goals buffer} displays the current list of subgoals to be
solved for a proof in progress. This is normally displayed at
the same time as the script buffer.
The @dfn{response buffer} displays other output from the proof
assistant, for example warning or informative messages.
@c Optionally, the goals buffer and script buffer can be identified
@c @pxref{Identify goals and response}. The disadvantage of this is that
@c the goals display can be replaced by other messages, so you must ask for
@c it to be refreshed. The advantage is that it is simpler to deal with
@c fewer Emacs buffers.
@node Regions in a proof script
@section Regions in a proof script
@node Script editing commands
@section Script editing commands
@node Script processing commands
@section Script processing commands
@c FIXME: requires formatting
Why is C-c C-b useful? Could just use the file to read it one go
(will we have a command to do this other than via the process?).
BUT it's nice because it stops exactly where a proof fails, so you can
continue development from there.
@node Toolbar commands
@section Toolbar commands
@node Other commands
@section Other commands
Please explain C-c C-v here.
Perhaps, don't explain C-c C-z here. Instead refer to @pxref{Working
directly with the proof shell}
@node Walkthrough example in LEGO
@section Walkthrough example in LEGO
@node Advanced Script Management
@chapter Advanced Script Management
@cindex Multiple Files
What we really mean by @emph{advanced} is that Proof General supports
large proof developments. These are typically spread across various
files which depend on each other in some way. Proof General knows enough
about the dependencies to allow script management across multiple files.
@menu
* Switching between proof scripts::
* View of processed files ::
* Retracting across files::
* Asserting across files::
* Working directly with the proof shell::
@end menu
@node Switching between proof scripts
@section Switching between proof scripts
@cindex Switching between proof scripts
Basic modularity in large proof developments can be achieved by
splitting proof scripts across various files. Let's assume that you are
in the middle of a proof development. You are working on a soundness
proof of Hoare Logic in a file called@footnote{The suffix may depend of
the specific proof assistant you are using e.g, LEGO's proof script
files have to end with @file{.l}.} @file{HSound.l}. It
depends on a number of other files which develop underlying
concepts e.g. syntax and semantics of expressions, assertions,
imperative programs. You notice that the current lemma is too difficult
to prove because you have forgotten to prove some more basic properties
about determinism of the programming language. Or perhaps a previous
definition is too cumbersome or even wrong.
At this stage, you would like to visit the appropriate file, say
@file{sos.l} and retract to where changes are required. For further
details on how to accomplish this, we refer to @ref{Retracting across
files}. Then, using script management, you want to develop some more
basic theory in @file{sos.l}. Once this task has been completed
(possibly involving retraction across even earlier files) and the new
development has been asserted, you want to swich back to @file{HSound.l}
and replay to the point you got stuck previously.
Some hours (or days) later you have completed the soundness proof and
are ready to tackle new challenges. Perhaps, you want to prove a
property that builds on soundness or you want to prove an orthogonal
property such as completeness.
Proof General lets you do all of this while maintaining the consistency
between proof script buffers and the state of the proof assistant.
However, you cannot have more than one buffer where only a fraction of
the proof script contains a locked region. Before you can employ script
management in another proof script buffer, you must either fully assert
or retract the current script buffer.
@node View of processed files
@section View of processed files
Proof General is aware of all files that the proof assistant has
processed or is currently processing. In fact, it relies on the proof
assistant explicitly telling the Proof General whenever it processes a
new file which corresponds@footnote{For example, LEGO generates additional compiled
(optimised) proof script files for efficiency.} to a file containing a proof
script. For further technical
details, @pxref{Handling Multiple Files}.
If the current proof script buffer depends on background material from
other files, proof assistants typically process these files
automatically. If you visit such a file, the whole file is locked as
having been processed in a single step. From the user's point of view,
you can only retract but not assert in this buffer. Furthermore,
retraction is only possible to the @emph{beginning} of the buffer.
To be more precise, buffers are locked as soon the Proof Assistant
notifies the Proof General of processing a file different from the
current proof script. Thus, if you visit the file while the Proof
Assitant is still processing the file, it is already completely locked.
If the Proof Assistant is not happy with the contents and
complains with an error message, the buffer will still be marked as
having been completely processed. Sorry. You need to visit the
troublesome file, retract (which will always retract to the beginning of
the file) and debug the problem e.g., by asserting all of the buffer
under the supervision of the Proof General, @pxref{Script processing
commands}.
In case you wondered, inconsistencies may arise when you have unsaved
changes in a proof script buffer and the Proof Assistant suddenly
decides to automatically process the corresponding file. The good news
is that Proof General detects this problem and flashes up a warning in
the response buffer. You might then want to visit the modified buffer,
save it and retract to the beginning. Then you are back on track.
@node Retracting across files
@section Retracting across files
@cindex Retraction
Make sure that the current script buffer has either been completely
asserted or retracted. Then you can retract proof scripts in a different
file. Simply visit a file that has been processed earlier and retract in
it, using the retraction commands from @ref{Script processing commands}. Apart from removing parts of the locked region in this
buffer, all files which depend on it will be retracted (and thus
unlocked) automatically. Proof General reminds you that now is a good
time to save any unmodified buffers.
@node Asserting across files
@section Asserting across files
@cindex Assertion
Make sure that the current script buffer has either been completely
asserted or retracted. Then you can assert proof scripts in a different
file. Simply visit a file that contains no locked region and assert some
command with the usual assertion commands, @pxref{Script processing
commands}. Proof General reminds you that now is a good time to save any
unmodified buffers. This is particularly useful as assertion may cause
the Proof Assistant to automatically process other files.
@node Working directly with the proof shell
@section Working directly with the proof shell
@cindex Shell
Occasionally you may want to review the dialogue of the entire session
with the proof assistant, or check that it hasn't done something
unexpected. Experienced users may also want to directly communicate with
the Proof Assistant rather than sending commands via the minibuffer,
@pxref{Other commands}.
Although the proof shell is usually hidden from view, it is run in a
buffer which provides the usual full editing and history facilities of
Emacs shells (see the package @file{comint.el} distributed with your
version of Emacs). You can switch to it using the menu:
@lisp
Proof-General -> Switch to buffers -> Proof Shell
@end lisp
@b{Warning:} you can probably cause confusion by typing in the shell
buffer! Proof General may lose track of the state of the proof
assistant.
Proof General watches the output from the proof assistant to guess when
a file is loaded or when a proof step is taken or undone, but it may not
be guaranteed when the restricted interface is by-passed. What happens
depends on how complete the communication is between Proof General and
the prover (which depends on the particular instantion of Proof
General).
To resynchronise, you have two options. If you are lucky, it might
suffice to
@table @kbd
@item C-c C-z
move the end of the locked region backwards to the end of the segment
containing the point.
@end table
Otherwise, you will need to restart script management altogether,
@pxref{Toolbar commands}.
@node Support for other Packages
@chapter Support for other Packages
@menu
* Support for function menus::
* Support for tags::
@end menu
@node Support for function menus
@section Support for function menus
@vindex proof-goal-with-hole-regexp
@cindex fume-func
fume-func is a handy package which makes a menu from the function
declarations in a buffer. Proof General configures fume-func so that
you can quickly jump to particular proofs in a script buffer. This is
done with the configuration variable @code{proof-goal-with-hole-regexp},
@pxref{Proof Script Mode} for further details.
If you want to use fume-func, you may need to enable it for yourself.
It is distributed with XEmacs but by not enabled by
default. To enable it you should find the file func-menu.el and follow
the instructions there. At the time of writing, the current version of
XEmacs is 20.4, supplied with function menu version 2.45, which suggests
the following code for your @file{.emacs} file:
@lisp
(require 'func-menu)
(define-key global-map 'f8 'function-menu)
(add-hook 'find-file-hooks 'fume-add-menubar-entry)
(define-key global-map "\C-cl" 'fume-list-functions)
(define-key global-map "\C-cg" 'fume-prompt-function-goto)
(define-key global-map '(shift button3) 'mouse-function-menu)
(define-key global-map '(meta button1) 'fume-mouse-function-goto)
@end lisp
If you have another version of Emacs, you should check the fume-func.el
file supplied with it.
@node Support for tags
@section Support for tags
@cindex tags
@c FIXME: instructions for setting up etags are needed
@node Customizing Proof General
@chapter Customizing Proof General
There are two kinds of customization for Proof General: it can be
customized for a user's preferences using a particular proof assistant,
or it can be customized by an Emacs expert to add a new proof assistant.
Here we cover the user-level customization for Proof General.
We only consider settings for Proof General itself. The support for a
particular proof assistant can provide extra customization settings.
See the chapters covering each assistant for details.
@menu
* Easy customization::
* Setting user options::
* Running on another machine::
* Tweaking configuration settings::
@end menu
@node Easy customization
@section Easy customization
Proof General uses the Emacs customization library extensively to
provide a friendly interface.
You can access a menu of the customization settings for Proof General
via the menu:
@lisp
Options -> Customize -> Emacs -> External -> Proof General
@end lisp
in XEmacs, or in Emacs
@c FIXME
@lisp
Options -> Customize -> Emacs -> External -> Proof General
@end lisp
Before Proof General is fully loaded, not all customization
settings will be shown in the menu. Proof General is fully
loaded when you visit a script file for the first time.
When visiting a script file, there is a more direct route to the
settings:
@lisp
Proof-General -> Customize
@end lisp
Using the customize facility is straightforward. You can select the
setting to customize via the menus, or with @code{M-x
customize-variable}. When you have selected a setting, you are shown a
buffer with its current value, and facility to edit it. Once you have
edited it, you can use the special buttons @var{set}, @var{save} and
@var{done}. You must use one of @var{set} or @var{save} to get any
effect. The @var{save} button stores the setting in your @file{.emacs}
file.
For more help, see @inforef{Easy Customization, ,xemacs}.
@node Setting user options
@section Setting user options
Here are the user options for Proof General. These can be set via the
customization system, via the old-fashioned @code{M-x edit-options}
mechanism, or simply by adding @code{setq}'s to your @file{.emacs} file.
The first approach is the recommended one.
Notice that in the customize menus, the variable names may be
abbreviated by omitting the "@code{proof}-" prefix. Also, some of the
option settings may have more descriptive names (for example, @var{on}
and @var{off}) than the low-level lisp values (non-@code{nil},
@code{nil}) which are mentioned here.
@defopt proof-prog-name-ask
If non-@code{nil}, query user which program to run for the inferior process.
@end defopt
@defopt proof-one-command-per-line
If non-@code{nil}, format for newlines after each proof command in a script.
@end defopt
@defopt proof-toolbar-wanted
Whether to use toolbar in proof mode.
@end defopt
@defopt proof-toolbar-follow-mode
Choice of how point moves with toolbar commands.
One of the symbols: @code{locked}, @code{follow}, @code{ignore}.
If @code{locked}, point sticks to the end of the locked region with
toolbar commands. @*
If @code{follow}, point moves just when needed to display the
locked region end. @*
If @code{ignore}, point is never moved after toolbar movement commands.
@end defopt
@defopt proof-window-dedicated
Whether response and goals buffers have dedicated windows.
If non-@code{nil}, windows displaying responses from the prover will not
be switchable to display other windows. This helps manage your display,
but can sometimes be inconvenient, especially for experienced Emacs
users.
@end defopt
@c FIXME needs to mention that without dedicated windows, buffers may be
@c hidden. Refer to the XEmacs manual on customising buffer display.
@node Running on another machine
@section Running on another machine
@node Tweaking configuration settings
@section Tweaking configuration settings
Configuration settings are the per-prover customizations of Proof
General. Occasionally you may like to adjust some of these settings to
improve the way Proof General works. Ideally this should not be
necessary. One case when it may be necessary is when a proof assistant
has a flexible proof script language in which one can define new tactics
or even operations, and you want Proof General to recognize some of
these which the default settings don't mention. So please feel free to
try adjusting the configuration settings and report to us if you find
better default values than the ones we have provided.
The configuration settings appear in the customization group
@code{prover-config}, or via the menu
@lisp
Proof-General -> Internals -> Prover Config
@end lisp
Some examples of settings you may like to tweak are:
proof-assistant-home-page
More details of the settings are given in @xref{Adapting Proof General
to New Provers}.
Unfortunately, although you can use the customization mechanism to set
and save these variables, saving them may have no effect because the
default settings are mostly hard-wired into the proof assistant code.
@c FIXME: this is a problem, code does need fixing.
At present there is no easy way to get around this.
@node LEGO Proof General
@chapter LEGO Proof General
LEGO proof script mode is a mode derived from proof script mode for
editing LEGO scripts. An important convention is that proof script
buffers @emph{must} start with a module declaration. If the proof script
buffer's file name is @file{fermat.l}, then it must commence with a
declaration of the form
@lisp
Module fermat;
@end lisp
If, in the development of the module @samp{fermat}, you require material
from other module e.g., @samp{lib_nat} and @samp{galois}, you need to
specify this dependency as part of the module declaration:
@lisp
Module fermat Import lib_nat galois;
@end lisp
No need to worry too much about effeciency. When you retract back to a
module declaration to add a new import item, LEGO does not actually
retract the previously imported modules. Therefore, reasserting the
extended module declaration really only processes the newly imported
modules.
Using the LEGO Proof General, you never ever need to use administrative
LEGO commands such as @samp{Forget}, @samp{ForgetMark}, @samp{KillRef},
@samp{Load}, @samp{Make}, @samp{Reload} and @samp{Undo} again
@footnote{And please, don't even think of including those in your LEGO
proof script!}. You can concentrate on your actual proof developments.
Script management in the Proof General will invoke the appropriate
commands for you. Proving with LEGO has never been easier.
@menu
* LEGO specific commands::
* LEGO tags::
* LEGO customizations::
@end menu
@node LEGO specific commands
@section LEGO specific commands
In addition to the commands provided by the generic Proof General, see
the previous sections, the LEGO Proof General provides a few extensions.
In proof scripts, there are some abbreviations for common commands:
@table @kbd
@item C-c i
intros
@item C-c I
Intros
@item C-c R
Refine
@end table
@node LEGO tags
@section LEGO tags
The LEGO Proof General provides the program @file{legotags} to generate
tags for LEGO proof scripts. Invoking @samp{legotags *.l} produces a
file @file{TAGS} for all LEGO modules in the current directory. The LEGO
library itself is shipped out with all its modules already being tagged.
See @ref{Support for tags} for further details.
@node LEGO customizations
@section LEGO customizations
We refer to chapter @ref{Customizing Proof General} for an introduction
to the customisation mechanism. In addition to customizations at the
generic level, for LEGO you can also customize:
@defopt lego-tags
The directory of the TAGS table for the LEGO library. The default is
@code{"/usr/lib/lego/lib_Type/"}.
@end defopt
@defopt lego-help-menu-list
List of menu items, as defined in @code{easy-menu-define} for LEGO
specific help.
@end defopt
@c We don't worry about the following for now. These are too obscure.
@c lego-indent
@c lego-test-all-name
@c We also don't document any of the internal variables which have been
@c set to configure the generic Proof General and which the user should
@c not tamper with
In Xemacs 20.4, LEGO script buffer are coloured (fontified as they say)
by default. To automatically switch on fontification in FSF Emacs 20.2,
you need to set
@vindex lego-mode-hooks
@cindex font-lock colour
@lisp
(add-hook 'lego-mode-hooks 'turn-on-font-lock)
@end lisp
in your @file{~/.emacs} file.
@node Coq Proof General
@chapter Coq Proof General
@menu
* Coq specific commands::
* Coq customizations::
@end menu
@node Coq specific commands
@section Coq specific commands
@node Coq customizations
@section Coq customizations
@node Isabelle Proof General
@chapter Isabelle Proof General
@menu
* Isabelle specific commands::
* Isabelle customizations::
@end menu
@node Isabelle specific commands
@section Isabelle specific commands
@unnumberedsubsec Associated files
@cindex Associated files
In Isabelle proofscript mode, @kbd{C-c C-o} (@code{thy-find-other-file})
finds and switches to the associated theory file, that is, the file with
the same base name but extension @file{.thy} swapped for @file{.ML}.
The same function (and keybinding) switches back to an ML file from the
theory file.
@deffn Command thy-find-other-file
Find and switch to the associated ML file (when editing a theory file)
or theory file (when editing an ML file).
@end deffn
@node Isabelle customizations
@section Isabelle customizations
@node Adapting Proof General to New Provers
@chapter Adapting Proof General to New Provers
Proof General has about 60 configuration variables which are set on a
per-prover basis to configure the various features. However, many of
these variables occcur in pairs (typically regular expressions matching
the start and end of some text), and you can begin by setting just a few
variables to get the basic features working.
@menu
* Skeleton example::
* Proof script settings::
* Proof shell settings::
@end menu
@node Skeleton example
@section Skeleton example
Each proof assistant supported has its own subdirectory under
@var{proof-home-directory}, used to store a root elisp file and any
other files needed to adapt the proof assistant for Proof General.
Here we show how a minimal configuration of Proof General works for
Isabelle, without any special changes to Isabelle.
@itemize @bullet
@item Make a directory called 'myassistant' under the Proof General home
directory, to put the specific customization and associated files in.
@item Add a file myassistant.el to the new directory.
@item Edit proof-site.el to add a new entry to the
@var{proof-assistants-table} variable. The new entry should
look like this:
(myassistant "My New Assistant" "\\.myasst$")
The first item is used to form the name of the internal variables
for the new mode as well as the directory and file where it loads
from. The second is a string, naming the proof assistant.
The third item is a regular expression to match names of
proof script files for this assistant. See the documentation
of @var{proof-assistants-table} for more details.
@item Define the new modes in myassistant.el, by looking at
the files for the currently supported assistants for example.
Basically you need to define some modes using @code{define-derived-mode}
and set the configuration variables. You could begin by setting
a minimum number of the variables, then adjust the
settings via the customize menus, under Proof-General -> Internals.
@end itemize
@node Proof script settings
@section Proof script settings
@node Proof shell settings
@section Proof shell settings
@menu
* Special annotations::
@end menu
@node Special annotations
@unnumberedsubsec Special annotations
@node Internals of Proof General
@chapter Internals of Proof General
@menu
* Proof Script Mode::
* Proof Shell Mode::
* Handling Multiple Files::
@end menu
@node Proof Script Mode
@section Proof Script Mode
@node Proof Shell Mode
@section Proof Shell Mode
@node Handling Multiple Files
@section Handling Multiple Files
@cindex Multiple Files
@c
@c
@c CHAPTER: Obtaining and Installing Proof General
@c
@c
@node Credits and References
@chapter Credits and References
@menu
* Credits::
* References::
@end menu
@node Credits
@unnumberedsec Credits
LEGO Proof General was written by Thomas Kleymann and Dilip Sequeira.
Coq Proof General was written by Healfdene Goguen.
Isabelle Proof General was written by David Aspinall.
The generic base for Proof General was developed by all four of us.
Thomas Kleymann provided the impetus to develop a generic Emacs
interface, following ideas used in Projet CROAP, and with the help of
Yves Bertot. David Aspinall provided the Proof General name and images.
An early version of this manual was prepared by Dilip Sequeira. The
present version was written by David Aspinall and Thomas Kleymann.
@node References
@unnumberedsec References
Script management as used in Proof General is described in the paper:
@itemize @bullet
@item
Yves Bertot and Laurent Th@'ery. A generic approach to building
user interfaces for theorem provers. To appear in Journal of
Symbolic Computation.
@end itemize
Proof General has the beginnings of support for proof by pointing,
as described in the document:
@itemize @bullet
@item
Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. Implementing
Proof by Pointing without a
Structure Editor. LFCS Technical Report ECS-LFCS-97-368. Also published as Rapport de recherche de
l'INRIA Sophia Antipolis RR-3286
@end itemize
@c
@c
@c APPENDIX: Obtaining and Installing Proof General
@c
@c
@node Obtaining and Installing Proof General
@appendix Obtaining and Installing Proof General
Proof General has its own
@uref{http://www.dcs.ed.ac.uk/home/proofgen,home page} hosted at
Edinburgh. Visit this page for the latest news!
@menu
* Obtaining Proof General::
* Installing Proof General from tarball::
* Installing Proof General from RPM package::
* Notes for syssies::
@end menu
@node Obtaining Proof General
@section Obtaining Proof General
You can obtain Proof General from the URL
@example
@uref{http://www.dcs.ed.ac.uk/home/proofgen/download.html}.
@end example
The distribution is available in three forms
@itemize @bullet
@item A source tarball, @*
@uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.tar.gz}
@item A Linux RPM package (for any architecture), @*
@uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.noarch.rpm}
@item A developer's tarball, @*
@uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral-devel-latest.tar.gz}
@end itemize
Both the tarball and the RPM package include the generic elisp code,
code for LEGO, Coq, and Isabelle, installation instructions (reproduced
below) and this documentation.
@c was Installing Proof General from @file{.tar.gz}
@node Installing Proof General from tarball
@section Installing Proof General from tarball
Copy the distribution to some directory @var{mydir}.
Unpack it there. For example:
@example
# cd @var{mydir}
# gunzip ProofGeneral-@var{version}.tar.gz
# tar -xpf ProofGeneral-@var{version}.tar
@end example
If you downloaded the version called @var{latest}, you'll find it
unpacks to a numeric version number.
Proof General will now be in some subdirectory of @var{mydir}. The name
of the subdirectory will depend on the version number of Proof General.
For example, it might be @file{ProofGeneral-2.0}. It's convenient to
link it to a fixed name:
@example
# ln -sf ProofGeneral-2.0 ProofGeneral
@end example
Now put this line in your @file{.emacs} file:
@lisp
(load-file "@var{mydir}/ProofGeneral/generic/proof-site.el")
@end lisp
This command will load @file{proof-site} which sets the Emacs load path
for Proof General and add auto-loads and modes for the assistants below:
@multitable @columnfractions .3 .3 .4
@item @b{Prover} @tab @b{Extensions} @tab @b{Modes}
@item Coq @tab @file{.v} @tab @code{coq-mode}
@item LEGO @tab @file{.l} @tab @code{lego-mode}
@item Isabelle @tab @file{.thy},@file{.ML} @tab @code{isa-mode}
@end multitable
When you load a file with one of these extensions, the corresponding
Proof General mode will be entered. You can also invoke the mode
command directly.
The default names for proof assistant binaries may work on your system.
If not, you will need to set the appropriate variables. The easiest way
to do this (and most other customization of Proof General) is via the
Customize mechanism, see the menu item:
@example
Proof-General -> Customize -> @var{Name of Assistant} -> Prog Name
@end example
The Proof-General menu is available from script buffers after
Proof General is loaded. To load it manually, type
@lisp
M-x load-library RET proof RET
@end lisp
Notice that the customization mechanism is only available in Emacs 20.x
and XEmacs. If you cannot use customize, simply add a line like this:
@lisp
(setq isabelle-prog-name "/usr/bin/isabelle FOL")
@end lisp
to your @file{.emacs} file.
@node Installing Proof General from RPM package
@section Installing Proof General from RPM package
To install an RPM package you need to be root. Then type
@example
# rpm -Uvh ProofGeneral-latest.noarch.rpm
@end example
Now add the line:
@lisp
(load-file "/usr/share/emacs/ProofGeneral/generic/proof-site.el")
@end lisp
to your @file{.emacs} or the site-wide initialisation file
@file{site-start.el}.
@node Notes for syssies
@section Notes for syssies
Here are some more notes for installing Proof General in more complex
ways. Only attempt things in this section if you really understand what
you're doing.
@unnumberedsubsec Byte compilation
Compilation of the Emacs lisp files improves efficiency but can
sometimes cause compatibility problems (especially if you use more than
one version of Emacs at the same time).
You can compile Proof General by typing @code{make} in the directory
where you installed it.
@unnumberedsubsec Site-wide installation
If you are installing Proof General site-wide, you can put the
components in the standard directories of the filesystem if you prefer,
providing the variables in @file{proof-site.el} are adjusted
accordingly. Make sure that the @file{generic} and assistant-specific
elisp files are kept in subdirectories (@file{coq}, @file{isa},
@file{lego}) of @code{proof-home-directory} so that the autoload
directory calculations are correct.
To prevent every user needing to edit their own @file{.emacs} files, you
can put the @code{load-file} command to load @file{proof-site.el} into
@file{site-start.el} or similar. Consult the Emacs documention for more
details if you don't know where to find this file.
@unnumberedsubsec Removing support for unwanted provers
You cannot run more than one instance of Proof General at a time: so if
you're using Coq, visiting an @file{.ML} file will not load Isabelle
Proof General, and the buffer remains in fundamental mode. If there are
some assistants supported that you never want to use, you can remove
them from the variable @code{proof-assistants} in @file{proof-site.el}
to solve this problem.
Via the Customize mechanism, see the menu:
@example
Options -> Customize -> Emacs -> External -> Proof General
@end example
or, after loading Proof General, in a proof script buffer
@example
Proof-General -> Customize
@end example
@c
@c
@c APPENDIX: Known bugs and workarounds
@c
@c
@node Known bugs and workarounds
@appendix Known bugs and workarounds
We only mention a few important problems here. The list is not a
description of all bugs and maybe out of date. @*
Please consult the file
@uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS,@file{BUGS}}
in the distribution for more detailed and up-to-date information. @*
If you discover a problem which isn't mentioned in @file{BUGS}, please
let us know by sending a note to @code{proofgen@@dcs.ed.ac.uk}.
@menu
* Bugs at the generic level::
* Bugs specific to LEGO Proof General::
* Bugs specific to Coq Proof General::
@end menu
@node Bugs at the generic level
@section Bugs at the generic level
@unnumberedsubsec Undo in XEmacs
Ordinary undo in script buffer can edit the "uneditable region" in
XEmacs. This doesn't happen in FSFmacs. Test case: Insert some
nonsense text after the locked region. Kill the line. Process to the
next command. Press @kbd{C-x u}, nonsense text appears in locked
region.
@strong{Workaround:} be careful with undo.
@unnumberedsubsec Pressing keyboard quit @kbd{C-g}
Using @kbd{C-g} can leave script management in a mess. The code is not
properly protected from Emacs interrupts.
@strong{Workaround:} Don't type @kbd{C-g} while script management is
processing. If you do, use @code{proof-restart-scripting} to restart
the system.
@unnumberedsubsec One prover at a time
You can't use more than one proof assistant at a time in the same Emacs
session. Attempting to load Proof General for a second prover will
fail, leaving a buffer in fundamental mode instead of the Proof General
mode for proof scripts.
@strong{Workaround:} stick to one prover per Emacs session, make sure
that the proof-assistants variables only enables Proof General for the
provers you need.
@node Bugs specific to LEGO Proof General
@section Bugs specific to LEGO Proof General
Getting retracting right is tricky when working on proofs.
@unnumberedsubsec Definitions in a proof state
A thorny issues are local
definitions in a proof state. LEGO cannot undo them explicitly.
@strong{Workaround:} retract back to a command before a definition.
@unnumberedsubsec Normalisation in proofs
Normalisation commands such as @samp{Dnf}, @samp{Hnf} @samp{Normal}
cannot be undone in a proof state by the Proof General.
@strong{Workaround:} retract back to the start of the proof.
@unnumberedsubsec Not saving proofs.
After LEGO has issued a @samp{***
QED ***} you may undo steps in the proof as long as you don't issue a
@samp{Save} command or start a new proof. The LEGO Proof General assumes
that all proofs are terminated with a proper @samp{Save} command.
@strong{Workaround:} Always issue a @samp{Save} command after completing
a proof. If you forget one, you should retract to a point before the
offending proof development.
@node Bugs specific to Coq Proof General
@section Bugs specific to Coq Proof General
The collection of tactics which Proof General is aware of is hard-wired.
Thus, user-defined tactics cannot be retracted.
@strong{Workaround:} You may need to retract to the start of the proof.
@node Plans and ideas
@appendix Plans and ideas
@node Variable Index
@unnumbered Variable Index
@printindex vr
@node Function Index
@unnumbered Function Index
@printindex fn
@node Concept Index
@unnumbered Concept Index
@printindex cp
@contents
@bye
@c OLD TEXI STUFF HERE
@b{Proof General} is a generic Emacs interface for proof assistants. It
works ideally under XEmacs, but can also be used with Emacs 19.
It is supplied ready-customised for these proof assistants:
@itemize @bullet
@item
@b{LEGO Proof General} for LEGO Version 1.3.1@*
by Thomas Kleymann and Dilip Sequeira
@item
@b{Coq Proof General} for Coq Version 6.2@*
by Healfdene Goguen
@item
@b{Isabelle Proof General} for Isabelle 98-1@*
by David Aspinall
@end itemize
Proof General itself was written by the above with help from Yves Bertot
and using ideas from Projet CROAP.
Proof General is suitable for use by pacifists and Emacs lovers alike.
The code is designed to be generic, so you can adapt Proof General to
other proof assistants if you know a little bit of Emacs Lisp. Our aim
is provide a powerful and configurable Emacs mode which helps
user-interaction with interactive proof assistants.
Please help us with this aim! Configure Proof General for your proof
assistant, by adding features at the generic level wherever possible.
Send ideas, comments, patches, code to @email{proofgen@@dcs.ed.ac.uk}.
Please feel free to download Proof General to customize it for another
system, and tell us how you get on.
******************
@menu
* Introduction::
* Commands::
* Multiple Files::
* An Active Terminator::
* Proof by Pointing::
* Walkthrough::
* LEGO mode::
* Coq mode::
* Known Problems::
* Internals::
* Variable Index::
* Function Index::
* Concept Index::
@end menu
@node Introduction, Commands, Top, Top
@comment node-name, next, previous, up
@unnumberedsec Introduction
A @strong{Script Buffer} is the primary buffer for developing proof
scripts. Its major mode is @emph{proof mode}. A script buffer is divided
into three regions:
@itemize @bullet
@item The @emph{Locked} region appears in blue (underlined on monochrome
displays) and contains commands which have been sent to the proof process
and verified. The commands in the locked region cannot be edited.
@item The @emph{Queue} region appears in pink (inverse video) and contains
commands waiting to be sent to the proof process. Like those in the
locked region, these commands can't be edited.
@item The @emph{Editing} region contains the commands the user is working
on, and can be edited as normal Emacs text.
@end itemize
These three regions appear in the buffer in the order above; that is,
the locked region is always at the start of the buffer, and the editing
region always at the end. The queue region only exists if there is input
waiting to be sent to the proof process.
Proof mode has two operations which transfer commands between these
regions: assertion and retraction. These cause commands to be sent to
the proof process. The @emph{Process Buffer} records the complete
communication between the prover and the Script Buffers. Error messages
and other important messages are highlighted in the Process Buffer. The
current proof obligations (if any) are always visible in the @emph{Goals
Buffer}.
Proof General is generous. It is not a perfect interface and users may
occasionaly want to freely interact with the prover without being
watched over by the Proof General. Users may interact @emph{directly}
with the prover by entering text in the Process Buffer instead of
invoking commands in a Script Buffer. Proof mode supports a variety of
means to interact with the prover. Try these first!
@cindex Assertion
@strong{Assertion} causes commands from the editing region to be
transferred to the queue region and sent one by one to the proof
process. If the command is accepted, it is transferred to the locked
region, but if an error occurs it is signalled to the user, and the
offending command is transferred back to the editing region together
with any remaining commands in the queue.
@cindex Retraction
@strong{Retraction} causes
commands to be transferred from the locked region to the editing region
(again via the queue region) and the appropriate 'undo' commands to be
sent to the proof process.
As commands are transferred to the locked region, they are aggregated
into segments which constitute the smallest units which can be
undone. Typically a segment consists of a declaration or definition, or
all the text from a `goal' command to the corresponding `save' command,
or the individual commands in the proof of an unfinished goal. As the
mouse moves over the the region, the segment containing the pointer will
be highlighted.
Commands in the editing region can be freely edited while
commands in the queue are transferred to the proof process. However,
assertion and retraction commands can only be issued when the queue is
empty.
@node Commands, Multiple Files, Introduction, Top
@section Proof Mode Commands
@table @kbd
@item C-c C-b
assert the commands in the buffer.
@item C-c return
assert the commands in the editing region up to and
including the one containing the point.
@item C-c u
retract the segments in the locked region back to and
including the one containing the point. If point is outside the *Locked*
region, the last segment is undone.
@item C-c C-u
retract the last segment in the locked region, and kill the text in it.
@footnote{Be careful with this, as it may delete more than you anticipate.
However, you can always recover the killed text using Emacs Undo.}
@item C-c '
move the point to the end of the locked region. If you are in a script
buffer other than the active scripting buffer, this will also transfer
you to the active one.
@item C-c C-e
move the point to the next terminator
@item C-c C-p
display the proof state in the goals buffer
@item C-c c
display the context in the process buffer
@item C-c h
print proof-system specific help text in the process buffer
@item C-c C-c
interrupt the process. This may leave script management or the
proof process (or both) in an inconsistent state.
@item C-c C-z
move the end of the locked region backwards to the end of the segment
containing the point. @footnote{Don't try this one at home, kids.}
@item C-c C-t
Send the command at the point to the subprocess, not
recording it in the locked region. @footnote{This is supplied in order
to enable the user to test the types and values of expressions. There's
some checking that the command won't change the proof state, but it
isn't foolproof.}
@item C-c C-v
Request a command from the minibuffer and send it to
the subprocess. Currently no checking whatsoever is done on the command.
@end table
The command @code{proof-restart-script} can be used to completely
restart script management.
@node Multiple Files, An Active Terminator, Commands, Top
@section Multiple Files
Proof mode has a rudimentary facility for operating with multiple files
in a proof development. This is currently only supported for LEGO. If
the user invokes script management in a different buffer from the one in
which it is running, one of two prompts will appear:
@itemize @bullet
@item ``Steal script management?''
if Emacs doesn't think the file is already part of the proof development
@item ``Reprocess this file?''
if Emacs thinks the file is already included in the proof process. If
the user confirms, Emacs will cause the proof process to forget the
contents of the file, so that it is processed afresh.
@end itemize
Currently this facility requires each script buffer to have a
corresponding file.
When working with script management in multiple buffers, it is easy
to lose track of which buffer is the current script buffer. As a mnemonic
aid, the word @samp{Scripting} appears in the minor mode list of the
active scripting buffer.
Caveats:
@itemize @minus
@item Note that if processing a buffer causes other files to be loaded
into the LEGO process, those files will be imported from disk rather
than from any Emacs buffer in which it is being edited, i.e.@: if your
file is going to be included indirectly, save it.
@item However much you move around the file system in Emacs, the
LEGOPATH will be the LEGOPATH you started with. No concept of
"current directory" is currently supported.
@end itemize
@node An Active Terminator, Proof by Pointing, Multiple Files, Top
@section An Active Terminator
Proof mode has a minor mode which causes the terminator to become
active. When this mode is active, pressing the terminator key (@kbd{;}
for LEGO, @kbd{.} for Coq) outside a comment or quote will cause the
character to be entered into the buffer, and all the commands in the
editing region up to the point to be asserted.
This mode can be toggled with the command
`proof-active-terminator-minor-mode' (@kbd{C-c ;} or @kbd{C-c .})
@node Proof by Pointing, Walkthrough, An Active Terminator, Top
@section Proof by Pointing
@emph{This mode is currently very unreliable, and we do not guarantee
that it will work as discussed in this document.}
Proof by pointing is a facility whereby proof commands can be generated
by using the mouse to select terms. When proving a goal, a summary of
the current proof state will appear in the goals buffer. By moving
the mouse over the buffer, the structure of the goal and hypothesis
terms will be shown by highlighting.
If a selection is made using the second (usually the middle) mouse
button, Emacs will generate the appropriate commands, insert them in the
script buffer, and send them to the proof process. These commands are
aggregated in the locked region as a single segment, so that a
mouse-generated command sequence can be retracted with a single
retraction command.
Further Information about proof by pointing may be found in the paper
@cite{User Interfaces for Theorem Provers} by Yves Bertot and Laurent
Thery, to appear in @cite{Information and Computation}, from which
the following example is taken.
@menu
* Proof by Pointing Example:: An example using proof by pointing
@end menu
@node Proof by Pointing Example, ,Proof by Pointing,Proof by Pointing
Suppose we wish to prove the lego term:
@example
(((p a) \/ (q b)) /\ @{x:Prop@}(p x) -> (q x)) -> (Ex ([x:Prop] q(x)));
@end example
Asserting this goal will result in the proof state
@example
?0 : ((p a \/ q b) /\ @{x:Prop@}(p x)->q x)->Ex ([x:Prop]q x)
@end example
appearing in the goals buffer. Suppose our strategy is to use a
case analysis on the disjunction, starting with the @samp{p(a)} subterm.
Clicking on this term will cause script management to insert the following
command sequence in the script buffer, and execute it.
@example
Intros H; Refine H; Intros H0 H1;
Refine or_elim H0 Then Intros H2; Try Refine H2;
@end example
The goals buffer will then read
@example
H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x
H0 : p a \/ q b
H1 : @{x:Prop@}(p x)->q x
H2 : p a
?10 : Ex ([x:Prop]q x)
@end example
Clicking on the subterm @samp{(p x)} in the hypothesis H1 will instruct
script management to prove an instance of @samp{(p x)} and deduce the
corresponding @samp{(q x)}. The commands
@example
allE H1; intros +1 H3; Refine impl_elim H3; Try Assumption;
@end example
are inserted and executed, leaving the proof state as
@example
H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x
H0 : p a \/ q b
H1 : @{x:Prop@}(p x)->q x
H2 : p a
H3 : (p a)->q a
?20 : (q a)->Ex ([x:Prop]q x)
@end example
Now clicking on the @samp{q x)} subterm in ?20 will prove the subgoal. We are
left with the other half of the original case analysis:
@example
H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x
H0 : p a \/ q b
H1 : @{x:Prop@}(p x)->q x
H2 : q b
?26 : Ex ([x:Prop]q x)
@end example
Clicking on @samp{q x} proves the goal.
@node Walkthrough, LEGO mode, Proof by Pointing, Top
@section A Walkthrough
Here's a LEGO example of how script management is used.
First, we turn on active terminator minor mode by typing @kbd{C-c ;}
Then we enter
`Module Walkthrough Import lib_logic;'
The command should be lit in pink (or inverse video if you don't have a
colour display). As LEGO imports each module, a line will appear in the
minibuffer showing the creation of context marks. Eventually the
command should turn blue, indicating that LEGO has successfully
processed it. Then type (on a separate line if you like)
@samp{Goal bland_commutes: @{A,B:Prop@} (and A B) -> (and B A);}
The goal should be echoed in the goals buffer.
@samp{Intros;}
Whoops! @kbd{C-c C-u} to pretend that didn't happen.
@samp{intros; andI;}
A proof summary will appear in the goals buffer. We could solve the
goal by pointing now, but we'll stay with the keyboard.
@samp{Refine H; intros; Immed; Refine H; intros; Immed;}
finishes the Goal.
@samp{Save bland_commutes;}
Moving the mouse pointer over the locked region now reveals that the
entire proof has been aggregated into a single segment. Suppose we
decide to call the goal something more sensible. Moving the cursor up
into the locked region, somewhere between `Goal' and `Save', we enter
@kbd{C-c u}. The segment is transferred back into the editing
region. Now we correct the goal name, move the cursor to the end of the
buffer, and type @kbd{C-c return}. Proof mode queues the commands for
processing and executes them.
@node LEGO mode, Coq mode, Walkthrough, Top
@section LEGO mode
LEGO mode is a mode derived from proof mode for editing LEGO scripts.
There are some abbreviations for common commands, which
add text to the buffer:
@table @kbd
@item C-c i
intros
@item C-c I
Intros
@item C-c R
Refine
@end table
@node Coq mode, Known Problems, LEGO mode, Top
@section Coq mode
Coq mode is a mode derived from proof mode for editing Coq scripts.
As well as custom popup menus, it has the following commands:
@table @kbd
@item C-c C-s
search for items in the library of a given type. This runs the
@kbd{Search} command of Coq.
@end table
In addition, there are some abbreviations for common commands, which
add text to the buffer:
@table @kbd
@item C-c I
Intros
@item C-c a
Apply
@end table
@node Known Problems, Internals, Coq mode, Top
@section Known Problems
Since Emacs is pretty flexible, there are a whole bunch of things you
can do to confuse script management. When it gets confused, it may
become distressed, and may eventually sulk. In such instances
@code{proof-restart-script-management} may be of use.
A few things to avoid:
@itemize @minus
@item If you're using script management with multiple files, don't start
changing the file names.
@item Script Management doesn't understand how to undo @code{Discharge}
commands in LEGO, and any attempts it makes to do so may leave it in an
inconsistent state. If you're undoing the effects of a @code{Discharge}
command, retract back to the declaration of whatever gets discharged.
@item Proof by Pointing doesn't work very well, and is inefficiently
implemented.
@item The locked and queue regions are not quite read-only: in particular
Emacs Undo can insert text into them.
@item When a LEGO import command fails, the created "Mark" is not
forgotten, and the proof process thinks the file has been included. So
if you assert the command again, it will probably be accepted by LEGO,
because the relevant mark is in the namespace.
@end itemize
Fixes for some of these may be provided in a future release.
@node Internals, Variable Index, Known Problems, Top
@comment node-name, next, previous, up
@section Internals
@menu
* Granularity of Atomic Command Sequences::
* Handling Multiple Files::
* Adding A New Proof Assistant::
* Literature::
@end menu
@node Granularity of Atomic Command Sequences, Handling Multiple Files, Internals, Internals
@comment node-name, next, previous, up
@unnumberedsubsec Granularity of Atomic Commands
@cindex Granularity of Atomic Sequences
@cindex Retraction
@cindex Goal
@cindex ACS (Atomic Command Sequence)
The *Locked* region of a script buffer contains the initial segment of
the proof script which has been processed successfully. It consists of
atomic sequences of commands (ACS). Retraction is supported to the
beginning of every ACS. By default, every command is an ACS. But the
granularity of atomicity can be adjusted for different proof assistants.
This is essential when arbitrary retraction is not supported. Usually,
after a theorem has been proved, one may only retract to the start of
the goal. One needs to mark the proof of the theorem as an ACS.
@vtable @code
@item proof-atomic-sequents-list
is a list of instructions for setting up ACSs. Each instruction is a
list of the form @code{(@var{end} @var{start} &optional
@var{forget-command})}. @var{end} is a regular expression to recognise
the last command in an ACS. @var{start} is a function. Its input is the
last command of an ACS. Its output is a regular expression to recognise
the first command of the ACS. It is evaluated once and the output is
successively matched against previously processed commands until a match
occurs (or the beginning of the current buffer is reached). The region
determined by (@var{start},@var{end}) is locked as an ACS. Optionally,
the ACS is annotated with the actual command to retract the ACS. This is
computed by applying @var{forget-command} to the first and last command
of the ACS.
@end vtable
@node Handling Multiple Files, Adding A New Proof Assistant, Granularity of Atomic Command Sequences, Internals
@comment node-name, next, previous, up
@unnumberedsubsec Handling Multiple Files
@cindex Multiple Files
Large proof developments are typically spread across multiple files.
Many provers support such developments by keeping track of dependencies
and automatically processing scripts. Proof General supports this
mechanism.
However, the prover must let the Proof General know whenever
it processes a file directly. Such files are being marked by Proof
General as having been processed by an atomic action (regardless of
whether an error occurs or not). The file can then only be edited after
retracting to the beginning of the file.
When retraction is requested in a buffer which is not the current
script, Proof General duely retracts in this buffer. It then arranges a
little conference with the prover to find out which other files have
also been retracted. With this strategy, Proof General doesn't have a
hard time to keep track of dependencies.
@vindex proof-shell-eager-annotation-start
@vindex proof-shell-eager-annotation-end
Proof General considers @var{output} delimited by the the two regualar
expressions @code{proof-shell-eager-annotation-start} and
@code{proof-shell-eager-annotation-end} as being important. It displays
the @var{output} in the Response buffer and analyses their contents further.
Among possibly other important messages characterised by these regular
expressions, the prover must tell the interface whenver it processes a
file and retracts across file boundaries.
@vtable @code
@item proof-included-files-list
records the file history. Whenever a new file is being processed, it
gets added to the
front of the list. When the prover retracts across file boundaries, this
list is resynchronised. It contains files in canonical truename format
@inforef{Truenames,,lispref}.
@item proof-shell-process-file
is either nil or a tuple of the
form (@var{regexp}, @var{function}). If @var{regexp} matches a substring
of @var{str},
then the function @var{function} is invoked with input @var{str}. It must return a script file
name (with complete path)
the system is currently processing. In practice, @var{function} is
likely to inspect the match data. @inforef{Match Data,,lispref}.
Care has to be taken in case the prover only reports on compiled
versions of files it is processing. In this case, @var{function} needs
to reconstruct the corresponding script file name.
The
new (true) file name is added to the front of @code{proof-included-files-list}.
@item proof-shell-retract-files-regexp
is a regular expression. It indicates that the prover has retracted
across file boundaries. At this stage, Proof General's view of the
processed files is out of date and needs to be updated with the help of
the function @code{proof-shell-compute-new-files-list}.
@end vtable
@ftable @code
@item proof-shell-compute-new-files-list
Takes as argument the current output of the prover. It needs to return
an up to date list of all processed files. Its output is stored in
@code{proof-included-files-list}. In practice, this function is likely
to inspect the previous (global) variable
@code{proof-included-files-list} and the match data
@inforef{Match Data,,lispref} triggered by @code{proof-shell-retract-files-regexp}.
@end ftable
@node Adding A New Proof Assistant, Literature, Handling Multiple Files, Internals
@comment node-name, next, previous, up
@unnumberedsubsec Adding Support for a New Proof Assistant
Suppose your new assistant is
called myassistant.
@itemize @minus
@item Make a directory called 'myassistant' under the Proof General home
directory, to put the specific customization and associated files in.
@item Add a file myassistant.el to the new directory.
@item Edit proof-site.el to add a new entry to the
@var{proof-assistants-table} variable. The new entry should
look like this:
(myassistant "My New Assistant" "\\.myasst$")
The first item is used to form the name of the internal variables
for the new mode as well as the directory and file where it loads
from. The second is a string, naming the proof assistant.
The third item is a regular expression to match names of
proof script files for this assistant. See the documentation
of @var{proof-assistants-table} for more details.
@item Define the new modes in myassistant.el, by looking at
the files for the currently supported assistants for example.
Basically you need to define some modes using @code{define-derived-mode}
and set the configuration variables. You could begin by setting
a minimum number of the variables, then adjust the
settings via the customize menus, under Proof-General -> Internals.
@end itemize
@node Literature, , Adding A New Proof Assistant, Internals
@comment node-name, next, previous, up
@unnumberedsubsec Literature
The current version supports Script Management as documented in:
@itemize @bullet
@item
Yves Bertot and Laurent Th@'ery. A generic approach to building
user interfaces for theorem provers. To appear in Journal of
Symbolic Computation.
@end itemize
It has the beginnings of support for Proof by Pointing, as documented in:
@itemize @bullet
@item
Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. Implementing
Proof by Pointing without a
Structure Editor. LFCS Technical Report ECS-LFCS-97-368. Also published as Rapport de recherche de
l'INRIA Sophia Antipolis RR-3286
@end itemize
|