-
Notifications
You must be signed in to change notification settings - Fork 0
/
Makefile
167 lines (148 loc) · 5.14 KB
/
Makefile
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
# This Makefile is used to build and install GNATprove and its
# sub-components, at the exception of provers (CVC4, Z3, Alt-Ergo) which
# should be separately built/installed.
#
# To build gnat2why, you need:
# . a working GNAT compiler
# . a symbolic link in gnat2why/gnat_src that points to the GNAT sources
# . an installation of the gnatcoll library
#
# To build gnatprove, you need:
# . an installation of the gnatcoll library
# . local checked out repositories of submodules why3.
#
# The necessary steps to correctly install gnat2why/gnatprove are
#
# 1) make setup
#
# This does the local setup of submodule why3.
#
# 2) make
#
# This builds gnatprove, gnat2why, and why3.
#
# 3) make install-all
#
# This copies all the necessary files into the install/ subdirectory, for
# gnatprove, gnat2why, and why3.
#
# 4) export PATH=/path/to/spark2014/install/bin:$PATH
#
# This puts the directory install/bin in your path.
.PHONY: clean doc gnat2why gnat2why-nightly gnatprove install \
install-all why3 all setup all-nightly doc-nightly
INSTALLDIR=$(CURDIR)/install
SHAREDIR=$(INSTALLDIR)/share
INCLUDEDIR=$(INSTALLDIR)/include/spark
LIBDIR=$(INSTALLDIR)/lib/gnat
EXAMPLESDIR=$(SHAREDIR)/examples/spark
DOCDIR=$(SHAREDIR)/doc/spark
GNATPROVEDIR=$(SHAREDIR)/spark
CONFIGDIR=$(GNATPROVEDIR)/config
THEORIESDIR=$(GNATPROVEDIR)/theories
RUNTIMESDIR=$(GNATPROVEDIR)/runtimes
DOC=ug lrm
# Control if gnatprove is built in production or debug mode
PROD=-XBuild=Production
CP=cp -pr
MV=mv -f
GNATMAKE=gnatmake
VERSION=0.0w
# main target for developers
all: gnat2why gnatprove why3
# main target for nightly builds
all-nightly: gnat2why-nightly gnatprove-nightly install install-examples
# Setup and installation of why3
# ==============================
#
# We deal differently with submodules for why3 in a developer
# setting, who builds directly why3, and for nightly builds, where
# the builds of why3 and cvc4, z3, and alt-ergo are handled separately.
#
# Thus, special targets are defined for the developer only:
# setup why3
# install-all install of gnatprove and why3
setup:
cd why3 && ./configure --prefix=$(INSTALLDIR) \
--enable-relocation \
--enable-coq-tactic=no \
--disable-menhirLib
why3:
$(MAKE) -C why3
install-all:
$(MAKE) install
$(MAKE) -C why3 install_spark2014_dev
# Move internal binaries to libexec/spark/bin like the nighty build
# does (in anod scripts), as why3 executables expect this relative
# location to find the Why3 installation files in share. Do this for
# all internal binaries even if not strictly needed.
mkdir -p install/libexec/spark/bin
$(MV) install/bin/why3server install/libexec/spark/bin
$(MV) install/bin/why3realize install/libexec/spark/bin
$(MV) install/bin/gnatwhy3 install/libexec/spark/bin
$(MV) install/bin/gnat_server install/libexec/spark/bin
$(MV) install/bin/why3config install/libexec/spark/bin
$(MV) install/bin/why3session install/libexec/spark/bin
# the following line is allowed to fail - why3ide might not be
# installed
-$(MV) install/bin/why3ide install/libexec/spark/bin
# Create the fake prover scripts to help extract benchmarks.
$(CP) benchmark_script/fake_* install/libexec/spark/bin
install:
mkdir -p $(INSTALLDIR)/bin $(CONFIGDIR) $(THEORIESDIR) \
$(RUNTIMESDIR) $(INCLUDEDIR) $(LIBDIR)
@echo "Generate default target.atp in $(INSTALLDIR)/bin:"
$(GNATMAKE) -q -c -u -gnats spark2014vsn.ads \
-gnatet=$(INSTALLDIR)/bin/target.atp
$(CP) share/spark/help.txt $(GNATPROVEDIR)
$(CP) share/spark/config/* $(CONFIGDIR)
$(CP) share/spark/theories/*why $(THEORIESDIR)
$(CP) share/spark/theories/*mlw $(THEORIESDIR)
$(CP) share/spark/runtimes/README $(RUNTIMESDIR)
@echo "Generate Coq files by preprocessing context files:"
$(MAKE) -C include generate
$(CP) include/*.ad? $(INCLUDEDIR)
$(CP) include/*.gpr $(LIBDIR)
$(CP) include/proof $(LIBDIR)
doc: $(DOC)
doc-nightly: $(DOC)
cd docs/ug; $(MAKE) generate-nightly VERSION=$(VERSION)
$(DOC):
$(MAKE) -C docs/$@ latexpdf LATEXOPTS="-interaction=nonstopmode" VERSION=$(VERSION)
$(MAKE) -C docs/$@ html VERSION=$(VERSION)
mkdir -p $(DOCDIR)/pdf
mkdir -p $(DOCDIR)/html/$@
$(CP) docs/$@/_build/latex/*.pdf $(DOCDIR)/pdf
$(CP) docs/$@/_build/html/* $(DOCDIR)/html/$@
$(MAKE) -C docs/$@ clean
gnat2why-nightly:
$(MAKE) -C gnat2why AUTOMATED=1 GPRARGS=$(PROD)
gnat2why:
$(MAKE) -C gnat2why
coverage:
$(MAKE) -C gnat2why coverage
gnatprove:
$(MAKE) -C gnatprove build
gnatprove-nightly:
$(MAKE) -C gnatprove build PROD=$(PROD)
install-examples:
mkdir -p $(EXAMPLESDIR)
# install examples from the testsuite as identified in file
# MANIFEST.examples
for dir in `grep -v "^--" MANIFEST.examples` ; do \
$(CP) testsuite/gnatprove/tests/$$dir $(EXAMPLESDIR); \
done
find $(EXAMPLESDIR) -name test.py -exec rm -f {} \;
find $(EXAMPLESDIR) -name test.out -exec rm -f {} \;
# install examples in GNATprove-by-Example section of User's Guide
# a special example
$(CP) docs/ug/gnatprove_by_example/examples \
$(EXAMPLESDIR)/gnatprove_by_example
clean:
$(MAKE) -C gnat2why clean
$(MAKE) -C gnatprove clean
$(MAKE) -C docs/ug clean
$(MAKE) -C docs/lrm clean
$(MAKE) -C why3 clean
$(MAKE) -C include clean
rm -f docs/sphinx_support/confvars.py