From 1419ef6783d95371ee0107830c3d98505372a16b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 15 Feb 2024 14:33:44 +0100 Subject: [PATCH] Try fixing makefile --- bootstrap/certicoqc/Makefile | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/bootstrap/certicoqc/Makefile b/bootstrap/certicoqc/Makefile index bd131a3d..893534b8 100644 --- a/bootstrap/certicoqc/Makefile +++ b/bootstrap/certicoqc/Makefile @@ -78,16 +78,6 @@ g_certicoqc.ml: g_certicoqc.mlg certicoqc.cmx certicoqc_plugin_wrapper.cmx certicoqc.cmx: certicoqc_plugin_wrapper.cmx -%.o: %.c theories/compile.vo - $(CCOMPILER) $(CCOMPILEROPTS) -o $@ $< - -.PRECIOUS: %.cmi -%.cmi: %.mli - ocamlfind opt ${PKGS} ${OCAMLOPTS} -for-pack Certicoqc_plugin $< - -%.cmx: %.ml %.cmi - ocamlfind opt -c ${PKGS} ${OCAMLOPTS} -for-pack Certicoqc_plugin -o $@ $< - certicoqc_plugin.cmxs: certicoqc_plugin.cmxa ${CFILES:.c=.o} ${RUNTIME_FILES} ocamlfind ocamlopt ${OCAMLOPTS} -shared -o $@ $+ @@ -99,6 +89,17 @@ certicoqc_plugin.cmxa: certicoqc_plugin.cmx certicoqc_wrapper.c: theories/compile.vo +%.o: %.c theories/compile.vo + $(CCOMPILER) $(CCOMPILEROPTS) -o $@ $< + +.PRECIOUS: %.cmi +%.cmi: %.mli + ocamlfind opt ${PKGS} ${OCAMLOPTS} -for-pack Certicoqc_plugin $< + +%.cmx: %.ml %.cmi + ocamlfind opt -c ${PKGS} ${OCAMLOPTS} -for-pack Certicoqc_plugin -o $@ $< + + install: theories/compile.vo certicoqc_plugin.cmxs install -d "$(COQLIBINSTALL)" install -m 0644 theories/CertiCoqC.v theories/CertiCoqC.vo theories/compile.v theories/compile.vo certicoqc_plugin.cmx* "$(COQLIBINSTALL)"