ergo/Makefile at master · j4m3sb0mb/ergo · GitHub

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
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
# http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.
#

# User-level configuration
include Makefile.config
# Contains the list of all the Coq modules
include Makefile.coq_modules

#
CP=cp

FILES = $(addprefix mechanization/,$(MODULES:%=%.v))

## Compiler
all:
	@$(MAKE) MAKEFLAGS= ergo

# Setup
setup:
	@$(MAKE) npm-setup

# Regenerate the npm directory
ergo:
	@$(MAKE) ergo-mechanization
	@$(MAKE) MAKEFLAGS= ergo-extraction-refresh

ergo-mechanization: _CoqProject Makefile.coq
	@echo "[Ergo] "
	@echo "[Ergo] Compiling Coq Mechanization"
	@echo "[Ergo] "
	@$(MAKE) -f Makefile.coq

ergo-extraction:
	@echo "[Ergo] "
	@echo "[Ergo] Compiling the extracted OCaml"
	@echo "[Ergo] "
	@$(MAKE) -C extraction all

ergo-extraction-refresh:
	@echo "[Ergo] "
	@echo "[Ergo] Extracting mechanization to OCaml"
	@echo "[Ergo] "
	@$(MAKE) -C extraction all-refresh

npm-setup:
	@echo "[Ergo] "
	@echo "[Ergo] Setting up for Node.js build"
	@echo "[Ergo] "
	npm install

## Documentation
documentation:
	$(MAKE) -C mechanization documentation

## Testing
test:
	lerna run test

## Cleanup
clean-mechanization: Makefile.coq
	- @$(MAKE) -f Makefile.coq clean

cleanall-mechanization:
	- @$(MAKE) -f Makefile.coq cleanall
	- @rm -f Makefile.coq
	- @rm -f Makefile.coq.conf
	- @rm -f _CoqProject
	- @find mechanization \( -name '*.vo' -or -name '*.v.d' -or -name '*.glob'  -or -name '*.aux' \) -print0 | xargs -0 rm -f

clean-extraction:
	- @$(MAKE) -C extraction clean

cleanall-extraction:
	- @$(MAKE) -C extraction cleanall

clean-npm:
	- @rm -f package-lock.json
	- @rm -rf dist

cleanall-npm: clean-npm
	- @node ./scripts/external/cleanExternalModels.js
	- @rm -f ergo*.tgz
	- @rm -rf node_modules
	- @rm -rf .nyc_output
	- @rm -rf coverage
	- @rm -rf log
	- @rm -f lerna-debug.log

clean: Makefile.coq
	- @$(MAKE) clean-npm
	- @$(MAKE) clean-extraction
	- @$(MAKE) -C packages/ergo-compiler clean
	- @$(MAKE) -C packages/ergo-engine clean
	- @$(MAKE) -C packages/ergo-cli clean

cleanall: Makefile.coq
	@echo "[Ergo] "
	@echo "[Ergo] Cleaning up"
	@echo "[Ergo] "
	- @$(MAKE) cleanall-npm
	- @$(MAKE) cleanall-extraction
	- @$(MAKE) cleanall-mechanization
	- @$(MAKE) -C packages/ergo-compiler cleanall
	- @$(MAKE) -C packages/ergo-engine cleanall
	- @$(MAKE) -C packages/ergo-cli cleanall

##
_CoqProject: Makefile.config
	@echo "[Ergo] "
	@echo "[Ergo] Setting up Coq"
	@echo "[Ergo] "
ifneq ($(QCERT),)
	(echo "-R mechanization ErgoSpec -R $(QCERT)/coq Qcert";) > _CoqProject
else
	(echo "-R mechanization ErgoSpec";) > _CoqProject
endif

Makefile.coq: _CoqProject Makefile $(FILES)
	coq_makefile -f _CoqProject $(FILES) -o Makefile.coq

.PHONY: all clean documentation npm ergo