Commit 4ff1dd2a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Detect whether coqtop.byte is present.

It is needed for compiling the Coq tactic Why3.vo file when native
compilation is disabled.

This commit also avoid a potential race condition when Why3.vo was
compiled with both the native and bytecode compilers.
parent a2e998a1
......@@ -146,7 +146,6 @@ why3.conf
# Coq tactic
/src/coq-tactic/why3tac.ml
/src/coq-tactic/.why3-vo-*
# Coq
......
......@@ -831,8 +831,8 @@ $(COQPCMX): OFLAGS += -rectypes
$(COQPDEP): $(COQPGENERATED)
byte: src/coq-tactic/.why3-vo-byte
opt: src/coq-tactic/.why3-vo-opt
byte: lib/coq-tactic/why3tac.cma
opt: lib/coq-tactic/why3tac.cmxs
lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmxa, @ZIPLIB@)
lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmx, @MENHIRLIB@)
......@@ -847,24 +847,20 @@ src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
$(SHOW) 'Camlp $<'
$(HIDE)$(COQCAMLP) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
COQRTAC = -R lib/coq-tactic Why3 -R lib/coq Why3
COQRTAC = -R lib/coq-tactic Why3 -R lib/coq Why3 -I lib/coq-tactic
ifeq (@coq_compat_version@,COQ86)
COQRTAC += -I lib/coq-tactic
endif
ifeq (@coq_compat_version@,COQ87)
COQRTAC += -I lib/coq-tactic
ifeq "$(OCAMLBEST)" "opt"
COQTACEXT = cmxs
else
COQTACEXT = cma
COQRTAC += -byte
endif
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cma
lib/coq-tactic/Why3.vo: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.$(COQTACEXT)
$(SHOW) 'Coqc $<'
$(HIDE)WHY3CONFIG="" $(COQC) -byte $(COQRTAC) $< && \
touch src/coq-tactic/.why3-vo-byte
$(HIDE)WHY3CONFIG="" $(COQC) $(COQRTAC) $<
src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cmxs
$(SHOW) 'Coqc $<'
$(HIDE)WHY3CONFIG="" $(COQC) -opt $(COQRTAC) $< && \
touch src/coq-tactic/.why3-vo-opt
all: lib/coq-tactic/Why3.vo
# depend and clean targets
......@@ -880,7 +876,6 @@ GENERATED += $(COQPGENERATED)
clean::
rm -f lib/coq-tactic/*.vo lib/coq-tactic/*.glob
rm -f src/coq-tactic/.why3-vo-*
install_no_local::
$(MKDIR_P) $(LIBDIR)/why3/coq-tactic
......@@ -1615,7 +1610,7 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
bash bench/bench ".@OCAMLBEST@"
@if test "@enable_coq_tactic@" = "yes"; then \
echo "=== checking the Coq tactic ==="; \
$(MAKE) test-coq-tactic.@OCAMLBEST@; fi
$(MAKE) test-coq-tactic; fi
###############
# test targets
......@@ -1678,11 +1673,8 @@ test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
@rm -f test-session.opt why3session.xml why3shapes why3shapes.gz
test-coq-tactic.byte: src/coq-tactic/.why3-vo-byte
$(COQC) -byte $(COQRTAC) bench/coq-tactic/test.v
test-coq-tactic.opt: src/coq-tactic/.why3-vo-opt
$(COQC) -opt $(COQRTAC) bench/coq-tactic/test.v
test-coq-tactic: lib/coq-tactic/Why3.vo
$(COQC) $(COQRTAC) bench/coq-tactic/test.v
#only test the compilation of runstrat
test-runstrat.byte: lib/why3/why3.cma lib/why3/META
......
......@@ -507,9 +507,9 @@ if test "$enable_coq_support" = yes; then
COQVERSION=`$COQC -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
#Even if the name of the variable is CAMLP4 the value can be camlp5
CAMLP4BIN=`coqtop -config | sed -n -e 's/CAMLP4BIN=\(.*\)$/\1/p'`
CAMLP4=`coqtop -config | sed -n -e 's/CAMLP4=\(.*\)$/\1/p'`
COQCAMLPLIB=`coqtop -config | sed -n -e 's/CAMLP4LIB=\(.*\)$/\1/p'`
CAMLP4BIN=`$COQC -config | sed -n -e 's/CAMLP4BIN=\(.*\)$/\1/p'`
CAMLP4=`$COQC -config | sed -n -e 's/CAMLP4=\(.*\)$/\1/p'`
COQCAMLPLIB=`$COQC -config | sed -n -e 's/CAMLP4LIB=\(.*\)$/\1/p'`
case $COQVERSION in
8.4*)
......@@ -577,6 +577,15 @@ if test "$enable_coq_tactic" = yes; then
fi
fi
if test "$enable_coq_tactic" = yes -a "$OCAMLBEST" = "byte"; then
AC_CHECK_PROG(COQTOPBYTE,coqtop.byte,coqtop.byte,no)
if test "$COQTOPBYTE" = no; then
enable_coq_tactic=no
AC_MSG_WARN(Cannot find coqtop.byte.)
reason_coq_tactic=" (byte compilation needed but coqtop.byte not found)"
fi
fi
if test "$enable_coq_libs" = yes; then
AC_MSG_CHECKING([for Flocq])
AS_IF(
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment