File: Makefile.developers

package info (click to toggle)
alt-ergo 2.0.0-3
  • links: PTS, VCS
  • area: main
  • in suites: buster
  • size: 2,096 kB
  • sloc: ml: 28,606; makefile: 15; sh: 12
file content (180 lines) | stat: -rw-r--r-- 6,619 bytes parent folder | download | duplicates (2)
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
COMMIT_ID = $(shell git log -1 | grep commit | cut -d " " -f 2)

edit: 
	emacs lib/*/*ml* tools/text/*.ml* tools/gui/*.ml* parsers/*/*.ml* plugins/*/*.ml* &

# Modules Architecture
###############################################################################

poor-archi: .depend
	cat .depend | ocamldot | dot -Tpdf > poor-archi.pdf

rich-archi:opt gui
	ocamldoc.opt $(INCLUDES) -dot -dot-reduce -dot-include-all lib/util/*.ml lib/structures/*.ml lib/reasoners/*.ml lib/frontend/*.ml tools/text/*.ml tools/gui/*.ml \
        parsers/why/*.ml lib/util/*.mli lib/structures/*.mli lib/reasoners/*.mli lib/frontend/*.mli tools/text/*.mli tools/gui/*.mli parsers/why/*.mli -verbose
	grep -v "}" ocamldoc.out > archi.dot
	rm ocamldoc.out
	cat ../extra/subgraphs.dot >> archi.dot
	echo "}" >> archi.dot
	dot -Tpdf archi.dot > archi.pdf

archi:$(NAME).byte $(GUINAME).byte
	ocamldoc.opt $(INCLUDES) -dot -dot-reduce lib/util/*.ml lib/structures/*.ml lib/reasoners/*.ml lib/frontend/*.ml tools/text/*.ml tools/gui/*.ml \
        parsers/why/*.ml lib/util/*.mli lib/structures/*.mli lib/reasoners/*.mli lib/frontend/*.mli tools/text/*.mli tools/gui/*.mli parsers/why/*.mli -verbose
	grep -v "}" ocamldoc.out > archi.dot
	rm ocamldoc.out
	cat ../extra/subgraphs.dot >> archi.dot
	echo "}" >> archi.dot
	dot -Tpdf archi.dot > archi.pdf
	evince archi.pdf 2> /dev/null > /dev/null &

# try-alt-ergo
##########################################################################################

try-alt-ergo:
	make clean
	cp -rf ../alt-ergo ../try-alt-ergo/
	cp -rf ../try-alt-ergo/extra/Makefile ../try-alt-ergo/alt-ergo/
	cp -rf ../try-alt-ergo/extra/Makefile.js ../try-alt-ergo/alt-ergo/
	cp -rf ../try-alt-ergo/lib-num ../try-alt-ergo/alt-ergo/
	cp -rf ../try-alt-ergo/js ../try-alt-ergo/alt-ergo/
	cp -rf ../try-alt-ergo/extra/src__main__main_js.ml ../try-alt-ergo/alt-ergo/tools/javascript/main_js.ml
	cp -rf ../try-alt-ergo/extra/src__util__myUnix.ml ../try-alt-ergo/alt-ergo/lib/util/myUnix.ml
	cp -rf ../try-alt-ergo/extra/src__util__numbers.ml ../try-alt-ergo/alt-ergo/lib/util/numbers.ml
	cp -rf ../try-alt-ergo/extra/src__util__myZip.ml ../try-alt-ergo/alt-ergo/lib/util/myZip.ml
	make depend -C ../try-alt-ergo/alt-ergo
	make byte -C ../try-alt-ergo/alt-ergo
	make try -C ../try-alt-ergo/alt-ergo
	cp ../try-alt-ergo/alt-ergo/try-alt-ergo.js ../try-alt-ergo/html-interface/try-alt-ergo/alt-ergo.js
	firefox ../try-alt-ergo/html-interface/try.html


try-alt-ergo-mini:
	make clean
	cp -rf ../alt-ergo ../try-alt-ergo/
	cp -rf ../try-alt-ergo/extra/Makefile ../try-alt-ergo/alt-ergo/
	cp -rf ../try-alt-ergo/extra/Makefile.js ../try-alt-ergo/alt-ergo/
	cp -rf ../try-alt-ergo/lib-num ../try-alt-ergo/alt-ergo/
	cp -rf ../try-alt-ergo/js ../try-alt-ergo/alt-ergo/
	cp -rf ../try-alt-ergo/extra/src__main__main_js_mini.ml ../try-alt-ergo/alt-ergo/tools/javascript/main_js.ml
	cp -rf ../try-alt-ergo/extra/src__util__myUnix.ml ../try-alt-ergo/alt-ergo/lib/util/myUnix.ml
	cp -rf ../try-alt-ergo/extra/src__util__numbers.ml ../try-alt-ergo/alt-ergo/lib/util/numbers.ml
	cp -rf ../try-alt-ergo/extra/src__util__myZip.ml ../try-alt-ergo/alt-ergo/lib/util/myZip.ml
	make depend -C ../try-alt-ergo/alt-ergo
	make byte -C ../try-alt-ergo/alt-ergo
	make try -C ../try-alt-ergo/alt-ergo
	cp ../try-alt-ergo/alt-ergo/try-alt-ergo.js ../try-alt-ergo/html-interface/try-alt-ergo/alt-ergo-mini.js
	firefox ../try-alt-ergo/html-interface/try-mini.html


# TESTS
##########################################################################################

non-regression:$(OPT) satML fm-simplex
	cp alt-ergo.opt ../non-regression/alt-ergo.opt
	cd ../non-regression &&  ./non-regression.sh
	rm ../non-regression/alt-ergo.opt




# try to make all the targets
##########################################################################################

test-everything:
	make configure
	./configure --prefix=`pwd`/test-make-everything
	rm -rf `pwd`/test-make-everything
	mkdir `pwd`/test-make-everything
	make show-dest-dirs
	make depend
	make all
	make gui
	make alt-ergo.byte
	make opt
	make alt-ergo.opt
	make altgr-ergo.opt
	make byte
	make altgr-ergo.byte
	make satML
	make fm-simplex
	make satML-plugin.cma
	make fm-simplex-plugin.cma
	make satML-plugin.cmxs
	make fm-simplex-plugin.cmxs
	make non-regression
	make archi
	make META
	make install-opt
	make install
	make install-byte
	make install-satML
	make install-fm-simplex
	make install-gui
	make install-man
	make stripped-arch-binary
#	make try-alt-ergo
#	make public-release # also performs opam-public, which needs public-export



# headers
##############
headers:
	cd ../extra/headers &&  ./headers.sh



# STATIC
##########################################################################################

BIBBYTE_STATIC = zarith.cma nums.cma unix.cma str.cma zip.cma # = BIBBYTE minus dynlink.cma
BIBOPT_STATIC = $(BIBBYTE_STATIC:.cma=.cmxa)

hide-dynlink-in-wrapper-MyDynlink:
	sed -i 's/include Dynlink/include DummyDL/g' lib/util/myDynlink.ml

static: hide-dynlink-in-wrapper-MyDynlink depend $(MAINCMX)
	$(OCAMLOPT) -ccopt -static $(OFLAGS) -o $@ $(BIBOPT_STATIC) $(MAINCMX)
	sed -i 's/include DummyDL/include Dynlink/g' lib/util/myDynlink.ml
	strip $@
	mv static alt-ergo-static-$(VERSION)-$(ARCH)


# PUBLIC RELEASES
##########################################################################################
PUBLIC_VERSION=$(VERSION)
PUBLIC_RELEASE=alt-ergo-free-$(PUBLIC_VERSION)
PUBLIC_TARGZ=$(PUBLIC_RELEASE).tar.gz
FILES_DEST=../public-release/$(PUBLIC_RELEASE)/$(PUBLIC_RELEASE)

public-release: # test-everything
	rm -rf ../public-release
	mkdir -p $(FILES_DEST)
	cp configure $(FILES_DEST)
	git clean -dfx
	cp ../License.OCamlPro ../LGPL-License.txt ../Apache-License-2.0.txt $(FILES_DEST)/
	cp ../README.md ../LICENSE.md ../COPYING.md $(FILES_DEST)/
	cp configure.in Makefile.configurable.in Makefile.users Makefile Makefile.developers $(FILES_DEST)/
	cp INSTALL.md opam CHANGES $(FILES_DEST)/
	cp -rf lib tools parsers plugins preludes examples doc $(FILES_DEST)/
	#echo "let version=\"$(PUBLIC_VERSION)\"" >> $(FILES_DEST)/lib/util/version.ml
	echo "let release_commit = \"$(COMMIT_ID)\"" >> $(FILES_DEST)/lib/util/version.ml
	echo "let release_date = \""`LANG=en_US; date`"\"" >> $(FILES_DEST)/lib/util/version.ml
	cd $(FILES_DEST)/.. && tar cfz $(PUBLIC_TARGZ) $(PUBLIC_RELEASE)
	rm -rf $(FILES_DEST)
	autoconf && ./configure

# Targets that work only after the modification in Makefile.XX and/or Alt-Ergo
###############################################################################

bisect-report:
	bisect-report -dump - -html report bisect*.out