Makefile.in 31.8 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1
2
##########################################################################
#                                                                        #
3
#  Copyright (C) 2010-2011                                               #
4
5
6
#    François Bobot                                                      #
#    Jean-Christophe Filliâtre                                           #
#    Claude Marché                                                       #
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
7
#    Andrei Paskevich                                                    #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
8
9
10
#                                                                        #
#  This software is free software; you can redistribute it and/or        #
#  modify it under the terms of the GNU Library General Public           #
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
11
#  License version 2.1, with the special exception on linking            #
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
12
13
14
15
16
17
18
19
#  described in file LICENSE.                                            #
#                                                                        #
#  This software is distributed in the hope that it will be useful,      #
#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  #
#                                                                        #
##########################################################################

Andrei Paskevich's avatar
Andrei Paskevich committed
20
include Version
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
21

22
23
24
25
26
27
VERBOSEMAKE ?= @enable_verbose_make@

ifeq ($(VERBOSEMAKE),yes)
  QUIET =
else
  QUIET = yes
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
28
29
endif

30
# install the binaries
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
31
DESTDIR =
32

33
prefix	    = @prefix@
34
35
36
37
38
exec_prefix = @exec_prefix@
datarootdir = @datarootdir@

BINDIR  = $(DESTDIR)@bindir@
LIBDIR  = $(DESTDIR)@libdir@
39
DATADIR = $(DESTDIR)@datarootdir@
40
MANDIR  = $(DESTDIR)@mandir@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
41

Andrei Paskevich's avatar
Andrei Paskevich committed
42
# OS specific stuff
43
44
EXE   = @EXE@
STRIP = @STRIP@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45
46

# other variables
47
48
49
50
51
52
53
54
55
56
OCAMLC    = @OCAMLC@
OCAMLOPT  = @OCAMLOPT@
OCAMLDEP  = @OCAMLDEP@
OCAMLLEX  = @OCAMLLEX@
OCAMLYACC = @OCAMLYACC@
OCAMLDOC  = @OCAMLDOC@
OCAMLLIB  = @OCAMLLIB@
OCAMLBEST = @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@

57
58
CAMLP5O   = @CAMLP5O@

59
ifeq (@enable_menhirlib@,yes)
Andrei Paskevich's avatar
Andrei Paskevich committed
60
61
  MENHIR    = @MENHIR@ --table
  MENHIRINC = -I @MENHIRLIB@
62
63
  MENHIRLIB = menhirLib
else
Andrei Paskevich's avatar
Andrei Paskevich committed
64
  MENHIR    = @MENHIR@
65
66
67
68
  MENHIRINC =
  MENHIRLIB =
endif

69
70
RUBBER = @RUBBER@

71
#PSVIEWER  = @PSVIEWER@
Andrei Paskevich's avatar
Andrei Paskevich committed
72
#PDFVIEWER = @PDFVIEWER@
73

74
75
BFLAGS = -w Aer-29 -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Aer-29 -dtypes    -I src $(INCLUDES)
76

77
ifeq (@enable_profiling@,yes)
78
79
80
81
OFLAGS += -g -p
STRIP = true
endif

82
83
# external libraries common to all binaries

84
EXTOBJS =
François Bobot's avatar
META    
François Bobot committed
85
EXTLIBS = str unix nums @META_DYNLINK@
86
87
88

EXTCMA	= $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
89

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90
91
92
###############
# main target
###############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
93

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94
all: @OCAMLBEST@
Francois Bobot's avatar
Francois Bobot committed
95

96
97
98
99
ifeq (@enable_local@,yes)
all: install_local
endif

100
101
plugins: plugins.@OCAMLBEST@

102
.PHONY: byte opt clean depend all install install_local install_no_local
103
.PHONY: plugins plugins.byte plugins.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
104

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
105
#############
106
# Why library
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
107
#############
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
108

109
LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
110
111
	       src/parser/parser.mli src/parser/parser.ml \
	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
112
	       src/driver/driver_lexer.ml
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
113

François Bobot's avatar
François Bobot committed
114
LIB_UTIL = stdlib exn_printer debug pp loc print_tree \
115
	   cmdline hashweak hashcons util sysutil rc plugin
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
116

117
LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
118

119
LIB_PARSER = ptree denv typing parser lexer
120

121
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
122
	     whyconf autodetection
123

124
LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
Andrei Paskevich's avatar
Andrei Paskevich committed
125
		inlining split_goal \
126
		eliminate_definition eliminate_algebraic \
127
		eliminate_inductive eliminate_let eliminate_if \
