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
|
INSTALLATION PROCEDURE FOR SSREFLECT
------------------------------------
Summary:
- Requirements
- Building Ssreflect
- Customization of the Proof General Emacs interface -
REQUIREMENTS
============
- Coq version 8.4 compiled with CamlP5
BUILDING SSREFLECT
==================================================
- We suppose that the Coq system has been compiled from sources and installed
on your system using a standard installation process.
- Your COQBIN environment variable must be point to directory where Coq's
binaries are.
- Your PATH environment variable value must make Coq binaries (coqtop,
coq_makefile,...) accessible. E.g. export PATH="$COQBIN:$PATH"
- Download and unpack the archive of the ssreflect distribution in a directory
whose name does not contain spaces (like " Documents and Settings" ...).
- Go to the root of the ssreflect directory creating by the previous
unpack and type `make && make install`. Note that if Coq is installed
system wide, like in /usr/local/, then `make install ` needs superuser
rights. In this case, on a modern Unix distribution, you can type
`make && sudo make install`.
- Note for Mac OSX users: If you encounter a "stack overflow" error message,
then set the following environment variable and try again:
OCAMLOPT=ocamlopt.opt
- Note for Mac OSX users and Windows users: If you encounter a linking error
it may be caused by an old version of OCaml that does not support
dynamic loding of plugins on you platform. Edit the Make file and uncomment
the lines marked for static linking. In this way a statically linked
binary bin/ssrcoq will be produced. It is up to you to copy it inside $COQBIN.
CUSTOMIZATION OF THE PROOF GENERAL EMACS INTERFACE
==================================================
The ssreflect distribution comes with a small configuration file
pg-ssr.el to extend ProofGeneral (PG), a generic interface for
proof assistants based on the customizable text editor Emacs, to the
syntax of ssreflect.
The >= 3.7 versions of ProofGeneral support this extension.
- Following the installation instructions, unpack the sources of PG in
a directory, for instance <my-pgssr-location>/ProofGeneral-3.7, and add
the following line to your .emacs file:
- under Unix/MacOS:
(load-file
"<my-pg-location>/ProofGeneral-3.7/generic/proof-site.el" )
- under Windows+Cygwin:
(load-file
"C:\\<my-pg-location>\\ProofGeneral-3.7\\generic\\proof-site.el")
where <my-pg-location> is the location of your own ProofGeneral
directory.
-Immediately after the previous line added to your .emacs, add this
one:
(load-file "<my-pgssr-location>/pg-ssr.el") respectively
(load-file "<my-pgssr-location>\\pg-ssr.el") for Windows+Cygwin
users, where <my-pgssr-location> is the location of your pg-ssr.el file.
Coq sources have a .v extension. Opening any .v file should
automatically launch ProofGeneral. Try this on a foo.v file.
In the menu 'ProofGeneral', choose the item:
'Advanced/Customize/Coq/Coq Prog Name' Change the value of the
variable to
<my-ssreflect-location>/bin/ssrcoq
or
<my-ssreflect-location>\\bin\\ssrcoq
for Windows+Cygwin users, where <my-ssreflect-location> is the location of
your coq directory.
|
