From 0eefd517c797f2f17ef9228e5a4d07c5dc8ecada Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 7 Jul 2022 10:09:17 +0200 Subject: Check early that extraction did not run into unimplemented axioms This has been known to happen, e.g. when using Flocq 4.0. If we don't stop the build at this point, a `ccomp` executable is built that fails every time it is run. Closes: #438 --- Makefile | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Makefile b/Makefile index 2c849f42..b3b7a124 100644 --- a/Makefile +++ b/Makefile @@ -205,6 +205,11 @@ extraction: extraction/STAMP extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMachdep.v rm -f extraction/*.ml extraction/*.mli $(COQEXEC) extraction/extraction.v + @if grep 'AXIOM TO BE REALIZED' extraction/*.ml; then \ + echo "An error occured during extraction to OCaml code."; \ + echo "Check the versions of Flocq and MenhirLib used."; \ + exit 2; \ + fi touch extraction/STAMP .depend.extr: extraction/STAMP tools/modorder driver/Version.ml -- cgit