128
129
		libencoding discriminate protect_enumeration \
		encoding encoding_select \
130
		encoding_decorate encoding_bridge encoding_twin \
François Bobot's avatar
François Bobot committed
131
		encoding_explicit encoding_guard encoding_sort \
132
		encoding_instantiate simplify_array filter_trigger \
133
134
		introduction abstraction close_epsilon lift_epsilon \
	        eval_match
135

136
LIB_PRINTER = print_real alt_ergo why3 smt smt2 coq tptp simplify gappa cvc3
137

138
139
140
141
142
143
LIBMODULES = src/config \
	      $(addprefix src/util/, $(LIB_UTIL)) \
	      $(addprefix src/core/, $(LIB_CORE)) \
	      $(addprefix src/parser/, $(LIB_PARSER)) \
	      $(addprefix src/driver/, $(LIB_DRIVER)) \
	      $(addprefix src/transform/, $(LIB_TRANSFORM)) \
144
	      $(addprefix src/printer/, $(LIB_PRINTER))
145

146
LIBDIRS = util core parser driver transform printer
147
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
MARCHE Claude's avatar
MARCHE Claude committed
148

149
ifeq (@enable_hypothesis_selection@,yes)
Andrei Paskevich's avatar
Andrei Paskevich committed
150
151
152
  LIB_TRANSFORM += hypothesis_selection
  INCLUDES += -I @OCAMLGRAPHLIB@
  EXTLIBS += graph
153
154
endif

