Skip to content

Commit 025f0b8

Browse files
JasonGrossJasonGross
authored
Add support for wasm files in assets subdirectory (#1966)
* Add support for wasm files in assets subdirectory This seems to be the change with the new wasm_of_ocaml. This commit should be backwards compatible with older wasm_of_ocaml. * fix missing \
1 parent 39bc427 commit 025f0b8

File tree

4 files changed

+80
-35
lines changed

4 files changed

+80
-35
lines changed

‎.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -239,6 +239,7 @@ fiat-html/wasm/fiat_crypto.wat
239239
fiat-html/wasm/fiat_crypto.wat.gz
240240
fiat-html/wasm/fiat_crypto.wasm
241241
fiat-html/wasm/fiat_crypto.wasm.map
242+
fiat-html/wasm/fiat_crypto.assets/
242243
fiat-html/version.js
243244
/Makefile.test-amd64-files.mk
244245

‎Makefile

+2-2
Original file line numberDiff line numberDiff line change
@@ -498,8 +498,8 @@ install-without-bedrock2: coq-without-bedrock2 $(filter %.vo,$(filter-out $(BEDR
498498
install-without-bedrock2:
499499
$(HIDE)$(MAKE) -f Makefile.coq install FILESTOINSTALL="$(filter-out $(BEDROCK2_FILES_PATTERN),$(FILESTOINSTALL))"
500500

501-
install-standalone-ocaml: standalone-ocaml
502-
install-standalone-haskell: standalone-haskell
501+
install-standalone-ocaml:: standalone-ocaml
502+
install-standalone-haskell:: standalone-haskell
503503

504504
.PHONY: validate
505505
validate: Makefile.coq

‎Makefile.config

+10-2
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,11 @@ UNIFIED_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionHaskell/%)
8585
SEPARATE_HASKELL_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionHaskell/%)
8686
HASKELL_BINARIES := $(UNIFIED_HASKELL_BINARIES) $(SEPARATE_HASKELL_BINARIES)
8787
JS_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.map)
88-
WASM_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wasm.map) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wasm) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wat.gz)
88+
WASM_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wat.gz)
89+
WASM_OF_OCAML_BASEDIR := src/ExtractionJsOfOCaml/
90+
WASM_OF_OCAML_EXTRA_FILES_WASM = $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wasm) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.assets/*.wasm)
91+
WASM_OF_OCAML_EXTRA_FILES_WASM_MAP = $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wasm.map) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.assets/*.wasm.map)
92+
WASM_OF_OCAML_EXTRA_FILES = $(WASM_OF_OCAML_EXTRA_FILES_WASM) $(WASM_OF_OCAML_EXTRA_FILES_WASM_MAP)
8993

9094
WITH_BEDROCK2_UNIFIED_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/WithBedrock/%)
9195
WITH_BEDROCK2_SEPARATE_OCAML_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionOCaml/WithBedrock/%)
@@ -94,4 +98,8 @@ WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/Extrac
9498
WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionHaskell/WithBedrock/%)
9599
WITH_BEDROCK2_HASKELL_BINARIES := $(WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES) $(WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES)
96100
WITH_BEDROCK2_JS_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.map)
97-
WITH_BEDROCK2_WASM_OF_OCAML := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.wasm) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.wat.gz)
101+
WITH_BEDROCK2_WASM_OF_OCAML := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.wat.gz)
102+
WITH_BEDROCK2_WASM_OF_OCAML_BASEDIR := src/ExtractionJsOfOCaml/WithBedrock/
103+
WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES_WASM = $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.wasm) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.assets/*.wasm)
104+
WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES_WASM_MAP = $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.wasm.map) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.assets/*.wasm.map)
105+
WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES = $(WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES_WASM) $(WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES_WASM_MAP)

‎Makefile.standalone

+67-31
Original file line numberDiff line numberDiff line change
@@ -114,62 +114,98 @@ standalone-separate-haskell: $(SEPARATE_STANDALONE_HASKELL:%=src/ExtractionHaske
114114
standalone-js-of-ocaml: $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.js)
115115
standalone-wasm-of-ocaml: $(STANDALONE_WASM_OF_OCAML:%=src/ExtractionJsOfOCaml/%.wasm) $(STANDALONE_WASM_OF_OCAML:%=src/ExtractionJsOfOCaml/%.wat.gz)
116116

117-
uninstall-standalone-ocaml: FILESTOINSTALL=$(OCAML_BINARIES)
118-
uninstall-standalone-unified-ocaml: FILESTOINSTALL=$(UNIFIED_OCAML_BINARIES)
119-
uninstall-standalone-separate-ocaml: FILESTOINSTALL=$(SEPARATE_OCAML_BINARIES)
120-
uninstall-standalone-haskell: FILESTOINSTALL=$(HASKELL_BINARIES)
121-
uninstall-standalone-unified-haskell: FILESTOINSTALL=$(UNIFIED_HASKELL_BINARIES)
122-
uninstall-standalone-separate-haskell: FILESTOINSTALL=$(SEPARATE_HASKELL_BINARIES)
123-
uninstall-standalone-js-of-ocaml: FILESTOINSTALL=$(JS_OF_OCAML_FILES)
124-
uninstall-standalone-wasm-of-ocaml: FILESTOINSTALL=$(WASM_OF_OCAML_FILES)
117+
uninstall-standalone-ocaml:: FILESTOINSTALL=$(OCAML_BINARIES)
118+
uninstall-standalone-unified-ocaml:: FILESTOINSTALL=$(UNIFIED_OCAML_BINARIES)
119+
uninstall-standalone-separate-ocaml:: FILESTOINSTALL=$(SEPARATE_OCAML_BINARIES)
120+
uninstall-standalone-haskell:: FILESTOINSTALL=$(HASKELL_BINARIES)
121+
uninstall-standalone-unified-haskell:: FILESTOINSTALL=$(UNIFIED_HASKELL_BINARIES)
122+
uninstall-standalone-separate-haskell:: FILESTOINSTALL=$(SEPARATE_HASKELL_BINARIES)
123+
uninstall-standalone-js-of-ocaml:: FILESTOINSTALL=$(JS_OF_OCAML_FILES)
124+
uninstall-standalone-wasm-of-ocaml:: FILESTOINSTALL=$(WASM_OF_OCAML_FILES)
125+
uninstall-standalone-wasm-of-ocaml: EXTRAFILESTOINSTALL=$(WASM_OF_OCAML_EXTRA_FILES)
126+
uninstall-standalone-wasm-of-ocaml:: EXTRAFILESBASEDIR=$(WASM_OF_OCAML_BASEDIR)
125127

126-
install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell: PERMS=0755
127-
install-standalone-js-of-ocaml install-standalone-wasm-of-ocaml: PERMS=0644
128-
install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell: INSTALLDIR=$(BINDIR)
129-
install-standalone-js-of-ocaml: INSTALLDIR=$(JSDIR)
130-
install-standalone-wasm-of-ocaml: INSTALLDIR=$(WASMDIR)
128+
install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell:: PERMS=0755
129+
install-standalone-js-of-ocaml install-standalone-wasm-of-ocaml:: PERMS=0644
130+
install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell:: INSTALLDIR=$(BINDIR)
131+
install-standalone-js-of-ocaml:: INSTALLDIR=$(JSDIR)
132+
install-standalone-wasm-of-ocaml:: INSTALLDIR=$(WASMDIR)
131133

132134

133135

134136
ifeq ($(SKIP_BEDROCK2),1)
135-
install-standalone-ocaml: FILESTOINSTALL=$(OCAML_BINARIES)
136-
install-standalone-unified-ocaml: FILESTOINSTALL=$(UNIFIED_OCAML_BINARIES)
137-
install-standalone-separate-ocaml: FILESTOINSTALL=$(SEPARATE_OCAML_BINARIES)
138-
install-standalone-haskell: FILESTOINSTALL=$(HASKELL_BINARIES)
139-
install-standalone-unified-haskell: FILESTOINSTALL=$(UNIFIED_HASKELL_BINARIES)
140-
install-standalone-separate-haskell: FILESTOINSTALL=$(SEPARATE_HASKELL_BINARIES)
141-
install-standalone-js-of-ocaml: FILESTOINSTALL=$(JS_OF_OCAML_FILES)
142-
install-standalone-wasm-of-ocaml: FILESTOINSTALL=$(WASM_OF_OCAML_FILES)
137+
install-standalone-ocaml:: FILESTOINSTALL=$(OCAML_BINARIES)
138+
install-standalone-unified-ocaml:: FILESTOINSTALL=$(UNIFIED_OCAML_BINARIES)
139+
install-standalone-separate-ocaml:: FILESTOINSTALL=$(SEPARATE_OCAML_BINARIES)
140+
install-standalone-haskell:: FILESTOINSTALL=$(HASKELL_BINARIES)
141+
install-standalone-unified-haskell:: FILESTOINSTALL=$(UNIFIED_HASKELL_BINARIES)
142+
install-standalone-separate-haskell:: FILESTOINSTALL=$(SEPARATE_HASKELL_BINARIES)
143+
install-standalone-js-of-ocaml:: FILESTOINSTALL=$(JS_OF_OCAML_FILES)
144+
install-standalone-wasm-of-ocaml:: FILESTOINSTALL=$(WASM_OF_OCAML_FILES)
145+
install-standalone-wasm-of-ocaml:: EXTRAFILESTOINSTALL1=$(WASM_OF_OCAML_EXTRA_FILES_WASM)
146+
install-standalone-wasm-of-ocaml:: EXTRAFILESTOINSTALL2=$(WASM_OF_OCAML_EXTRA_FILES_WASM_MAP)
147+
install-standalone-wasm-of-ocaml:: EXTRAFILESTOINSTALL=$(WASM_OF_OCAML_EXTRA_FILES)
148+
install-standalone-wasm-of-ocaml:: EXTRAFILESBASEDIR=$(WASM_OF_OCAML_BASEDIR)
143149

144150
else
145-
install-standalone-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_OCAML_BINARIES)
146-
install-standalone-unified-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_UNIFIED_OCAML_BINARIES)
147-
install-standalone-separate-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_SEPARATE_OCAML_BINARIES)
148-
install-standalone-haskell: FILESTOINSTALL=$(WITH_BEDROCK2_HASKELL_BINARIES)
149-
install-standalone-unified-haskell: FILESTOINSTALL=$(WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES)
150-
install-standalone-separate-haskell: FILESTOINSTALL=$(WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES)
151-
install-standalone-js-of-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_JS_OF_OCAML_FILES)
152-
install-standalone-wasm-of-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_WASM_OF_OCAML_FILES)
151+
install-standalone-ocaml:: FILESTOINSTALL=$(WITH_BEDROCK2_OCAML_BINARIES)
152+
install-standalone-unified-ocaml:: FILESTOINSTALL=$(WITH_BEDROCK2_UNIFIED_OCAML_BINARIES)
153+
install-standalone-separate-ocaml:: FILESTOINSTALL=$(WITH_BEDROCK2_SEPARATE_OCAML_BINARIES)
154+
install-standalone-haskell:: FILESTOINSTALL=$(WITH_BEDROCK2_HASKELL_BINARIES)
155+
install-standalone-unified-haskell:: FILESTOINSTALL=$(WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES)
156+
install-standalone-separate-haskell:: FILESTOINSTALL=$(WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES)
157+
install-standalone-js-of-ocaml:: FILESTOINSTALL=$(WITH_BEDROCK2_JS_OF_OCAML_FILES)
158+
install-standalone-wasm-of-ocaml:: FILESTOINSTALL=$(WITH_BEDROCK2_WASM_OF_OCAML_FILES)
159+
install-standalone-wasm-of-ocaml:: EXTRAFILESTOINSTALL1=$(WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES_WASM)
160+
install-standalone-wasm-of-ocaml:: EXTRAFILESTOINSTALL2=$(WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES_WASM_MAP)
161+
install-standalone-wasm-of-ocaml:: EXTRAFILESTOINSTALL=$(WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES)
162+
install-standalone-wasm-of-ocaml:: EXTRAFILESBASEDIR=$(WITH_BEDROCK2_WASM_OF_OCAML_BASEDIR)
153163

154164
endif
155165

156-
install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell install-standalone-js-of-ocaml install-standalone-wasm-of-ocaml:
166+
install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell install-standalone-js-of-ocaml install-standalone-wasm-of-ocaml::
157167
$(HIDE)code=0; for f in $(FILESTOINSTALL); do\
158168
if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
159169
done; exit $$code
170+
171+
install-standalone-wasm-of-ocaml::
172+
$(HIDE)code=0; if [ -z "$(strip $(wildcard $(EXTRAFILESTOINSTALL1)))" ]; then \
173+
>&2 echo "Missing $(EXTRAFILESTOINSTALL1)"; code=1; \
174+
fi; \
175+
if [ -z "$(strip $(wildcard $(EXTRAFILESTOINSTALL2)))" ]; then \
176+
>&2 echo "Missing $(EXTRAFILESTOINSTALL2)"; code=1; \
177+
fi; \
178+
exit $$code
179+
180+
install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell install-standalone-js-of-ocaml install-standalone-wasm-of-ocaml::
160181
$(HIDE)for f in $(FILESTOINSTALL); do\
161182
install -d "$(INSTALLDIR)/" &&\
162183
install -m $(PERMS) "$$f" "$(INSTALLDIR)/" &&\
163184
echo INSTALL "$$f" "$(INSTALLDIR)/";\
164185
done
165186

166-
uninstall-standalone-ocaml uninstall-standalone-unified-ocaml uninstall-standalone-separate-ocaml uninstall-standalone-haskell uninstall-standalone-unified-haskell uninstall-standalone-separate-haskell uninstall-standalone-wasm-of-ocaml uninstall-standalone-js-of-ocaml:
187+
install-standalone-wasm-of-ocaml::
188+
$(HIDE)for f in $(patsubst $(EXTRAFILESBASEDIR)%,%,$(wildcard $(EXTRAFILESTOINSTALL))); do\
189+
fdir="$$(dirname "$$f")" &&\
190+
fname="$$(basename "$$f")" &&\
191+
install -d "$(INSTALLDIR)/$$fdir" &&\
192+
install -m $(PERMS) "$(EXTRAFILESBASEDIR)$$f" "$(INSTALLDIR)/$$fdir/" &&\
193+
echo INSTALL "$(EXTRAFILESBASEDIR)$$f" "$(INSTALLDIR)/$$fdir/";\
194+
done
195+
196+
uninstall-standalone-ocaml uninstall-standalone-unified-ocaml uninstall-standalone-separate-ocaml uninstall-standalone-haskell uninstall-standalone-unified-haskell uninstall-standalone-separate-haskell uninstall-standalone-wasm-of-ocaml uninstall-standalone-js-of-ocaml::
167197
$(HIDE)for f in $(FILESTOINSTALL); do \
168198
instf="$(INSTALLDIR)/`basename $$f`" &&\
169199
rm -f "$$instf" &&\
170200
echo RM "$$instf"; \
171201
done
172202

203+
uninstall-standalone-wasm-of-ocaml::
204+
$(HIDE)for f in $(wildcard $(patsubst $(EXTRAFILESBASEDIR)%,$(INSTALLDIR)/%,$(EXTRAFILESTOINSTALL))); do\
205+
rm -f "$$f" &&\
206+
echo RM "$$f"; \
207+
done
208+
173209
install-standalone: install-standalone-ocaml # install-standalone-haskell
174210
install-standalone-unified: install-standalone-unified-ocaml # install-standalone-unified-haskell
175211
install-standalone-separate: install-standalone-separate-ocaml # install-standalone-separate-haskell

0 commit comments

Comments
 (0)