/
Makefile.install
284 lines (251 loc) · 9.95 KB
/
Makefile.install
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
# -*- mode: makefile; -*-
# An install script, as Makefile, to set up the initial installation
# of the mizar wiki. We will probably run this only a handful of
# times.
# The following should be present in the environment or as argments to
# `make':
#
# - REPOS_BASE: the root directory where our repos -- the backend and
# the bare frontend -- will be stored
#
# - MIZFILES: the root directory of a mizar installation. It should
# contain data files mml.lar etc, the prel subdirectory, and the mml
# subdirectory.
#
# - XSL4MIZ: root directory of Josef Urban's xsl4mizar code.
#
# One can optionally specify:
#
# - MIZBIN: default: $(MIZFILES)/bin. The directory where the mizar
# binaries are held
#
# - MAKEJOBS: default 1. The degree of parallelization used by make
# when computing the initial HTML-ized presentation of the MML
#
# - NUM_ARTICLES: default 10. The length of the initial segment of
# mml.lar (taken from MIZFILES). Set it to a big value to ensure
# that the entire current MML is used; set it to a low-value for
# debugging purposes.
#
# - MWIKI_USER: default "mwiki". The name of the unix user to add that
# will preside over the whole mess.
#
# - INSTALL: default /usr/bin/install. If this is GNU install, then
# no need to adjust. (On Mac OX X, /usr/bin/install is not GNU
# install, so I need to set this value to "ginstall".)
#
# - HEAD: default /usr/bin/head. See description of INSTALL variable.
PUBLIC_REPO_NAME=mwiki-public
DEVEL_REPO_NAME=mwiki-devel
SCRATCH_BASE=$(REPOS_BASE)/scratch
PUBLIC_REPOS_BASE=$(REPOS_BASE)/public
DEVEL_REPOS_BASE=$(REPOS_BASE)/devel
PUBLIC_REPO=$(REPOS_BASE)/public/mwiki
PUBLIC_SANDBOX=$(PUBLIC_REPOS_BASE)/sandbox
PUBLIC_COMPILED_REPO=$(PUBLIC_REPOS_BASE)/compiled
DEVEL_REPO=$(REPOS_BASE)/devel/mwiki
DEVEL_SANDBOX=$(DEVEL_REPOS_BASE)/sandbox
DEVEL_COMPILED_REPO=$(DEVEL_REPOS_BASE)/compiled
BARE_PUBLIC_REPO=$(PUBLIC_REPOS_BASE)/mwiki.git
BARE_DEVEL_REPO=$(DEVEL_REPOS_BASE)/mwiki.git
REPOBIN=$(PUBLIC_REPO)/bin
MIZBIN=$(MIZFILES)/bin
MAKEJOBS=1
SHEETS=addabsrefs miz evl2dep
PERLSCRIPTS=mkxmlhead mkmmlindex duplicates
PERLMODULES=mizar
GITWEB_ROOT=/var/cache/git
NUM_ARTICLES=10
HEAD=/usr/bin/head
INSTALL=/usr/bin/install
INITIAL_SEGMENT=$(shell $(HEAD) -n $(NUM_ARTICLES) $(MIZFILES)/mml.lar)
APACHE_ROOT=
HTTPD_CONF_DIR=$(APACHE_ROOT)/etc/apache2/sites-enabled
PUBLIC_MWIKI_USER=mwiki
DEVEL_MWIKI_USER=mizdev
# .PHONY: all repo sandbox deps xml repo-miz repo-prel repo-perl repo-bin repo-xsl repo-export repo-gitinit repo-makefiles
MIZBINARIES=accom envget exporter makeenv transfer verifier
MIZROOTFILES=mml.ini mml.vct mizar.dct mizar.msg
repos: public-repos devel-repos gitweb mwiki
rm -Rf $(SCRATCH_BASE) # no need for this anymore
public-repos: public-repo-init public-sandbox public-compiled public-repo-export
chown -R $(PUBLIC_MWIKI_USER) $(PUBLIC_REPOS_BASE)
chgrp -R $(PUBLIC_MWIKI_USER) $(PUBLIC_REPOS_BASE)
devel-repos: devel-repo-init devel-sandbox devel-compiled devel-repo-export
chown -R $(DEVEL_MWIKI_USER) $(DEVEL_REPOS_BASE)
chgrp -R $(DEVEL_MWIKI_USER) $(DEVEL_REPOS_BASE)
scratch-mizfiles:
# .miz
mkdir -p $(SCRATCH_BASE)/mml
for article in hidden tarski $(INITIAL_SEGMENT); do \
$(INSTALL) --preserve-timestamps --mode=644 $(MIZFILES)/mml/$$article.miz $(SCRATCH_BASE)/mml; \
done
# prel
mkdir -p $(SCRATCH_BASE)/prel
cp -p $(MIZFILES)/prel/h/hidden.* $(SCRATCH_BASE)/prel
cp -p $(MIZFILES)/prel/*/*.dre $(SCRATCH_BASE)/prel
chown -R $(PUBLIC_MWIKI_USER) $(SCRATCH_BASE)/prel
# data
for rootfile in $(MIZROOTFILES); do \
cp -p $(MIZFILES)/$$rootfile $(SCRATCH_BASE); \
done
head -n $(NUM_ARTICLES) $(MIZFILES)/mml.lar > $(SCRATCH_BASE)/mml.lar
# bin
mkdir -p $(SCRATCH_BASE)/bin
for binary in $(MIZBINARIES); do \
$(INSTALL) --mode 755 $(MIZBIN)/$$binary $(SCRATCH_BASE)/bin/$$binary; \
done
# data
for rootfile in $(MIZROOTFILES); do \
cp -p $(MIZFILES)/$$rootfile $(SCRATCH_BASE); \
done
head -n $(NUM_ARTICLES) $(MIZFILES)/mml.lar > $(SCRATCH_BASE)/mml.lar
# xsl
mkdir -p $(SCRATCH_BASE)/xsl
for sheet in $(SHEETS); do \
$(INSTALL) --mode 644 $(XSL4MIZ)/$$sheet.xsl $(SCRATCH_BASE)/xsl; \
done
# perl
mkdir -p $(SCRATCH_BASE)/.perl
for perlfile in $(PERLMODULES); do \
$(INSTALL) --mode 644 $$perlfile.pm $(SCRATCH_BASE)/.perl; \
done
for perlfile in $(PERLSCRIPTS); do \
$(INSTALL) --mode 755 $$perlfile.pl $(SCRATCH_BASE)/.perl; \
done
# makefiles
$(INSTALL) --mode 644 Makefile.repo $(SCRATCH_BASE)/Makefile
$(INSTALL) --mode 644 Makefile-depsrepo $(SCRATCH_BASE)/mml/Makefile
scratch-deps: scratch-mizfiles
touch $(SCRATCH_BASE)/mml/hidden-prel # everything depends on hidden-prel
@$(MAKE) -C $(SCRATCH_BASE)/mml -j $(MAKEJOBS) evls deps MIZFILES=$(SCRATCH_BASE) PATH=$(SCRATCH_BASE)/bin:$(PATH)
scratch-html: scratch-deps
@$(MAKE) -C $(SCRATCH_BASE) -j $(MAKEJOBS) xmlvrfs prels absrefs htmls MIZFILES=$(SCRATCH_BASE) PATH=$(SCRATCH_BASE)/bin:$(PATH)
scratch: scratch-html
public-repo-init: public-mwiki-user scratch
mkdir -p $(PUBLIC_REPO)
cp -R $(SCRATCH_BASE)/* $(PUBLIC_REPO)
cp -R $(SCRATCH_BASE)/.perl $(PUBLIC_REPO)
chown $(PUBLIC_MWIKI_USER) $(PUBLIC_REPO)
chgrp $(PUBLIC_MWIKI_USER) $(PUBLIC_REPO)
cd $(PUBLIC_REPO) && git init
$(INSTALL) \
--mode 644 \
--owner=$(PUBLIC_MWIKI_USER) --group=$(PUBLIC_MWIKI_USER) \
gitignore-public $(PUBLIC_REPO)/.gitignore
$(INSTALL) \
--mode 644 \
--owner=$(PUBLIC_MWIKI_USER) --group=$(PUBLIC_MWIKI_USER) \
public-repo-description $(PUBLIC_REPO)/.git/description
cd $(PUBLIC_REPO) && git add . && git commit -m 'Initial commit.'
$(INSTALL) \
--mode 755 \
--owner=$(PUBLIC_MWIKI_USER) \
--group=$(PUBLIC_MWIKI_USER) \
pre-commit post-commit $(PUBLIC_REPO)/.git/hooks
devel-repo-init: devel-mwiki-user scratch
mkdir -p $(DEVEL_REPO)
cp -R $(SCRATCH_BASE)/* $(DEVEL_REPO)
cp -R $(SCRATCH_BASE)/.perl $(DEVEL_REPO)
chown $(DEVEL_MWIKI_USER) $(DEVEL_REPO)
chgrp $(DEVEL_MWIKI_USER) $(DEVEL_REPO)
cd $(DEVEL_REPO) && git init
$(INSTALL) \
--mode 644 \
--owner=$(DEVEL_MWIKI_USER) --group=$(DEVEL_MWIKI_USER) \
gitignore-devel $(DEVEL_REPO)/.gitignore
$(INSTALL) \
--mode 644 \
--owner=$(DEVEL_MWIKI_USER) --group=$(DEVEL_MWIKI_USER) \
devel-repo-description $(DEVEL_REPO)/.git/description
cd $(DEVEL_REPO) && git add . && git commit -m 'Initial commit.'
$(INSTALL) \
--mode 755 \
--owner=$(DEVEL_MWIKI_USER) --group=$(DEVEL_MWIKI_USER) \
pre-commit post-commit $(DEVEL_REPO)/.git/hooks
public-mwiki-user:
-adduser --shell=/usr/bin/git-shell \
--home=$(PUBLIC_REPOS_BASE) \
--disabled-password \
$(PUBLIC_MWIKI_USER) \
|| echo "$(PUBLIC_MWIKI_USER) already exists"
-git daemon \
--syslog \
--base-path=$(PUBLIC_REPOS_BASE) \
--user=$(PUBLIC_MWIKI_USER) \
--detach
devel-mwiki-user:
-adduser --shell=/usr/bin/git-shell \
--disabled-password \
--home=$(DEVEL_REPOS_BASE) \
$(DEVEL_MWIKI_USER) \
|| echo "$(DEVEL_MWIKI_USER) already exists"
public-compiled: scratch
rsync -a --del $(SCRATCH_BASE)/ $(PUBLIC_COMPILED_REPO)
# ===> ^ <===
# trailing slash -- see the rsync man page to learn why it's there
devel-compiled: scratch
rsync -a --del $(SCRATCH_BASE)/ $(DEVEL_COMPILED_REPO)
# ===> ^ <===
# trailing slash -- see the rsync man page to learn why it's there
public-sandbox: scratch # our dirty sandbox
rsync -a --del $(SCRATCH_BASE)/ $(PUBLIC_SANDBOX)
# ===> ^ <===
# trailing slash -- see the rsync man page to learn why it's there
devel-sandbox: scratch # our dirty sandbox
rsync -a --del $(SCRATCH_BASE)/ $(DEVEL_SANDBOX)
# ===> ^ <===
# trailing slash -- see the rsync man page to learn why it's there
public-repo-export: public-repo-init
git clone --bare $(PUBLIC_REPO) $(BARE_PUBLIC_REPO)
$(INSTALL) \
--mode=644 \
--owner=$(PUBLIC_MWIKI_USER) --group=$(PUBLIC_MWIKI_USER) \
public-repo-description $(BARE_PUBLIC_REPO)/description
sed -e "s|@@BACKEND@@|$(PUBLIC_REPO)|g" < pre-receive.in \
> $(BARE_PUBLIC_REPO)/hooks/pre-receive
chmod 755 $(BARE_PUBLIC_REPO)/hooks/pre-receive
chown $(PUBLIC_MWIKI_USER) $(BARE_PUBLIC_REPO)/hooks/pre-receive
chgrp $(PUBLIC_MWIKI_USER) $(BARE_PUBLIC_REPO)/hooks/pre-receive
touch $(BARE_PUBLIC_REPO)/git-daemon-export-ok
GIT_DIR=$(BARE_PUBLIC_REPO) git config --add daemon.receivepack true
devel-repo-export: devel-repo-init
git clone --bare $(DEVEL_REPO) $(BARE_DEVEL_REPO)
$(INSTALL) \
--mode=644 \
--owner=$(DEVEL_MWIKI_USER) --group=$(DEVEL_MWIKI_USER) \
devel-repo-description $(BARE_DEVEL_REPO)/description
sed -e "s|@@BACKEND@@|$(DEVEL_REPO)|g" < pre-receive.in \
> $(BARE_DEVEL_REPO)/hooks/pre-receive
chmod 755 $(BARE_DEVEL_REPO)/hooks/pre-receive
chown $(DEVEL_MWIKI_USER) $(BARE_DEVEL_REPO)/hooks/pre-receive
chgrp $(DEVEL_MWIKI_USER) $(BARE_DEVEL_REPO)/hooks/pre-receive
gitweb: public-repo-export devel-repo-export
ln -s $(BARE_PUBLIC_REPO) $(GITWEB_ROOT)/mwiki-public.git
ln -s $(BARE_DEVEL_REPO) $(GITWEB_ROOT)/mwiki-devel.git
$(INSTALL) -m 644 gitweb $(APACHE_ROOT)/etc/apache2/sites-available/gitweb
cd $(APACHE_ROOT)/etc/apache2/sites-enabled \
&& ln -s ../sites-available/gitweb gitweb
apache2ctl restart
mwiki: public-repos
$(INSTALL) -m 644 mwiki.apacheconf \
$(APACHE_ROOT)/etc/apache2/sites-available/mwiki
cd $(APACHE_ROOT)/etc/apache2/sites-enabled \
&& ln -s ../sites-available/mwiki mwiki
apache2ctl restart
clean:
rm -Rf $(REPOS_BASE)
rm -f $(GITWEB_ROOT)/mwiki-public.git
rm -f $(GITWEB_ROOT)/mwiki-devel.git
-killall git-daemon
deluser $(PUBLIC_MWIKI_USER) \
|| echo "user $(PUBLIC_MWIKI_USER) doesn't exist"
deluser $(DEVEL_MWIKI_USER) \
|| echo "user $(DEVEL_MWIKI_USER) doesn't exist"
rm -f $(APACHE_ROOT)/etc/apache2/sites-available/gitweb
rm -f $(APACHE_ROOT)/etc/apache2/sites-enabled/mwiki
rm -f $(APACHE_ROOT)/etc/apache2/sites-available/mwiki
rm -f $(APACHE_ROOT)/etc/apache2/sites-enabled/gitweb
rm -f $(APACHE_ROOT)/var/log/apache2/gitweb.error.log
rm -f $(APACHE_ROOT)/var/log/apache2/gitweb.access.log
apache2ctl restart