155
156
157
158
LIBML  = $(addsuffix .ml,  $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
159

160
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
161
$(LIBCMX): OFLAGS += -for-pack Why
162

163
# build targets
164

165
166
byte: src/why.cma
opt:  src/why.cmxa
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
167

168
src/why.cma: src/why.cmo
169
170
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

171
src/why.cmxa: src/why.cmx
172
173
	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^

174
175
src/why.cmo: $(LIBCMO)
	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
176

177
178
179
180
src/why.cmx: $(LIBCMX)
	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

# depend target
181

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
182
183
include .depend.lib

Andrei Paskevich's avatar
Andrei Paskevich committed
184
.depend.lib: src/config.ml $(LIBGENERATED)
185
	$(OCAMLDEP) -slash -I src $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
186
187
188

depend: .depend.lib

189
190
# clean target

Andrei Paskevich's avatar
Andrei Paskevich committed
191
LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
192
193
LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
	   $(addsuffix /*.annot, $(LIBSDIRS)) \
194
195
	   $(addsuffix /*.output, $(LIBSDIRS)) \
	   $(addsuffix /*.automaton, $(LIBSDIRS)) \
196
197
198
199
200
201
	   $(addsuffix /*.o, $(LIBSDIRS)) \
	   $(addsuffix /*~, $(LIBSDIRS))

clean::
	rm -f $(LIBCLEAN) $(LIBGENERATED)
	rm -f src/why.cm[iox] src/why.[ao] src/why.cma src/why.cmxa
202
	rm -f .depend.lib
203

204
205
206
###############
# installation
###############
207

208
install_no_local::
209
	mkdir -p $(BINDIR)
210
	mkdir -p $(LIBDIR)/why3
211
	mkdir -p $(DATADIR)/why3/images
MARCHE Claude's avatar
MARCHE Claude committed
212
	mkdir -p $(DATADIR)/why3/emacs
213
	mkdir -p $(DATADIR)/why3/lang
MARCHE Claude's avatar
MARCHE Claude committed
214
215
	mkdir -p $(DATADIR)/why3/theories
	mkdir -p $(DATADIR)/why3/theories/transform
216
	mkdir -p $(DATADIR)/why3/modules
MARCHE Claude's avatar
MARCHE Claude committed
217
218
219
	mkdir -p $(DATADIR)/why3/drivers
	cp -f theories/*.why $(DATADIR)/why3/theories
	cp -f theories/transform/*.why $(DATADIR)/why3/theories/transform
220
	cp -f modules/*.mlw $(DATADIR)/why3/modules
MARCHE Claude's avatar
MARCHE Claude committed
221
	cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
222
223
	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
	cp -f share/images/*.png $(DATADIR)/why3/images
MARCHE Claude's avatar
MARCHE Claude committed
224
	cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el
225
226
	cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang

MARCHE Claude's avatar
MARCHE Claude committed
227
228
229
install_no_local_lib::
	mkdir -p $(OCAMLLIB)/why3
	cp -f src/why.cm* $(OCAMLLIB)/why3
230
	cp -f META $(OCAMLLIB)/why3
MARCHE Claude's avatar
MARCHE Claude committed
231
232
	if test -f src/why.a; then cp -f src/why.a $(OCAMLLIB)/why3; fi

233
234
235
236
237
ifeq (@enable_local@,yes)
install install-lib:
	@echo "Why is configured in local installation mode."
	@echo "To install Why, run ./configure --disable-local ; make ; make install"
else
238
install: install_no_local
MARCHE Claude's avatar
MARCHE Claude committed
239
install-lib: install_no_local_lib
240
241
endif

MARCHE Claude's avatar
MARCHE Claude committed
242
243
install-all: install install-lib

244

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
245
##################
246
# Why binary
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
247
248
##################

249
250
byte: bin/why3.byte
opt:  bin/why3.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
251

252
bin/why3.opt: src/why.cmxa src/main.cmx
Andrei Paskevich's avatar
Andrei Paskevich committed
253
254
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
255
256
	$(STRIP) $@

257
bin/why3.byte: src/why.cma src/main.cmo
Andrei Paskevich's avatar
Andrei Paskevich committed
258
259
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
260

261
262
263
bin/why3: bin/why3.@OCAMLBEST@
	ln -sf why3.@OCAMLBEST@ $@

264
265
src/main.cmo: src/why.cma
src/main.cmx: src/why.cmxa
266

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
267
clean::
Andrei Paskevich's avatar
Andrei Paskevich committed
268
	rm -f src/main.cm[iox] src/main.annot src/main.o
269
	rm -f bin/why3.byte bin/why3.opt bin/why3
270

271
install_no_local::
272
273
274
	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3

install_local: bin/why3
275

276
277
278
########
# Whyml
########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
279

280
281
PGM_FILES = pgm_ttree pgm_types pgm_pretty \
	    pgm_module pgm_wp pgm_env pgm_typing pgm_main
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
282

283
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
284

285
286
287
288
289
PGMML  = $(addsuffix .ml,  $(PGMMODULES))
PGMMLI = $(addsuffix .mli, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))

290
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
291
292

# build targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
293

294
295
byte: bin/why3ml.byte
opt:  bin/why3ml.opt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
296

297
bin/why3ml.opt: src/why.cmxa $(PGMCMX) src/main.cmx
298
299
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
300
301
	$(STRIP) $@

302
bin/why3ml.byte: src/why.cma $(PGMCMO) src/main.cmo
303
304
305
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

306
307
308
bin/why3ml: bin/why3ml.@OCAMLBEST@
	ln -sf why3ml.@OCAMLBEST@ $@

309
# depend and clean targets
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
310
311

include .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
312

313
.depend.programs:
314
	$(OCAMLDEP) -slash -I src -I src/programs $(PGMML) $(PGMMLI) > $@
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
315

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
316
317
318
depend: .depend.programs

clean::
319
320
	rm -f src/programs/*.cm[iox] src/programs/*.o
	rm -f src/programs/*.annot src/programs/*~
321
	rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
322
	rm -f .depend.programs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
323

324
325
# test target

326
327
%.gui: %.why bin/why3ide.opt
	bin/why3ide.opt $*.why
328

329
330
%: %.mlw bin/why3ml.opt
	bin/why3ml.opt $*.mlw
331

332
333
%: %.why bin/why3.opt
	bin/why3.opt $*.why
François Bobot's avatar
François Bobot committed
334

335
336
%.gui: %.mlw bin/why3ide.opt
	bin/why3ide.opt $*.mlw
337

338
339
340
%.type: %.mlw bin/why3ide.opt
	bin/why3ml.opt --type-only $*.mlw

341
install_no_local::
342
	cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml
343

344
install_local: bin/why3ml
345

346
347
348
349
##########
# gallery
##########

350
GALLERYPGMS = binary_search bresenham sf same_fringe relabel quicksort \
351
        power mergesort_list mac_carthy isqrt insertion_sort_list flag \
352
	distance muller fib_memo fibonacci \
353
354
        vstte10_aqueue vstte10_inverting vstte10_max_sum \
	vstte10_queens vstte10_search_list \
355
        vacid_0_sparse_array
356
357
358

.PHONY: gallery

359
360
361
362
363
364
365
gallery::
	@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
	@for f in $(GALLERYPGMS); do \
	  echo "exporting $$f"; \
	  mkdir -p $(GALLERYDIR)/$$f; \
	  cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \
	done
366

367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
########
# Config
########

CONFIG_FILES = whyconfig

CONFIGMODULES = $(addprefix src/config/, $(CONFIG_FILES))

CONFIGML  = $(addsuffix .ml,  $(CONFIGMODULES))
CONFIGMLI = $(addsuffix .mli, $(CONFIGMODULES))
CONFIGCMO = $(addsuffix .cmo, $(CONFIGMODULES))
CONFIGCMX = $(addsuffix .cmx, $(CONFIGMODULES))

$(CONFIGCMO) $(CONFIGCMX): INCLUDES += -I src/programs

# build targets

384
385
byte: bin/why3config.byte
opt:  bin/why3config.opt
386

387
bin/why3config.opt: src/why.cmxa $(CONFIGCMX)
388
389
390
391
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

392
bin/why3config.byte: src/why.cma $(CONFIGCMO)
393
394
395
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

396
397
398
bin/why3config: bin/why3config.@OCAMLBEST@
	ln -sf why3config.@OCAMLBEST@ $@

399
400
401
402
403
404
405
406
407
408
409
410
411
# depend and clean targets

include .depend.config

.depend.config: $(CONFIGGENERATED)
	$(OCAMLDEP) -slash -I src -I src/config $(CONFIGML) $(CONFIGMLI) > $@

depend: .depend.config

clean::
	rm -f src/config/*.cm[iox] src/config/*.o
	rm -f src/config/*.annot src/config/*~
	rm -f src/config/*.output src/config/*.automaton
412
	rm -f bin/why3config.byte bin/why3config.opt bin/why3config
413
414
415
	rm -f .why.conf
	rm -f .depend.config

416
417
local_config: bin/why3config.@OCAMLBEST@
	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
418
		--detect --conf_file why.conf
419

420
install_no_local::
421
	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config
422

423
install_local: bin/why3config
424

MARCHE Claude's avatar
MARCHE Claude committed
425
426
427
428
###############
# IDE
###############

429
430
ifeq (@enable_ide@,yes)

431
IDE_FILES = xml session gconfig newmain
MARCHE Claude's avatar
MARCHE Claude committed
432
433
434
435
436
437
438
439

IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))

IDEML  = $(addsuffix .ml,  $(IDEMODULES))
IDEMLI = $(addsuffix .mli, $(IDEMODULES))
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))

440
$(IDECMO) $(IDECMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
441

442
# build targets
MARCHE Claude's avatar
MARCHE Claude committed
443

444
445
byte: bin/why3ide.byte
opt:  bin/why3ide.opt
MARCHE Claude's avatar
MARCHE Claude committed
446

447
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
448
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
Andrei Paskevich's avatar
Andrei Paskevich committed
449
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
MARCHE Claude's avatar
MARCHE Claude committed
450

451
bin/why3ide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
MARCHE Claude's avatar
MARCHE Claude committed
452
	$(if $(QUIET), @echo 'Linking  $@' &&) \
453
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
MARCHE Claude's avatar
MARCHE Claude committed
454
455
	$(STRIP) $@

456
bin/why3ide.byte: src/why.cma $(PGMCMO) $(IDECMO)
MARCHE Claude's avatar
MARCHE Claude committed
457
	$(if $(QUIET),@echo 'Linking  $@' &&) \
458
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
MARCHE Claude's avatar
MARCHE Claude committed
459

460
461
462
bin/why3ide: bin/why3ide.@OCAMLBEST@
	ln -sf why3ide.@OCAMLBEST@ $@

MARCHE Claude's avatar
MARCHE Claude committed
463
464
465
466
# depend and clean targets

include .depend.ide

MARCHE Claude's avatar
MARCHE Claude committed
467
.depend.ide: src/ide/xml.ml
468
	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
MARCHE Claude's avatar
MARCHE Claude committed
469
470
471
472

depend: .depend.ide

clean::
473
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
474
475
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
476
	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
MARCHE Claude's avatar
MARCHE Claude committed
477
478
	rm -f .depend.ide

479
install_no_local::
480
481
482
	cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide

install_local: bin/why3ide
483

484
endif
MARCHE Claude's avatar
d    
MARCHE Claude committed
485

486

MARCHE Claude's avatar
MARCHE Claude committed
487
488
489
490
491
492
493
494
495
496
497
498
499
###############
# Replayer
###############

REPLAYER_FILES = xml session replay

REPLAYERMODULES = $(addprefix src/ide/, $(REPLAYER_FILES))

REPLAYERML  = $(addsuffix .ml,  $(REPLAYERMODULES))
REPLAYERMLI = $(addsuffix .mli, $(REPLAYERMODULES))
REPLAYERCMO = $(addsuffix .cmo, $(REPLAYERMODULES))
REPLAYERCMX = $(addsuffix .cmx, $(REPLAYERMODULES))

Andrei Paskevich's avatar
Andrei Paskevich committed
500
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
MARCHE Claude's avatar
MARCHE Claude committed
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528

# build targets

byte: bin/why3replayer.byte
opt:  bin/why3replayer.opt

bin/why3replayer.opt: src/why.cmxa $(PGMCMX) $(REPLAYERCMX)
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

bin/why3replayer.byte: src/why.cma $(PGMCMO) $(REPLAYERCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

bin/why3replayer: bin/why3replayer.@OCAMLBEST@
	ln -sf why3replayer.@OCAMLBEST@ $@

# depend and clean targets

include .depend.replayer

.depend.replayer: src/ide/xml.ml
	$(OCAMLDEP) -slash -I src -I src/ide $(REPLAYERML) $(REPLAYERMLI) > $@

depend: .depend.replayer

clean::
529
	rm -f src/ide/xml.ml
MARCHE Claude's avatar
MARCHE Claude committed
530
531
532
533
534
535
536
537
538
539
540
	rm -f src/ide/*.cm[iox] src/ide/*.o
	rm -f src/ide/*.annot src/ide/*~
	rm -f bin/why3replayer.byte bin/why3replayer.opt bin/why3replayer
	rm -f .depend.replayer

install_no_local::
	cp -f bin/why3replayer.@OCAMLBEST@ $(BINDIR)/why3replayer

install_local: bin/why3replayer


541
###############
542
# Bench
543
544
###############

545
546
ifeq (@enable_bench@,yes)

547
BENCH_FILES = bench benchrc benchdb whybench
548
549
550

BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES))

551
BENCHMODULES := src/ide/worker src/ide/db $(BENCHMODULES)
552
553
554
555
556
557

BENCHML  = $(addsuffix .ml,  $(BENCHMODULES))
BENCHMLI = $(addsuffix .mli, $(BENCHMODULES))
BENCHCMO = $(addsuffix .cmo, $(BENCHMODULES))
BENCHCMX = $(addsuffix .cmx, $(BENCHMODULES))

558
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I @SQLITE3LIB@
559
560
561

# build targets

562
563
byte: bin/why3bench.byte
opt:  bin/why3bench.opt
564

Andrei Paskevich's avatar
Andrei Paskevich committed
565
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I @SQLITE3LIB@
566
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3
567

568
bin/why3bench.opt: src/why.cmxa $(PGMCMX) $(BENCHCMX)
569
570
571
572
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

573
bin/why3bench.byte: src/why.cma  $(PGMCMO) $(BENCHCMO)
574
575
576
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

577
578
579
bin/why3bench: bin/why3bench.@OCAMLBEST@
	ln -sf why3bench.@OCAMLBEST@ $@

580
581
582
583
584
585
586
587
588
589
590
591
# depend and clean targets

include .depend.bench

.depend.bench:
	$(OCAMLDEP) -slash -I src -I src/bench -I src/ide $(BENCHML) $(BENCHMLI) > $@

depend: .depend.bench

clean::
	rm -f src/bench/*.cm[iox] src/bench/*.o
	rm -f src/bench/*.annot src/bench/*~
592
	rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
593
594
595
	rm -f .depend.bench

install_no_local::
596
597
598
	cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench

install_local: bin/why3bench
599

600
601
endif

602
603
604
##############
# Coq plugin
##############
605

606
ifeq (@enable_coq_support@,yes)
607

608
609
610
611
612
613
614
615
616
617
618
619
620
COQGENERATED = src/coq-plugin/g_whytac.ml

COQ_FILES = whytac g_whytac

COQMODULES = $(addprefix src/coq-plugin/, $(COQ_FILES))

COQML  = $(addsuffix .ml,  $(COQMODULES))
COQCMO = $(addsuffix .cmo, $(COQMODULES))
COQCMX = $(addsuffix .cmx, $(COQMODULES))

COQTREES = kernel lib interp parsing proofs pretyping tactics library toplevel
COQINCLUDES = -I src/coq-plugin $(addprefix -I @COQLIB@/, $(COQTREES))

621
$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
622

623
624
byte: src/coq-plugin/whytac.cma
opt:  src/coq-plugin/whytac.cmxs
625

626
627
src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
628

629
src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
630
631
	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

632
src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
633
634
	$(OCAMLC) -a $(BFLAGS) -o $@ $^

635
636
637
638
src/coq-plugin/g_whytac.ml: src/coq-plugin/g_whytac.ml4
	$(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@

# depend and clean targets
Andrei Paskevich's avatar
Andrei Paskevich committed
639

640
641
642
643
644
645
646
647
648
649
650
651
652
653
include .depend.coq

.depend.coq: $(COQGENERATED)
	$(OCAMLDEP) -slash -I src -I src/coq-plugin $(COQML) > $@

depend: .depend.coq

clean::
	rm -f src/coq-plugin/*.cm[iox] src/coq-plugin/*.o
	rm -f src/coq-plugin/*.cma src/coq-plugin/*.cmxs
	rm -f src/coq-plugin/*.annot src/coq-plugin/*~
	rm -f $(COQGENERATED)
	rm -f .depend.coq

654
endif
655

656
657
658
########
# Tptp2why
########
659

660
ifeq (@enable_whytptp@,yes)
661

662
663
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
664

François Bobot's avatar
François Bobot committed
665
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
666

667
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
668
669
670
671
672
673

TPTPML  = $(addsuffix .ml,  $(TPTPMODULES))
TPTPMLI = $(addsuffix .mli, $(TPTPMODULES))
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))

674
675
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
676
677
678

# build targets

François Bobot's avatar
François Bobot committed
679
plugins.byte byte: plugins/whytptp.cmo
680
plugins.opt  opt : plugins/whytptp.cmxs
681

François Bobot's avatar
François Bobot committed
682
683
plugins/whytptp.cmxs plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
plugins/whytptp.cmxs plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
684

685
plugins/whytptp.cmxs: $(TPTPCMX)
686
	$(if $(QUIET), @echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
687
	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
688

689
plugins/whytptp.cmo: $(TPTPCMO)
690
	$(if $(QUIET),@echo 'Linking  $@' &&) \
François Bobot's avatar
François Bobot committed
691
692
	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^

François Bobot's avatar
François Bobot committed
693
install_no_local::
694
	cp -f plugins/whytptp.cm* $(LIBDIR)/why3/
François Bobot's avatar
François Bobot committed
695

696
697
698
699
700
701
702
703
704
705
706
# depend and clean targets

include .depend.tptp2why

.depend.tptp2why: $(TPTPGENERATED)
	$(OCAMLDEP) -slash -I src -I src/tptp2why $(TPTPML) $(TPTPMLI) > $@

depend: .depend.tptp2why

clean::
	rm -f $(TPTPGENERATED)
707
	rm -f src/tptp2why/*.cm* src/tptp2why/*.o
708
	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
709
	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
710
	rm -f plugins/whytptp.cm* plugins/whytptp.o
711
712
	rm -f .depend.tptp2why

713
endif
714

715
716
717
718
#######
# tools
#######

719
TOOLS = bin/why3-cpulimit
720
721
722

byte opt: $(TOOLS)

MARCHE Claude's avatar
gappa    
MARCHE Claude committed
723
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
MARCHE Claude's avatar
MARCHE Claude committed
724
	$(CC) -Wall -o $@ $^
725
726

clean::
MARCHE Claude's avatar
gappa    
MARCHE Claude committed
727
	rm -f bin/why3-cpulimit src/tools/*~
728

729
install_no_local::
730
	cp -f bin/why3-cpulimit $(BINDIR)/why3-cpulimit
731

732
733
734
735
#########
# why3doc
#########

736
737
# WHY3DOC_FILES = doc_html doc_main
WHY3DOC_FILES = to_html
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761

WHY3DOCMODULES = $(addprefix src/why3doc/, $(WHY3DOC_FILES))

WHY3DOCML  = $(addsuffix .ml,  $(WHY3DOCMODULES))
WHY3DOCMLI = $(addsuffix .mli, $(WHY3DOCMODULES))
WHY3DOCCMO = $(addsuffix .cmo, $(WHY3DOCMODULES))
WHY3DOCCMX = $(addsuffix .cmx, $(WHY3DOCMODULES))

$(WHY3DOCCMO) $(WHY3DOCCMX): INCLUDES += -I src/why3doc

# build targets

byte: bin/why3doc.byte
opt:  bin/why3doc.opt

bin/why3doc.opt: src/why.cmxa $(WHY3DOCCMX)
	$(if $(QUIET), @echo 'Linking  $@' &&) \
	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
	$(STRIP) $@

bin/why3doc.byte: src/why.cma $(WHY3DOCCMO)
	$(if $(QUIET),@echo 'Linking  $@' &&) \
	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^

762
763
764
bin/why3doc: bin/why3doc.@OCAMLBEST@
	ln -sf why3doc.@OCAMLBEST@ $@

765
766
767
install_no_local::
	cp -f bin/why3doc.@OCAMLBEST@ $(BINDIR)/why3doc

768
769
# depend and clean targets

770
771
WHY3DOCGENERATED=src/why3doc/to_html.ml

772
773
include .depend.why3doc

774
.depend.why3doc: $(WHY3DOCGENERATED)
775
776
777
778
779
	$(OCAMLDEP) -slash -I src -I src/why3doc $(WHY3DOCML) $(WHY3DOCMLI) > $@

depend: .depend.why3doc

clean::
780
	rm -f $(WHY3DOCGENERATED)
781
782
	rm -f src/why3doc/*.cm[iox] src/why3doc/*.o
	rm -f src/why3doc/*.annot src/why3doc/*~
783
	rm -f bin/why3doc.byte bin/why3doc.opt bin/why3doc
784
785
	rm -f .depend.why3doc

786
787
install_local: bin/why3doc

788
789
790
791
########
# bench
########

François Bobot's avatar
François Bobot committed
792
.PHONY: bench test comp_bench_plugins
793

794
795
bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
	$(MAKE) test-api
796
	sh bench/bench \
797
798
	    "bin/why3.@OCAMLBEST@" \
	    "bin/why3ml.@OCAMLBEST@"
799

800
BENCH_PLUGINS_CMO := helloworld.cmo
801
802
803
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)

François Bobot's avatar
François Bobot committed
804
805
806
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)

# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
807
# 	bin/why3.byte -D bench/plugins/helloworld.drv \
François Bobot's avatar
François Bobot committed
808
809
810
# 	tests/test-jcf.why -T Test -G G
# 	bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv  \
# 	tests/test-jcf.why -T Test -G G
811
812

###############
813
# test targets
814
###############
815

816
817
test2: bin/why3.byte $(TOOLS)
	bin/why3.byte tests/test-jcf.why
818

819
test: bin/why3.byte plugins.byte $(TOOLS)
820
	mkdir -p output_why3
821
822
823
824
825
	bin/why3.byte -D drivers/why3.drv -o output_why3 tests/test-jcf.why
	# bin/why3.byte -D drivers/alt_ergo.drv tests/test-jcf.why -T Test -G G
	# bin/why3.byte -P alt-ergo --timelimit 3 tests/test-jcf.why -T Test -G G
	# bin/why3.byte -D drivers/coq.drv tests/test-jcf.why -T Test -G G
	echo bin/why3.byte -P alt-ergo --timelimit 1 --prove theories/real.why
MARCHE Claude's avatar
MARCHE Claude committed
826
	@printf "*** Checking Coq file generation ***\\n"
827
	@mkdir -p output_coq
MARCHE Claude's avatar
MARCHE Claude committed
828
	@for i in int.Abs int.EuclideanDivision int.ComputerDivision  \
MARCHE Claude's avatar
MARCHE Claude committed
829
830
		real.Abs real.FromIntTest real.SquareTest \
		real.ExpLogTest real.PowerTest real.TrigonometryTest \
831
		floating_point.Test map.TestBv32 \
MARCHE Claude's avatar
MARCHE Claude committed
832
		; do \
833
	  printf "Generating Coq file for $$i\\n" && \
834
	  	bin/why3.byte -P coq -o output_coq -T $$i ; done
MARCHE Claude's avatar
MARCHE Claude committed
835
	@printf "*** Checking Coq compilation ***\\n"
836
	@for i in output_coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
837

838
839
840
testl: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte tests/test-pgm-jcf.mlw
	ocamlrun -bt bin/why3ml.byte -P alt-ergo tests/test-pgm-jcf.mlw
841

842
843
testl-debug: bin/why3ml.opt
	bin/why3ml.opt --debug program_typing tests/test-pgm-jcf.mlw
844

845
846
testl-ide: bin/why3ide.opt
	bin/why3ide.opt tests/test-pgm-jcf.mlw
847

848
849
testl-type: bin/why3ml.byte
	ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
850

MARCHE Claude's avatar
MARCHE Claude committed
851
test-api: src/why.cma
Andrei Paskevich's avatar
Andrei Paskevich committed
852
	ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why.cma examples/use_api.ml \
MARCHE Claude's avatar
MARCHE Claude committed
853
	|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
854

MARCHE Claude's avatar
MARCHE Claude committed
855
bts12244: src/why.cma
Andrei Paskevich's avatar
Andrei Paskevich committed
856
	ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why.cma examples/bts12244.ml
MARCHE Claude's avatar
MARCHE Claude committed
857

858
859

## Examples : Plugins ##
860

861
ifeq (@enable_plugins@,yes)
862

863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
PLUGDIR = examples/plugins/
PLUG_FILES = genequlin

PLUGMODULES = $(addprefix $(PLUGDIR), $(PLUG_FILES))

PLUGML  = $(addsuffix .ml,  $(PLUGMODULES))
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
PLUGCMXS = $(addsuffix .cmxs, $(PLUGMODULES))

# ifeq (@enable_plug_support@,yes)
# byte: src/plug-plugin/whytac.cma
# opt:  src/plug-plugin/whytac.cmxs
# endif

# $(PLUGCMO):  src/why.cma
# $(PLUGCMXS): src/why.cmxa

.PHONY: examples_plugins.byte examples_plugins.opt

examples_plugins.byte : $(PLUGCMO)
examples_plugins.opt : $(PLUGCMXS)

# depend and clean targets

include .depend.plug

.depend.plug: $(PLUGGENERATED)
	$(OCAMLDEP) -slash -I src -I $(PLUGDIR) $(PLUGML) | sed "s/cmx/cmxs/" > $@

depend: .depend.plug

clean::
	rm -f $(PLUGDIR)/*.cm[iox] $(PLUGDIR)/*.o
	rm -f $(PLUGDIR)/*.cma $(PLUGDIR)/*.cmxs
	rm -f $(PLUGDIR)/*.annot $(PLUGDIR)/*~
	rm -f $(PLUGGENERATED)
	rm -f .depend.plug
901

902
endif
903

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
904
905
906
################
# documentation
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
907

908
909
910
911
912
.PHONY: doc

ifeq (@enable_doc@,yes)

doc: doc/manual.pdf
MARCHE Claude's avatar
MARCHE Claude committed
913
# doc/manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
914

915
916
BNF = qualid constant operator term type formula theory why_file  \
      typev expr module whyml_file
917
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
MARCHE Claude's avatar
MARCHE Claude committed
918
919
920
921
922
923
924
925

doc/%_bnf.tex: doc/%.bnf doc/bnf
	doc/bnf $< > $@

doc/bnf: doc/bnf.mll
	$(OCAMLLEX) $<
	$(OCAMLOPT) -o $@ doc/bnf.ml

926
927
928
929
DOC = api glossary ide intro library macros manpages \
      manual starting syntax syntaxref version whyml

DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
930

931
doc/manual.pdf: $(BNFTEX) $(DOCTEX) doc/manual.bib
932
	cd doc; $(RUBBER) -d manual.tex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
933

934
935
# doc/manual.html: doc/manual.tex doc/version.tex
# 	$(MAKE) -C doc manual.html
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
936

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
937
clean::
938
939
940
941
942
943
944
	cd doc; $(RUBBER) -d --clean manual.tex

else

doc:

endif
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
945

946
##########
MARCHE Claude's avatar
API doc    
MARCHE Claude committed
947
# API DOC
948
##########
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
949

MARCHE Claude's avatar
API doc    
MARCHE Claude committed
950
951
.PHONY: apidoc

MARCHE Claude's avatar
MARCHE Claude committed
952
MODULESTODOC = util/util util/hashweak \
953
	core/ident core/ty core/term core/decl core/theory \
MARCHE Claude's avatar
MARCHE Claude committed
954
	core/env core/task \
955
956
	driver/whyconf driver/driver \
	ide/session
MARCHE Claude's avatar
MARCHE Claude committed
957
958
#	transform/introduction \
#	ide/db
MARCHE Claude's avatar
MARCHE Claude committed
959
960
961

FILESTODOC = $(addsuffix .mli, $(addprefix src/, $(MODULESTODOC)))

962
apidoc: $(FILESTODOC)
963
	mkdir -p doc/apidoc
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
964
	$(OCAMLDOC) -d doc/apidoc -html -keep-code $(INCLUDES) \
965
		$(LIBINCLUDES) -I src $(FILESTODOC)
966
# $(LIBML)
MARCHE Claude's avatar
MARCHE Claude committed
967

MARCHE Claude's avatar
MARCHE Claude committed
968
install_apidoc: apidoc
969
	rsync -av doc/apidoc/ marche@scm.gforge.inria.fr:/home/groups/why3/htdocs/apidoc/
MARCHE Claude's avatar
MARCHE Claude committed
970

MARCHE Claude's avatar
MARCHE Claude committed
971
doc/apidoc.tex: $(FILESTODOC)
MARCHE Claude's avatar
MARCHE Claude committed
972
	$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
973
		$(LIBINCLUDES) -I src $(FILESTODOC)
974
# $(LIBML)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
975

976
clean::
977
	rm -f doc/apidoc/*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
978

979
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
980
# generic rules
981
################
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
982

Andrei Paskevich's avatar