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 \

.gitignore

@@ -239,6 +239,7 @@ fiat-html/wasm/fiat_crypto.wat
 fiat-html/wasm/fiat_crypto.wat.gz
 fiat-html/wasm/fiat_crypto.wasm
 fiat-html/wasm/fiat_crypto.wasm.map
+fiat-html/wasm/fiat_crypto.assets/
 fiat-html/version.js
 /Makefile.test-amd64-files.mk
 

Makefile

@@ -498,8 +498,8 @@ install-without-bedrock2: coq-without-bedrock2 $(filter %.vo,$(filter-out $(BEDR
 install-without-bedrock2:
 	$(HIDE)$(MAKE) -f Makefile.coq install FILESTOINSTALL="$(filter-out $(BEDROCK2_FILES_PATTERN),$(FILESTOINSTALL))"
 
-install-standalone-ocaml: standalone-ocaml
-install-standalone-haskell: standalone-haskell
+install-standalone-ocaml:: standalone-ocaml
+install-standalone-haskell:: standalone-haskell
 
 .PHONY: validate
 validate: Makefile.coq

Makefile.config

@@ -85,7 +85,11 @@ UNIFIED_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionHaskell/%)
 SEPARATE_HASKELL_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionHaskell/%)
 HASKELL_BINARIES := $(UNIFIED_HASKELL_BINARIES) $(SEPARATE_HASKELL_BINARIES)
 JS_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.map)
