forked from coq-community/corn
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathREADME
151 lines (127 loc) · 5.52 KB
/
README
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
C-CoRN, the Coq Constructive Repository at Nijmegen
---------------------------------------------------
This file contains some basic information about C-CoRN.
PREREQUISITES
-------------
C-CoRN (notice the capitals) is designed to run with Coq version 8.0.
A (no longer updated) version compatible with version 7.4 is also
available.
Before installing C-CoRN, please check that you have:
- Coq version 8.0 (a compiled source tree, not only a binary package)
- the OCaml you used to compile Coq
- at least 128MiB RAM memory available (and preferably more, especially if
you plan to use the formalization of Real Analysis).
- GNU make version 3.80 or later
- a POSIX-compliant operating system. This means Unix, a clone
thereof or a good emulation layer on top of another OS. In
particular, *hard* links must be supported by the file system.
- the GNU Bourne Again SHell (we use some bashisms)
In order for C-CoRN to work, you need to set some environment variables.
We advise you to do this inside a .bash_profile or similar.
- COQTOP should be set to the location of the Coq sources (e.g.
/usr/local/src/coq-8.0/)
- COQBIN should be set to the directory where the Coq binaries can
be found, if different from ${COQTOP}/bin/.
FILES
-----
Any distribution of C-CoRN should include the following files at root
level:
- Makefile
- Makefile.{realpath,common}
- README
- tree.ps.gz
and the directories
- doc
- tactics
- tools
According to which version you downloaded you will also get some or all
of the following directories:
- algebra
- complex
- fta
- ftc
- metrics
- model
- reals
- transc
If you obtained C-CoRN via CVS, you will also have a directory named
devel/.
Important note: if you plan to regularly update C-CoRN, you should
keep any files you work on under devel/ or out of the CoRN tree
altogether. This will ensure that subsequent updates will not
overwrite your developments.
COMPILING
---------
C-CoRN now comes with a general purpose Makefile. This allows you to
uniformly:
- (re)compile C-CoRN;
- automatically generate postscript or html documentation from C-CoRN;
- refresh the list of dependencies;
- see which commands are actually used for these tasks.
The default behaviour of make (with no target specified) is to recompile
all files that have been changed since the last compilation, as well as
everything that depends on these files. The following targets are also
allowed:
dep -> recalculates the dependencies of modified files
Note that this is called automatically before
compilation, you normally don't need to call it
explicitly.
clean -> removes all .vo, .cmx, .cmi, .cmo, .o, .vi, .g, emacs
backup (*~) files, the CoRN toplevel and compiler and
the globals file. Also does depclean.
depclean -> forget all computed dependencies. Useful to force a
full recomputation of the dependencies.
distclean -> removes things that should not be distributed from a
CVS checkout.
doc -> produces both postscript and html documentation
doc-clean -> removes all documentation files
doc-html -> produces only html documentation
doc-ps -> produces only postscript documentation
showcommands -> prints the actual command line that will be used to
compile files
human -> setup CoRN for human convenience (see `HUMAN CONVENIENCE' section)
ide -> setup CoRN for human convenience using coqide
Besides these, flags can also be given to make. Currently, the following
are recognized.
devel="space separated directories list"
-> compile the files in these directory trees, too. Between a
command with some value of devel (e.g. unset) and a
command with some other value (e.g. set to anything but
empty), you _must_ force a complete recompilation of the
dependencies (make depclean). For example, to compile all
files in the devel/ sub-directory and all its
subdirectories (like devel=yes did before) use
devel=./devel . To compile files in devel/lcf and
devel/foo, use devel="./devel/lcf ./devel/foo" . Yes, this
means that directories containing a space in their name
won't work.
OPT=[option] -> adds [option] to the Coq command line
OCAMLC=file
OCAMLOPT=file
-> Choose an ocamlc and ocamlopt to use
COQDOC=file -> Choose a coqdoc to use
HUMAN CONVENIENCE
-----------------
CoRN now has a few facilities for the convenience of the human beings
using it. Enable with "make human", or "make ide" for coqide support
(this needs a coqide-enabled Coq).
This will create Makefiles in every directory scanned for .v files
(but will not overwrite the Makefile if any is present) so that all
make commands work from anywhere in the CoRN hierarchy.
It also populates the "bin" directory with CoRNc, CoRNtop and (with
coqide support) CoRNide. These are CoRN versions of coqc, coqtop and
coqide, respectively. We suggest you add the "bin" directory of CoRN
to your PATH.
DEPENDENCIES
------------
The distribution includes a (gzip'ed) postscript file tree.ps.gz
with the dependency tree of all the files in the standard, full,
version of C-CoRN.
OTHERS
------
More information can be found at the C-CoRN page,
http://c-corn.cs.kun.nl/
For any questions, comments, bug reports or other feel free to e-mail
lcf@cs.kun.nl.
$Id$
LocalWords: Nijmegen CoRN Coq CVS