Makefile 2.64 KB
Newer Older
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
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
# Copyright Raphaël Cauderlier (2014)

# <raphael.cauderlier@inria.fr>

# This software is a computer program whose purpose is to translate object-oriented program written in the simply-typed ς-calculus from Abadi and Cardelli to Dedukti and Coq.

# This software is governed by the CeCILL-B license under French law and
# abiding by the rules of distribution of free software.  You can use,
# modify and/ or redistribute the software under the terms of the CeCILL-B
# license as circulated by CEA, CNRS and INRIA at the following URL
# "http://www.cecill.info".

# As a counterpart to the access to the source code and rights to copy,
# modify and redistribute granted by the license, users are provided
# only with a limited warranty and the software's author, the holder of
# the economic rights, and the successive licensors have only limited
# liability.

# In this respect, the user's attention is drawn to the risks associated
# with loading, using, modifying and/or developing or reproducing the
# software by the user in light of its specific status of free software,
# that may mean that it is complicated to manipulate, and that also
# therefore means that it is reserved for developers and experienced
# professionals having in-depth computer knowledge. Users are therefore
# encouraged to load and test the software's suitability as regards
# their requirements in conditions enabling the security of their
# systems and/or data to be ensured and, more generally, to use and
# operate it in the same conditions as regards security.

# The fact that you are presently reading this means that you have had
# knowledge of the CeCILL-B license and that you accept its terms.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
32
33
34
35

DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)

36
37
38
39
40
41
42
# Change COMPILE_MODE to byte if you want bytecode
# instead of machine code
COMPILE_MODE = native

# The destination of the install target, without trailing slash
INSTALL_DIR = /usr/local/bin

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
43
.PHONY:	clean depend
44
.SUFFIXES: .dk .dko .ml .native .byte .v .vo
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
45

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
46
.dk.dko:
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
47
48
49
50
	dkcheck -e -nc $<

.v.vo:
	coqc $<
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
51

52
53
.ml.native:
	ocamlbuild -use-menhir $@
54
55
.ml.byte:
	ocamlbuild -use-menhir $@
56

57
all: $(DKOS) sigmaid
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
58
59
60

depend: .depend
.depend:
61
	dkdep pts.dk dk_*.dk > .depend
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
62
63

clean:
64
65
66
67
68
69
70
71
72
	rm -rf *.dko *.vo *.glob .depend tmp.dk \
            test.dk test.v \
	    sigmaid sigmaid.native sigmaid.byte _build

sigmaid: sigmaid.$(COMPILE_MODE)
	ln -s sigmaid.$(COMPILE_MODE) sigmaid

install: sigmaid
	install sigmaid $(INSTALL_DIR)/
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
73

74
75
test.dk: sigmaid.$(COMPILE_MODE)
	./sigmaid.$(COMPILE_MODE) test.sigma
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
76

77
78
test.v: sigmaid.$(COMPILE_MODE)
	./sigmaid.$(COMPILE_MODE) test.sigma
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
79

80
81
82
83
84
test.dko: test.dk dk_obj_examples.dko

test.vo: test.v coq_obj.vo

test: test.dko test.vo
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
85

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
86
-include .depend