-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)
+WASM_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wat.gz)
+WASM_OF_OCAML_BASEDIR := src/ExtractionJsOfOCaml/
+WASM_OF_OCAML_EXTRA_FILES_WASM = $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wasm) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.assets/*.wasm)
+WASM_OF_OCAML_EXTRA_FILES_WASM_MAP = $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wasm.map) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.assets/*.wasm.map)
+WASM_OF_OCAML_EXTRA_FILES = $(WASM_OF_OCAML_EXTRA_FILES_WASM) $(WASM_OF_OCAML_EXTRA_FILES_WASM_MAP)
 
 WITH_BEDROCK2_UNIFIED_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/WithBedrock/%)
 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
 WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionHaskell/WithBedrock/%)
 WITH_BEDROCK2_HASKELL_BINARIES := $(WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES) $(WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES)
 WITH_BEDROCK2_JS_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.map)
-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)
+WITH_BEDROCK2_WASM_OF_OCAML := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.wat.gz)
+WITH_BEDROCK2_WASM_OF_OCAML_BASEDIR := src/ExtractionJsOfOCaml/WithBedrock/
+WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES_WASM = $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.wasm) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.assets/*.wasm)
+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)
+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

@@ -114,62 +114,98 @@ standalone-separate-haskell: $(SEPARATE_STANDALONE_HASKELL:%=src/ExtractionHaske
 standalone-js-of-ocaml: $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.js)
 standalone-wasm-of-ocaml: $(STANDALONE_WASM_OF_OCAML:%=src/ExtractionJsOfOCaml/%.wasm) $(STANDALONE_WASM_OF_OCAML:%=src/ExtractionJsOfOCaml/%.wat.gz)
 
-uninstall-standalone-ocaml: FILESTOINSTALL=$(OCAML_BINARIES)
-uninstall-standalone-unified-ocaml: FILESTOINSTALL=$(UNIFIED_OCAML_BINARIES)
-uninstall-standalone-separate-ocaml: FILESTOINSTALL=$(SEPARATE_OCAML_BINARIES)
-uninstall-standalone-haskell: FILESTOINSTALL=$(HASKELL_BINARIES)
-uninstall-standalone-unified-haskell: FILESTOINSTALL=$(UNIFIED_HASKELL_BINARIES)
-uninstall-standalone-separate-haskell: FILESTOINSTALL=$(SEPARATE_HASKELL_BINARIES)
-uninstall-standalone-js-of-ocaml: FILESTOINSTALL=$(JS_OF_OCAML_FILES)
-uninstall-standalone-wasm-of-ocaml: FILESTOINSTALL=$(WASM_OF_OCAML_FILES)
+uninstall-standalone-ocaml:: FILESTOINSTALL=$(OCAML_BINARIES)
+uninstall-standalone-unified-ocaml:: FILESTOINSTALL=$(UNIFIED_OCAML_BINARIES)
+uninstall-standalone-separate-ocaml:: FILESTOINSTALL=$(SEPARATE_OCAML_BINARIES)
+uninstall-standalone-haskell:: FILESTOINSTALL=$(HASKELL_BINARIES)
+uninstall-standalone-unified-haskell:: FILESTOINSTALL=$(UNIFIED_HASKELL_BINARIES)
+uninstall-standalone-separate-haskell:: FILESTOINSTALL=$(SEPARATE_HASKELL_BINARIES)
+uninstall-standalone-js-of-ocaml:: FILESTOINSTALL=$(JS_OF_OCAML_FILES)
+uninstall-standalone-wasm-of-ocaml:: FILESTOINSTALL=$(WASM_OF_OCAML_FILES)
+uninstall-standalone-wasm-of-ocaml: EXTRAFILESTOINSTALL=$(WASM_OF_OCAML_EXTRA_FILES)
+uninstall-standalone-wasm-of-ocaml:: EXTRAFILESBASEDIR=$(WASM_OF_OCAML_BASEDIR)
 
-install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell: PERMS=0755
-install-standalone-js-of-ocaml install-standalone-wasm-of-ocaml: PERMS=0644
-install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell: INSTALLDIR=$(BINDIR)
-install-standalone-js-of-ocaml: INSTALLDIR=$(JSDIR)
-install-standalone-wasm-of-ocaml: INSTALLDIR=$(WASMDIR)
+install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell:: PERMS=0755
+install-standalone-js-of-ocaml install-standalone-wasm-of-ocaml:: PERMS=0644
+install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell:: INSTALLDIR=$(BINDIR)
+install-standalone-js-of-ocaml:: INSTALLDIR=$(JSDIR)
+install-standalone-wasm-of-ocaml:: INSTALLDIR=$(WASMDIR)
 
 
 
 ifeq ($(SKIP_BEDROCK2),1)
-install-standalone-ocaml: FILESTOINSTALL=$(OCAML_BINARIES)
-install-standalone-unified-ocaml: FILESTOINSTALL=$(UNIFIED_OCAML_BINARIES)
-install-standalone-separate-ocaml: FILESTOINSTALL=$(SEPARATE_OCAML_BINARIES)
-install-standalone-haskell: FILESTOINSTALL=$(HASKELL_BINARIES)
-install-standalone-unified-haskell: FILESTOINSTALL=$(UNIFIED_HASKELL_BINARIES)
-install-standalone-separate-haskell: FILESTOINSTALL=$(SEPARATE_HASKELL_BINARIES)
-install-standalone-js-of-ocaml: FILESTOINSTALL=$(JS_OF_OCAML_FILES)
-install-standalone-wasm-of-ocaml: FILESTOINSTALL=$(WASM_OF_OCAML_FILES)
+install-standalone-ocaml:: FILESTOINSTALL=$(OCAML_BINARIES)
+install-standalone-unified-ocaml:: FILESTOINSTALL=$(UNIFIED_OCAML_BINARIES)
+install-standalone-separate-ocaml:: FILESTOINSTALL=$(SEPARATE_OCAML_BINARIES)
+install-standalone-haskell:: FILESTOINSTALL=$(HASKELL_BINARIES)
+install-standalone-unified-haskell:: FILESTOINSTALL=$(UNIFIED_HASKELL_BINARIES)
+install-standalone-separate-haskell:: FILESTOINSTALL=$(SEPARATE_HASKELL_BINARIES)
+install-standalone-js-of-ocaml:: FILESTOINSTALL=$(JS_OF_OCAML_FILES)
+install-standalone-wasm-of-ocaml:: FILESTOINSTALL=$(WASM_OF_OCAML_FILES)
+install-standalone-wasm-of-ocaml:: EXTRAFILESTOINSTALL1=$(WASM_OF_OCAML_EXTRA_FILES_WASM)
+install-standalone-wasm-of-ocaml:: EXTRAFILESTOINSTALL2=$(WASM_OF_OCAML_EXTRA_FILES_WASM_MAP)
+install-standalone-wasm-of-ocaml:: EXTRAFILESTOINSTALL=$(WASM_OF_OCAML_EXTRA_FILES)
+install-standalone-wasm-of-ocaml:: EXTRAFILESBASEDIR=$(WASM_OF_OCAML_BASEDIR)
 
 else
-install-standalone-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_OCAML_BINARIES)
-install-standalone-unified-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_UNIFIED_OCAML_BINARIES)
-install-standalone-separate-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_SEPARATE_OCAML_BINARIES)
-install-standalone-haskell: FILESTOINSTALL=$(WITH_BEDROCK2_HASKELL_BINARIES)
-install-standalone-unified-haskell: FILESTOINSTALL=$(WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES)
-install-standalone-separate-haskell: FILESTOINSTALL=$(WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES)
-install-standalone-js-of-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_JS_OF_OCAML_FILES)
-install-standalone-wasm-of-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_WASM_OF_OCAML_FILES)
+install-standalone-ocaml:: FILESTOINSTALL=$(WITH_BEDROCK2_OCAML_BINARIES)
+install-standalone-unified-ocaml:: FILESTOINSTALL=$(WITH_BEDROCK2_UNIFIED_OCAML_BINARIES)
+install-standalone-separate-ocaml:: FILESTOINSTALL=$(WITH_BEDROCK2_SEPARATE_OCAML_BINARIES)
+install-standalone-haskell:: FILESTOINSTALL=$(WITH_BEDROCK2_HASKELL_BINARIES)
+install-standalone-unified-haskell:: FILESTOINSTALL=$(WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES)
+install-standalone-separate-haskell:: FILESTOINSTALL=$(WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES)
+install-standalone-js-of-ocaml:: FILESTOINSTALL=$(WITH_BEDROCK2_JS_OF_OCAML_FILES)
+install-standalone-wasm-of-ocaml:: FILESTOINSTALL=$(WITH_BEDROCK2_WASM_OF_OCAML_FILES)
+install-standalone-wasm-of-ocaml:: EXTRAFILESTOINSTALL1=$(WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES_WASM)
+install-standalone-wasm-of-ocaml:: EXTRAFILESTOINSTALL2=$(WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES_WASM_MAP)
+install-standalone-wasm-of-ocaml:: EXTRAFILESTOINSTALL=$(WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES)
+install-standalone-wasm-of-ocaml:: EXTRAFILESBASEDIR=$(WITH_BEDROCK2_WASM_OF_OCAML_BASEDIR)
 
 endif
 
-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:
+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::
 	$(HIDE)code=0; for f in $(FILESTOINSTALL); do\
 	 if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
 	done; exit $$code
+
+install-standalone-wasm-of-ocaml::
+	$(HIDE)code=0; if [ -z "$(strip $(wildcard $(EXTRAFILESTOINSTALL1)))" ]; then \
+	  >&2 echo "Missing $(EXTRAFILESTOINSTALL1)"; code=1; \
+	fi; \
+	if [ -z "$(strip $(wildcard $(EXTRAFILESTOINSTALL2)))" ]; then \
+	  >&2 echo "Missing $(EXTRAFILESTOINSTALL2)"; code=1; \
+	fi; \
+	exit $$code
+
+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::
 	$(HIDE)for f in $(FILESTOINSTALL); do\
 	   install -d "$(INSTALLDIR)/" &&\
 	   install -m $(PERMS) "$$f" "$(INSTALLDIR)/" &&\
 	   echo INSTALL "$$f" "$(INSTALLDIR)/";\
 	done
 
-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:
+install-standalone-wasm-of-ocaml::
+	$(HIDE)for f in $(patsubst $(EXTRAFILESBASEDIR)%,%,$(wildcard $(EXTRAFILESTOINSTALL))); do\
+	  fdir="$$(dirname "$$f")" &&\
+	  fname="$$(basename "$$f")" &&\
+	  install -d "$(INSTALLDIR)/$$fdir" &&\
+	  install -m $(PERMS) "$(EXTRAFILESBASEDIR)$$f" "$(INSTALLDIR)/$$fdir/" &&\
+	  echo INSTALL "$(EXTRAFILESBASEDIR)$$f" "$(INSTALLDIR)/$$fdir/";\
+	done
+
+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::
 	$(HIDE)for f in $(FILESTOINSTALL); do \
 	 instf="$(INSTALLDIR)/`basename $$f`" &&\
 	 rm -f "$$instf" &&\
 	 echo RM "$$instf"; \
 	done
 
+uninstall-standalone-wasm-of-ocaml::
+	$(HIDE)for f in $(wildcard $(patsubst $(EXTRAFILESBASEDIR)%,$(INSTALLDIR)/%,$(EXTRAFILESTOINSTALL))); do\
+	  rm -f "$$f" &&\
+	  echo RM "$$f"; \
+	done
+
 install-standalone: install-standalone-ocaml # install-standalone-haskell
 install-standalone-unified: install-standalone-unified-ocaml # install-standalone-unified-haskell
 install-standalone-separate: install-standalone-separate-ocaml # install-standalone-separate-haskell