From 025f0b8a0da45679c084b33b48eadafedd9dc99b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 21 Sep 2024 21:44:31 -0700 Subject: [PATCH] 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 | 1 + Makefile | 4 +- Makefile.config | 12 +++++- Makefile.standalone | 98 +++++++++++++++++++++++++++++++-------------- 4 files changed, 80 insertions(+), 35 deletions(-) diff --git a/.gitignore b/.gitignore index 0447e9d30b..2727a856cd 100644 --- a/.gitignore +++ b/.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 diff --git a/Makefile b/Makefile index 8163b0367f..72a5f3ab79 100644 --- a/Makefile +++ b/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 diff --git a/Makefile.config b/Makefile.config index bed7f453ea..fcf1f5cbcb 100644 --- a/Makefile.config +++ b/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) diff --git a/Makefile.standalone b/Makefile.standalone index cfb4602ef2..5df3bfa4d8 100644 --- a/Makefile.standalone +++ b/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