Don't sed wasm files, instead use subfolders to ensure the binary nam…

…es are correct from the start (#1961)

.github/workflows/coq-docker.yml

@@ -366,7 +366,7 @@ jobs:
         name: ExtractionOCaml-${{ matrix.coq-version }}
         path: src/ExtractionOCaml
     - name: make binaries executable
-      run: git check-ignore src/ExtractionOCaml/* | grep -v '\.' | xargs chmod +x
+      run: git check-ignore src/ExtractionOCaml/* src/ExtractionOCaml/*/* | grep -v '\.' | xargs chmod +x
     - name: generated-files
       run: etc/ci/github-actions-make.sh --warnings -f Makefile.examples -j2 generated-files
       if: github.event_name == 'pull_request'
@@ -428,7 +428,7 @@ jobs:
         name: ExtractionOCaml-master
         path: src/ExtractionOCaml
     - name: make binaries executable
-      run: git check-ignore src/ExtractionOCaml/* | grep -v '\.' | xargs chmod +x
+      run: git check-ignore src/ExtractionOCaml/* src/ExtractionOCaml/*/* | grep -v '\.' | xargs chmod +x
     - name: only-test-amd64-files
       run: etc/ci/github-actions-make.sh -f Makefile.examples -j2 only-test-amd64-files SLOWEST_FIRST=1
       env:

.gitignore

@@ -171,17 +171,17 @@ src/ExtractionHaskell/bedrock2_solinas_reduction
 src/ExtractionHaskell/bedrock2_unsaturated_solinas
 src/ExtractionHaskell/bedrock2_word_by_word_montgomery
 src/ExtractionHaskell/fiat_crypto
-src/ExtractionHaskell/with_bedrock2_base_conversion
-src/ExtractionHaskell/with_bedrock2_dettman_multiplication
-src/ExtractionHaskell/with_bedrock2_fiat_crypto
-src/ExtractionHaskell/with_bedrock2_saturated_solinas
-src/ExtractionHaskell/with_bedrock2_solinas_reduction
-src/ExtractionHaskell/with_bedrock2_unsaturated_solinas
-src/ExtractionHaskell/with_bedrock2_word_by_word_montgomery
+src/ExtractionHaskell/WithBedrock/base_conversion
+src/ExtractionHaskell/WithBedrock/dettman_multiplication
+src/ExtractionHaskell/WithBedrock/fiat_crypto
+src/ExtractionHaskell/WithBedrock/saturated_solinas
+src/ExtractionHaskell/WithBedrock/solinas_reduction
+src/ExtractionHaskell/WithBedrock/unsaturated_solinas
+src/ExtractionHaskell/WithBedrock/word_by_word_montgomery
 src/ExtractionHaskell/*.hs
 src/ExtractionOCaml/bedrock2_fiat_crypto
 src/ExtractionOCaml/fiat_crypto
-src/ExtractionOCaml/with_bedrock2_fiat_crypto
+src/ExtractionOCaml/WithBedrock/fiat_crypto
 src/ExtractionOCaml/saturated_solinas
 src/ExtractionOCaml/dettman_multiplication
 src/ExtractionOCaml/unsaturated_solinas
@@ -194,23 +194,32 @@ src/ExtractionOCaml/bedrock2_unsaturated_solinas
 src/ExtractionOCaml/bedrock2_solinas_reduction
 src/ExtractionOCaml/bedrock2_word_by_word_montgomery
 src/ExtractionOCaml/bedrock2_base_conversion
-src/ExtractionOCaml/with_bedrock2_saturated_solinas
-src/ExtractionOCaml/with_bedrock2_dettman_multiplication
-src/ExtractionOCaml/with_bedrock2_unsaturated_solinas
-src/ExtractionOCaml/with_bedrock2_solinas_reduction
-src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery
-src/ExtractionOCaml/with_bedrock2_base_conversion
+src/ExtractionOCaml/WithBedrock/saturated_solinas
+src/ExtractionOCaml/WithBedrock/dettman_multiplication
+src/ExtractionOCaml/WithBedrock/unsaturated_solinas
+src/ExtractionOCaml/WithBedrock/solinas_reduction
+src/ExtractionOCaml/WithBedrock/word_by_word_montgomery
+src/ExtractionOCaml/WithBedrock/base_conversion
 src/ExtractionOCaml/perf_unsaturated_solinas
 src/ExtractionOCaml/perf_word_by_word_montgomery
 src/ExtractionOCaml/*.ml
 src/ExtractionOCaml/*.mli
+src/ExtractionOCaml/WithBedrock/*.ml
+src/ExtractionOCaml/WithBedrock/*.mli
 src/ExtractionJsOfOCaml/*.ml
 src/ExtractionJsOfOCaml/*.mli
 src/ExtractionJsOfOCaml/*.js
 src/ExtractionJsOfOCaml/*.map
 src/ExtractionJsOfOCaml/*.wasm
 src/ExtractionJsOfOCaml/*.wat
 src/ExtractionJsOfOCaml/*.wat.gz
+src/ExtractionJsOfOCaml/WithBedrock/*.ml
+src/ExtractionJsOfOCaml/WithBedrock/*.mli
+src/ExtractionJsOfOCaml/WithBedrock/*.js
+src/ExtractionJsOfOCaml/WithBedrock/*.map
+src/ExtractionJsOfOCaml/WithBedrock/*.wasm
+src/ExtractionJsOfOCaml/WithBedrock/*.wat
+src/ExtractionJsOfOCaml/WithBedrock/*.wat.gz
 src/Rewriter/PerfTesting/Specific/generated/*.v
 src/Rewriter/PerfTesting/Specific/generated/*.log
 src/Rewriter/PerfTesting/Specific/generated/*.sh
@@ -225,11 +234,11 @@ fiat-amd64/*.description
 fiat-amd64/*.invocation
 fiat-html/fiat_crypto.js
 fiat-html/fiat_crypto.map
-fiat-html/wasm_fiat_crypto.js
-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.js
+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/version.js
 /Makefile.test-amd64-files.mk
 

Makefile

@@ -73,9 +73,9 @@ BEDROCK2_FILES_PATTERN := \
 	src/ExtractionJsOfOCaml/bedrock2_% \
 	src/ExtractionOCaml/bedrock2_% \
 	src/ExtractionHaskell/bedrock2_% \
-	src/ExtractionJsOfOCaml/with_bedrock2_% \
-	src/ExtractionOCaml/with_bedrock2_% \
-	src/ExtractionHaskell/with_bedrock2_% \
+	src/ExtractionJsOfOCaml/WithBedrock/% \
+	src/ExtractionOCaml/WithBedrock/% \
+	src/ExtractionHaskell/WithBedrock/% \
 	src/Assembly/WithBedrock/% \
 	src/Bedrock/% # it's important to catch not just the .vo files, but also the .glob files, etc, because this is used to filter FILESTOINSTALL
 EXCLUDE_PATTERN :=

Makefile.config

@@ -7,7 +7,9 @@ SHOW := $(if $(VERBOSE),@true "",@echo "")
 HIDE := $(if $(VERBOSE),,@)
 
 BINDIR?=/usr/local/bin
-JSDIR?=fiat-html
+JSWASM_BASEDIR?=fiat-html
+JSDIR?=$(JSWASM_BASEDIR)
+WASMDIR?=$(JSWASM_BASEDIR)/wasm
 # or $(shell opam config var bin) ?
 
 MOD_NAME := Crypto
@@ -56,8 +58,8 @@ endif
 UNIFIED_BASE_STANDALONE := fiat_crypto
 SEPARATE_BASE_STANDALONE := unsaturated_solinas saturated_solinas dettman_multiplication word_by_word_montgomery base_conversion solinas_reduction
 BASE_STANDALONE := $(SEPARATE_BASE_STANDALONE) $(UNIFIED_STANDALONE)
-BEDROCK2_UNIFIED_STANDALONE := $(addprefix bedrock2_,$(UNIFIED_BASE_STANDALONE)) $(addprefix with_bedrock2_,$(UNIFIED_BASE_STANDALONE))
-BEDROCK2_SEPARATE_STANDALONE := $(addprefix bedrock2_,$(SEPARATE_BASE_STANDALONE)) $(addprefix with_bedrock2_,$(SEPARATE_BASE_STANDALONE))
+BEDROCK2_UNIFIED_STANDALONE := $(addprefix bedrock2_,$(UNIFIED_BASE_STANDALONE)) $(addprefix WithBedrock/,$(UNIFIED_BASE_STANDALONE))
+BEDROCK2_SEPARATE_STANDALONE := $(addprefix bedrock2_,$(SEPARATE_BASE_STANDALONE)) $(addprefix WithBedrock/,$(SEPARATE_BASE_STANDALONE))
 BEDROCK2_STANDALONE := $(BEDROCK2_UNIFIED_STANDALONE) $(BEDROCK2_SEPARATE_STANDALONE)
 UNIFIED_STANDALONE := $(UNIFIED_BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_UNIFIED_STANDALONE))
 SEPARATE_STANDALONE := $(SEPARATE_BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_SEPARATE_STANDALONE))
@@ -83,17 +85,13 @@ 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_TEXT_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wasm.map)
-WASM_OF_OCAML_BINARY_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wasm) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wat.gz)
-WASM_OF_OCAML_FILES := $(WASM_OF_OCAML_TEXT_FILES) $(WASM_OF_OCAML_BINARY_FILES)
+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)
 
-WITH_BEDROCK2_UNIFIED_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%)
-WITH_BEDROCK2_SEPARATE_OCAML_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%)
+WITH_BEDROCK2_UNIFIED_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/WithBedrock/%)
+WITH_BEDROCK2_SEPARATE_OCAML_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionOCaml/WithBedrock/%)
 WITH_BEDROCK2_OCAML_BINARIES := $(WITH_BEDROCK2_UNIFIED_OCAML_BINARIES) $(WITH_BEDROCK2_SEPARATE_OCAML_BINARIES)
-WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionHaskell/with_bedrock2_%)
-WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionHaskell/with_bedrock2_%)
+WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionHaskell/WithBedrock/%)
+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/with_bedrock2_%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/with_bedrock2_%.map)
-WITH_BEDROCK2_WASM_OF_OCAML_TEXT_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/with_bedrock2_%.js)
-WITH_BEDROCK2_WASM_OF_OCAML_BINARY_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/with_bedrock2_%.wasm) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/with_bedrock2_%.wat.gz)
-WITH_BEDROCK2_WASM_OF_OCAML_FILES := $(WITH_BEDROCK2_WASM_OF_OCAML_TEXT_FILES) $(WITH_BEDROCK2_WASM_OF_OCAML_BINARY_FILES)
+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)

Makefile.standalone

@@ -70,7 +70,7 @@ $(STANDALONE_OCAML:%=src/ExtractionOCaml/%.cmi) : %.cmi : %.ml
 $(STANDALONE_OCAML:%=src/ExtractionOCaml/%) : % : %.ml %.cmi
 	$(SHOW)'$(CAMLOPT_PERF_SHOW) $< -o $@'
 	$(HIDE)$(ENSURE_STACK_LIMIT); \
-	 $(TIMER) $(CAMLOPT_PERF) $(STANDALONE_CAMLFLAGS) -linkpkg -I src/ExtractionOCaml/ -o $@ $<
+	 $(TIMER) $(CAMLOPT_PERF) $(STANDALONE_CAMLFLAGS) -linkpkg -I $(dir $@) -o $@ $<
 
 $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.cmi) : %.cmi : %.ml
 	$(SHOW)'OCAMLC $*.mli'
@@ -80,7 +80,7 @@ $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.cmi) : %.cmi : %.ml
 $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.byte) : %.byte : %.ml %.cmi
 	$(SHOW)'OCAMLC $< -o $@'
 	$(HIDE)$(ENSURE_STACK_LIMIT); \
-	 $(TIMER) $(OCAMLC) $(STANDALONE_JS_CAMLFLAGS) -linkpkg -I src/ExtractionJsOfOCaml/ -o $@ $<
+	 $(TIMER) $(OCAMLC) $(STANDALONE_JS_CAMLFLAGS) -linkpkg -I $(dir $@) -o $@ $<
 
 $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.js) : %.js : %.byte
 	$(SHOW)'JS_OF_OCAML $<'
@@ -127,7 +127,7 @@ install-standalone-ocaml install-standalone-unified-ocaml install-standalone-sep
 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=$(JSDIR)
+install-standalone-wasm-of-ocaml: INSTALLDIR=$(WASMDIR)
 
 
 
@@ -141,15 +141,6 @@ 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 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
-	$(HIDE)for f in $(FILESTOINSTALL); do\
-	   install -d "$(INSTALLDIR)/" &&\
-	   install -m $(PERMS) "$$f" "$(INSTALLDIR)/" &&\
-	   echo INSTALL "$$f" "$(INSTALLDIR)/";\
-	done
 else
 install-standalone-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_OCAML_BINARIES)
 install-standalone-unified-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_UNIFIED_OCAML_BINARIES)
@@ -158,58 +149,19 @@ 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_TEXT_FILES)
-install-standalone-wasm-of-ocaml: BINARYFILESTOINSTALL=$(WITH_BEDROCK2_WASM_OF_OCAML_BINARY_FILES)
+install-standalone-wasm-of-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_WASM_OF_OCAML_FILES)
 
-install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell:
-	$(HIDE)code=0; for f in $(FILESTOINSTALL); do\
-	 if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
-	done; exit $$code
-	$(HIDE)for f in $(FILESTOINSTALL); do\
-	   fdir="$$(dirname "$$f")" &&\
-	   fname="$$(basename "$$f")" &&\
-	   df="$${fname#with_bedrock2_}" &&\
-	   install -d "$(INSTALLDIR)/" &&\
-	   install -m $(PERMS) "$$f" "$(INSTALLDIR)/$$df" &&\
-	   echo INSTALL "$$f" "$(INSTALLDIR)/$$df";\
-	done
-install-standalone-js-of-ocaml:
+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:
 	$(HIDE)code=0; for f in $(FILESTOINSTALL); do\
 	 if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
 	done; exit $$code
 	$(HIDE)for f in $(FILESTOINSTALL); do\
-	   fdir="$$(dirname "$$f")" &&\
-	   fname="$$(basename "$$f")" &&\
-	   df="$${fname#with_bedrock2_}" &&\
-	   install -d "$(INSTALLDIR)/" &&\
-	   install -m $(PERMS) "$$f" "$(INSTALLDIR)/$$df" &&\
-	   sed -i.bak -e 's,\(sourceMappingURL=.*\)with_bedrock2_,\1,g; s,\("file":[^"]*"[^"]*\)with_bedrock2_,\1,g' "$(INSTALLDIR)/$$df" &&\
-	   rm -f "$(INSTALLDIR)/$$df.bak" &&\
-	   echo 'INSTALL+SED' "$$f" "$(INSTALLDIR)/$$df";\
-	done
-install-standalone-wasm-of-ocaml:
-	$(HIDE)code=0; for f in $(FILESTOINSTALL) $(BINARYFILESTOINSTALL); do\
-	 if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
-	done; exit $$code
-	$(HIDE)for f in $(FILESTOINSTALL); do\
-	   fdir="$$(dirname "$$f")" &&\
-	   fname="$$(basename "$$f")" &&\
-	   df="wasm_$${fname#with_bedrock2_}" &&\
-	   install -d "$(INSTALLDIR)/" &&\
-	   install -m $(PERMS) "$$f" "$(INSTALLDIR)/$$df" &&\
-	   sed -i.bak -e 's,with_bedrock2_,wasm_,g' "$(INSTALLDIR)/$$df" &&\
-	   rm -f "$(INSTALLDIR)/$$df.bak" &&\
-	   echo 'INSTALL+SED' "$$f" "$(INSTALLDIR)/$$df";\
-	done
-	$(HIDE)for f in $(BINARYFILESTOINSTALL); do\
-	   fdir="$$(dirname "$$f")" &&\
-	   fname="$$(basename "$$f")" &&\
-	   df="wasm_$${fname#with_bedrock2_}" &&\
 	   install -d "$(INSTALLDIR)/" &&\
-	   install -m $(PERMS) "$$f" "$(INSTALLDIR)/$$df" &&\
-	   echo 'INSTALL' "$$f" "$(INSTALLDIR)/$$df";\
+	   install -m $(PERMS) "$$f" "$(INSTALLDIR)/" &&\
+	   echo INSTALL "$$f" "$(INSTALLDIR)/";\
 	done
-endif
 
 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 \

fiat-html/wasm_fiat_crypto_worker.js

@@ -1,4 +1,4 @@
-self.importScripts("wasm_fiat_crypto.js");
+self.importScripts("wasm/fiat_crypto.js");
 let pending = [];
 self.onmessage = function (e) { pending.push(e); };
 setTimeout(function () {

src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v → src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v

@@ -1,4 +1,4 @@
 Require Import Crypto.Bedrock.Standalone.StandaloneJsOfOCamlMain.
 Import Bedrock2Later.
 
-Extraction "src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.tmp" FiatCrypto.main.
+Extraction "src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.tmp" FiatCrypto.main.

src/ExtractionOCaml/WithBedrock/base_conversion.v

@@ -0,0 +1,4 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2Later.
+
+Extraction "src/ExtractionOCaml/WithBedrock/base_conversion.tmp" BaseConversion.main.

src/ExtractionOCaml/WithBedrock/dettman_multiplication.v

@@ -0,0 +1,4 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2Later.
+
+Extraction "src/ExtractionOCaml/WithBedrock/dettman_multiplication.tmp" DettmanMultiplication.main.

src/ExtractionOCaml/with_bedrock2_fiat_crypto.v → src/ExtractionOCaml/WithBedrock/fiat_crypto.v

@@ -1,4 +1,4 @@
 Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
 Import Bedrock2Later.
 
-Extraction "src/ExtractionOCaml/with_bedrock2_fiat_crypto.tmp" FiatCrypto.main.
+Extraction "src/ExtractionOCaml/WithBedrock/fiat_crypto.tmp" FiatCrypto.main.

src/ExtractionOCaml/WithBedrock/saturated_solinas.v

@@ -0,0 +1,4 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2Later.
+
+Extraction "src/ExtractionOCaml/WithBedrock/saturated_solinas.tmp" SaturatedSolinas.main.

src/ExtractionOCaml/WithBedrock/solinas_reduction.v

@@ -0,0 +1,4 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2Later.
+
+Extraction "src/ExtractionOCaml/WithBedrock/solinas_reduction.tmp" SaturatedSolinas.main.

src/ExtractionOCaml/WithBedrock/unsaturated_solinas.v

@@ -0,0 +1,4 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2Later.
+
+Extraction "src/ExtractionOCaml/WithBedrock/unsaturated_solinas.tmp" UnsaturatedSolinas.main.

src/ExtractionOCaml/WithBedrock/word_by_word_montgomery.v

@@ -0,0 +1,4 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2Later.
+
+Extraction "src/ExtractionOCaml/WithBedrock/word_by_word_montgomery.tmp" WordByWordMontgomery.main.