blob: 78318d59b7221579cc1d17de439500ac7b0323d0 (
plain)
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
|
# to be linked to makefile (lowercase - takes precedence over Makefile)
# in main directory
TOPDIR=.
BASEDIR=
SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel
default: noargument
# set the devel makefile
setup-devel:
@ln -sfv dev/Makefile.devel makefile
@(for i in $(SOURCEDIRS); do \
(cd $(TOPDIR)/$$i; ln -sfv ../dev/Makefile.dir Makefile) \
done)
clean-devel:
echo rm -f makefile .depend.devel
echo rm -f $(foreach dir,$(SOURCEDIRS), $(TOPDIR)/$(dir)/Makefile)
coqtop: bin/coqtop.byte
ln -sf bin/coqtop.byte coqtop
quick:
$(MAKE) states BEST=byte
include Makefile
include $(TOPDIR)/dev/Makefile.common
# this file is better described in dev/Makefile.dir
include .depend.devel
#if dev/Makefile.local exists, it is included
ifneq ($(wildcard $(TOPDIR)/dev/Makefile.local),)
include $(TOPDIR)/dev/Makefile.local
endif
#runs coqtop with all theories required
total:
ledit ./bin/coqtop.byte $(foreach th,$(THEORIESVO),-require $(notdir $(basename $(th))))
#runs coqtop storing using the history file
run: $(TOPDIR)/coqtop
ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop
|
