fix extraction of non-aarch64 targets

4 files changed, 11 insertions, 6 deletions

diff --git a/.gitignore b/.gitignore
index 1d6cad94..fa9b1c67 100644
--- a/.gitignore
+++ b/.gitignore
@@ -76,6 +76,7 @@
 /lib/Responsefile.ml
 /driver/Version.ml
 /driver/Compiler.v
+/extraction/extraction.v
 # Documentation
 /doc/coq2html
 /doc/coq2html.ml
diff --git a/Makefile b/Makefile
index 1289b364..616c808f 100644
--- a/Makefile
+++ b/Makefile
@@ -249,8 +249,8 @@ endif
 tools/compiler_expand: tools/compiler_expand.ml
 ifeq ($(OCAML_NATIVE_COMP),true)
 	ocamlopt -o $@ $+
-	ocamlc -o $@ $+
 else
+	ocamlc -o $@ $+
 endif
 
 tools/modorder: tools/modorder.ml
@@ -274,6 +274,11 @@ latexdoc:
 	@tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; }
 	@chmod a-w $*.v
 
+extraction/extraction.v: Makefile extraction/extraction.vexpand
+	cat extraction/extraction.vexpand > extraction/extraction.v
+	echo "$(EXTRA_EXTRACTION)" >> extraction/extraction.v
+	echo "." >> extraction/extraction.v
+
 driver/Compiler.v: driver/Compiler.vexpand tools/compiler_expand
 	tools/compiler_expand driver/Compiler.vexpand $@
 
@@ -354,10 +359,10 @@ clean:
 	rm -f $(patsubst %, %/*.vo*, $(DIRS))
 	rm -f $(patsubst %, %/.*.aux, $(DIRS))
 	rm -rf doc/html doc/*.glob
-	rm -f driver/Version.ml
+	rm -f driver/Version.ml driver/Compiler.v
 	rm -f compcert.ini compcert.config
-	rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr
-	rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o
+	rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr extraction/extraction.v
+	rm -f tools/ndfun tools/modorder tools/compiler_expand tools/*.cm? tools/*.o
 	rm -f $(GENERATED) .depend
 	rm -f .lia.cache
 	$(MAKE) -f Makefile.extr clean
diff --git a/configure b/configure
index 79ce89df..83d68ed6 100755
--- a/configure
+++ b/configure
@@ -824,6 +824,7 @@ BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList
     ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v
     # TODO: UPDATE THIS
     # DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v
+EXTRA_EXTRACTION=   Asmgen.Asmgen_expand.loadimm32 Asmgen.Asmgen_expand.addimm64 Asmgen.Asmgen_expand.storeptr
 EOF
 fi
 
diff --git a/extraction/extraction.v b/extraction/extraction.vexpand
index ffcebaaa..568b1b46 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.vexpand
@@ -248,5 +248,3 @@ Separate Extraction
    Parser.translation_unit_file
    Compopts.optim_postpass
    Archi.has_notrap_loads
-   Asmgen.Asmgen_expand.loadimm32 Asmgen.Asmgen_expand.addimm64
-   Asmgen.Asmgen_expand.storeptr.