forked from HoTT/Coq-HoTT
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathINSTALL.txt
153 lines (102 loc) · 5.24 KB
/
INSTALL.txt
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
# QUICK INSTALLATION INSTRUCTIONS
1. Install a custom Coq from https://github.com/HoTT/coq. This is a fork
of the trunk and is compatible with standard Coq 8.4 trunk, except that
it supports special command-line options that turn on the homotopy theory
interpretation.
2. Get the HoTT library at https://github.com/HoTT/HoTT.git. Go at the
root of the HoTT created directory.
3. If you installed custom Coq so that it is found in the `PATH`, run
./configure
make
If you installed custom Coq in a secret place, tell ./configure
where to find it as follows:
./configure COQBIN=<absolute-directory-containing-coq-executables>
make
4. You can now use the HoTT library in place by running ./hoqtop and
./hoqc. You can also use ./hoqide which is the version of coqide
running the hoqtop toplevel if you have compiled it successfully.
5. The library is loaded with `Require Import HoTT.Homotopy`.
6. You can install the library globally with `make install`.
# LONG INSTALLATION INSTRUCTIONS
## PREREQUISITES
The HoTT library requires a custom version of Coq which supports the
command-line options `-relevant-equality` and
`-warn-universe-inconsistencies`. The first one changes the
interpretation of equality to one that conforms to the
homotopy-theoretic interpretation, while the second one is an ugly
temporary hack that turns universe inconsistencies intro warning
rather than errors.
At present only a fork of the Coq trunk supports these options, but we
hope to get them into the official Coq soon. Unfortunately for you
that means you will have to compile a version of Coq, available at
https://github.com/HoTT/coq
If you have never compiled Coq you may prefer to ask a friend for
help. If you feel brave you should try doing it yourself:
1. Obtain the custom Coq fork. If you have git clone the fork with
git clone https://github.com/HoTT/coq.git
If you do not have git, you may still download the files as an
archive file at
https://github.com/HoTT/coq/zipball/trunk (but it is better for you
in the long run to learn git).
2. Compile Coq, as explained in the INSTALL.txt file of Coq
distribution. You will need some prerequisites for compilation, such
as OCaml 3.11.2 or later.
If you do not want the custom Coq to override one that you already
have installed, configure Coq with either `./configure -local` so
that it will work in-place, or use
`./configure -prefix <dir>`, as explained by `./configure -help`.
## INSTALLATION OF HoTT
Once you have installed the correct version of Coq, as explained in
PREREQUISITES, you proceed as follows. Clone the HoTT repository with
git clone https://github.com/HoTT/HoTT.git
Even better, if you would like to contribute to HoTT, first fork the
repository on github and then use your own fork. This way you will be
able to make pull requests.
If you do not want to deal with git at all, you may download an
archive of HoTT at https://github.com/HoTT/HoTT/zipball/master and
unpack that. We do not recommend this option because the HoTT library
is under heavy development and you want to be able to easily track
changes.
Next you should configure the HoTT library:
1. If you installed the custom Coq as your default version of Coq,
which means that it it can be fond in PATH, run
./configure
in the HoTT directory.
2. If you installed the custom Coq somewhere special or configured it
with `-local`, you should tell ./configure where to find the custom
Coq:
./configure COQBIN=<directory-containing-coq-executables>
where you should specify the *absolute* path name (starting with /)
of the directory which contains `coqtop`, `coqc`, etc.
Often coqide is a bit tricky to compile. If you did not compile
coqide, you can tell the configure script to skip installing hoqide by
providing the --without-coqide option.
To compile the HoTT library type
make
Because it is a bit tricky to run Coq with a custom standard library,
we provided scripts `hoqtop` and `hoqc` that do this for you, so you
can run
./hoqtop
directly from the HoTT directory to start using the library. Load it
with
Require Import HoTT.Homotopy.
There is also `hoqc` for compiling files. You may prefer to install
`hoqtop`, `hoqc` and the library files globally, in which case you
type
sudo make install
By default the files will be installed in `/usr/local/bin` and
`/usr/local/share/hott`. You can change the location by using
standard `configure` parameters when you run it. For example
./configure --bindir=$HOME/bin --datadir-$HOME/stuff
will install `hoqtop` and `hoqc` in the `bin` subdirectory of your
home directory and the HoTT library in `stuff/hott` subdirectory of
your home directory.
If you are using ProofGeneral (PG), do not forget to change the name
of the Coq program called by PG. For instance you can edit the name of
the executable called by PG by typing 'M-x customize-variable', then
'proof-prog-name' which displays a customization utility. An other
option is to type 'M-x customize-variable', then
'proof-prog-name-ask', to click on the 'Toogle' button in front of
Proof Prog Name Ask and to save this for future sessions. This will
prompt PG to ask you for the name of the coq toplevel to be used each
time you start evaluating a file.