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
|
#------------------------------------------------------------------------
#
# File : Makefile (top level make file for E and its libraries)
#
# Author: Stephan Schulz
#
# Top level make file. Check Makefile.vars for system-dependend tool
# selection and compilation options.
#
# Changes
#
# Created: Sun Jul 6 22:55:11 MET DST 1997
#
#------------------------------------------------------------------------
.PHONY: all depend remove_links clean cleandist default_config debug_config distrib fulldistrib top links tags rebuild install config remake documentation E man
include Makefile.vars
# Project specific variables
PROJECT = E
LIBS = BASICS INOUT TERMS ORDERINGS CLAUSES PROPOSITIONAL LEARN \
PCL2 HEURISTICS CONTROL
HEADERS = $(LIBS) EXTERNAL PROVER
CODE = $(LIBS) SIMPLE_APPS EXTERNAL PROVER
PARTS = $(CODE) DOC
all: E
# Generate dependencies
depend:
@for subdir in $(CODE); do\
cd $$subdir; touch Makefile.dependencies; $(MAKE) depend; cd ..;\
done;
# Remove all automatically generated files
remove_links:
@if [ -d include ]; then\
cd include; rm -f *.h;\
fi;
@if [ -d lib ]; then\
cd lib; rm -f *.a;\
fi;
clean: remove_links
@for subdir in $(PARTS); do\
cd $$subdir; touch Makefile.dependencies;$(MAKE) clean; cd ..;\
done;
cleandist: clean
@rm -f *~ */*~
default_config:
./configure
@cat Makefile.vars| \
gawk '/^NODEBUG/{print "NODEBUG = -DNDEBUG -DFAST_EXIT";next}/^MEMDEBUG/{print "MEMDEBUG = # -DCLB_MEMORY_DEBUG # -DCLB_MEMORY_DEBUG2";next}/^DEBUGGER/{print "DEBUGGER = # -g -ggdb";next}/^PROFFLAGS/{print "PROFFLAGS = # -pg";next}{print}' > __tmpmake__;mv __tmpmake__ Makefile.vars
debug_config:
@cat Makefile.vars| \
gawk '/^NODEBUG/{print "NODEBUG = # -DNDEBUG -DFAST_EXIT";next}/^MEMDEBUG/{print "MEMDEBUG = -DCLB_MEMORY_DEBUG # -DCLB_MEMORY_DEBUG2";next}{print}' > __tmpmake__;mv __tmpmake__ Makefile.vars
commit_id:
echo '#define ECOMMITID "'`git rev-parse HEAD`'"' > PROVER/e_gitcommit.h
# Build a distribution
distrib: default_config commit_id man documentation cleandist
@echo "Did you think about: "
@echo " - Changing the bibliographies to local version"
@echo " - increasing the dev version number and committing to git?"
@echo " ??? "
@echo "" > etc/NO_DISTRIB
@cd ..; find $(PROJECT) -name ".git" -print >> $(PROJECT)/etc/NO_DISTRIB;\
$(TAR) cfX - $(PROJECT)/etc/NO_DISTRIB $(PROJECT) |$(GZIP) - -c > $(PROJECT).tgz
# Include the GIT subdirecctories (and non-GPL files, of which there currently are none).
fulldistrib: man documentation cleandist default_config
@echo "Warning: You are building a full archive!"
@echo "Did you remember to increase the dev version number and commit to git?"
@cd ..; $(TAR) cf - $(PROJECT)|$(GZIP) - -c > $(PROJECT)_FULL.tgz
# Build StarExec package. This is not supposed to be super-portable
# StarExec runs all binaries from its local bin/, so we cheat
starexec:
echo $(STAREXECPATH)
rm -rf $(STAREXECPATH)
find . -name ".#*" -exec rm {} \;
make clean
./configure --bindir="." --enable-ho
make
./configure --prefix=$(STAREXECPATH) --enable-ho
make install
make clean
./configure --bindir="."
make
./configure --prefix=$(STAREXECPATH)
make install
cp etc/STAREXEC2.2/starexec_run* $(STAREXECPATH)/bin
$(eval E_VERSION=`$$(STAREXECPATH)/bin/eprover --version | cut -d' ' -f1-2| sed -e 's/ /-/'`)
cd $(STAREXECPATH); zip -r $(E_VERSION).zip bin man
# Make all library parts
top: E
# Create symbolic links
links: remove_links
@mkdir -p include
@cd include; find .. -not -path '../include/*' -name "[^.]*.h" -exec $(LN) {} \;
@mkdir -p lib
# @cd lib;find .. -not -path '../lib/*' -name "[^.]*.a" -exec $(LN) {} \;
@cd lib;\
for subdir in $(LIBS); do\
$(LN) ../$$subdir/$$subdir.a .;\
done;
tags:
etags-emacs `find . \( -name "*.[ch]" -or -name "*.py" \) -and \( -not -path "*include*" -and -not -name ".#*" \)`
#ctags-exuberant -e -R .
# etags */*.c */*.h
# cd PYTHON; make ptags
# Rebuilding from scratch
rebuild:
echo 'Rebuilding with debug options $(DEBUGFLAGS)'
$(MAKE) clean
$(MAKE) config
$(MAKE)
# Configure the whole package
config:
echo 'Configuring build system'
$(MAKE) links
$(MAKE) depend
# Configure and copy executables to the installation directory
install:
-sh -c 'mkdir -p $(EXECPATH)'
-sh -c 'development_tools/e_install PROVER/eprover $(EXECPATH)'
-sh -c 'development_tools/e_install PROVER/eprover-ho $(EXECPATH)'
-sh -c 'development_tools/e_install PROVER/epclextract $(EXECPATH)'
-sh -c 'development_tools/e_install PROVER/e_stratpar $(EXECPATH)'
-sh -c 'development_tools/e_install PROVER/eground $(EXECPATH)'
-sh -c 'development_tools/e_install PROVER/e_ltb_runner $(EXECPATH)'
-sh -c 'development_tools/e_install PROVER/e_deduction_server $(EXECPATH)'
-sh -c 'development_tools/e_install PROVER/e_axfilter $(EXECPATH)'
-sh -c 'development_tools/e_install PROVER/checkproof $(EXECPATH)'
-sh -c 'development_tools/e_install PROVER/ekb_create $(EXECPATH)'
-sh -c 'development_tools/e_install PROVER/ekb_delete $(EXECPATH)'
-sh -c 'development_tools/e_install PROVER/ekb_ginsert $(EXECPATH)'
-sh -c 'development_tools/e_install PROVER/ekb_insert $(EXECPATH)'
-sh -c 'mkdir -p $(MANPATH)'
-sh -c 'development_tools/e_install DOC/man/eprover.1 $(MANPATH)'
-sh -c 'development_tools/e_install DOC/man/epclextract.1 $(MANPATH)'
-sh -c 'development_tools/e_install DOC/man/e_stratpar.1 $(MANPATH)'
-sh -c 'development_tools/e_install DOC/man/eground.1 $(MANPATH)'
-sh -c 'development_tools/e_install DOC/man/e_ltb_runner.1 $(MANPATH)'
-sh -c 'development_tools/e_install DOC/man/e_deduction_server.1 $(MANPATH)'
-sh -c 'development_tools/e_install DOC/man/e_axfilter.1 $(MANPATH)'
-sh -c 'development_tools/e_install DOC/man/checkproof.1 $(MANPATH)'
-sh -c 'development_tools/e_install DOC/man/ekb_create.1 $(MANPATH)'
-sh -c 'development_tools/e_install DOC/man/ekb_delete.1 $(MANPATH)'
-sh -c 'development_tools/e_install DOC/man/ekb_ginsert.1 $(MANPATH)'
-sh -c 'development_tools/e_install DOC/man/ekb_insert.1 $(MANPATH)'
# Also remake documentation
remake: config rebuild documentation
README: README.md
grep -v '```' README.md > README
documentation: README
cd DOC; $(MAKE)
man: E
mkdir -p DOC/man
help2man -N -i DOC/bug_reporting PROVER/eprover > DOC/man/eprover.1
help2man -N -i DOC/bug_reporting PROVER/e_stratpar > DOC/man/e_stratpar.1
help2man -N -i DOC/bug_reporting PROVER/eground > DOC/man/eground.1
help2man -N -i DOC/bug_reporting PROVER/epclextract > DOC/man/epclextract.1
help2man -N -i DOC/bug_reporting PROVER/e_ltb_runner > DOC/man/e_ltb_runner.1
help2man -N -i DOC/bug_reporting PROVER/e_deduction_server > DOC/man/e_deduction_server.1
help2man -N -i DOC/bug_reporting PROVER/e_axfilter > DOC/man/e_axfilter.1
help2man -N -i DOC/bug_reporting PROVER/checkproof > DOC/man/checkproof.1
help2man -N -i DOC/bug_reporting PROVER/ekb_create > DOC/man/ekb_create.1
help2man -N -i DOC/bug_reporting PROVER/ekb_delete > DOC/man/ekb_delete.1
help2man -N -i DOC/bug_reporting PROVER/ekb_ginsert > DOC/man/ekb_ginsert.1
help2man -N -i DOC/bug_reporting PROVER/ekb_insert > DOC/man/ekb_insert.1
# Build the single libraries
E: links
@for subdir in $(CODE); do\
cd $$subdir; touch Makefile.dependencies; $(MAKE); cd ..;\
done;
J ?= 4
benchpress-quick:
@echo "run provers on example problems..."
benchpress run -j $(J) -c benchpress.sexp --task eprover-quick-test --progress
.PHONY: benchpress
|
