Support the use of already-installed MenhirLib and Flocq libraries

configure flags -use-external-Flocq and -use external-MenhirLib.

11 files changed, 82 insertions, 67 deletions

diff --git a/Makefile b/Makefile
index 127ed5d2..4b0b5761 100644
--- a/Makefile
+++ b/Makefile
@@ -27,14 +27,19 @@ else
 ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH)
 endif
 
-DIRS=lib common $(ARCHDIRS) backend cfrontend driver \
-  flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 \
-  exportclight MenhirLib cparser
+DIRS := lib common $(ARCHDIRS) backend cfrontend driver exportclight cparser
 
-RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \
-  MenhirLib cparser
+COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(d))
 
-COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d))
+ifeq ($(LIBRARY_FLOCQ),local)
+DIRS += flocq/Core flocq/Prop flocq/Calc flocq/IEEE754
+COQINCLUDES += -R flocq Flocq
+endif
+
+ifeq ($(LIBRARY_MENHIRLIB),local)
+DIRS += MenhirLib
+COQINCLUDES += -R MenhirLib MenhirLib
+endif
 
 COQCOPTS ?= -w -undeclared-scope -w -omega-is-deprecated
 COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
@@ -50,6 +55,7 @@ GPATH=$(DIRS)
 
 # Flocq
 
+ifeq ($(LIBRARY_FLOCQ),local)
 FLOCQ=\
   Raux.v Zaux.v Defs.v Digits.v Float_prop.v FIX.v FLT.v FLX.v FTZ.v \
   Generic_fmt.v Round_pred.v Round_NE.v Ulp.v Core.v \
@@ -57,6 +63,9 @@ FLOCQ=\
   Div_sqrt_error.v Mult_error.v Plus_error.v \
   Relative.v Sterbenz.v Round_odd.v Double_rounding.v \
   Binary.v Bits.v
+else
+FLOCQ=
+endif
 
 # General-purpose libraries (in lib/)
 
@@ -117,9 +126,13 @@ PARSER=Cabs.v Parser.v
 
 # MenhirLib
 
+ifeq ($(LIBRARY_MENHIRLIB),local)
 MENHIRLIB=Alphabet.v Automaton.v Grammar.v Interpreter_complete.v \
   Interpreter_correct.v Interpreter.v Main.v Validator_complete.v \
   Validator_safe.v Validator_classes.v
+else
+MENHIRLIB=
+endif
 
 # Putting everything together (in driver/)
 
@@ -259,7 +272,7 @@ driver/Version.ml: VERSION
 
 cparser/Parser.v: cparser/Parser.vy
 	@rm -f $@
-	$(MENHIR) --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy
+	$(MENHIR) --coq --coq-no-version-check cparser/Parser.vy
 	@chmod a-w $@
 
 depend: $(GENERATED) depend1
@@ -318,6 +331,9 @@ check-proof: $(FILES)
 print-includes:
 	@echo $(COQINCLUDES)
 
+CoqProject:
+	@echo $(COQINCLUDES) > _CoqProject
+
 -include .depend
 
 FORCE:
diff --git a/aarch64/Archi.v b/aarch64/Archi.v
index 24431cb2..42500e70 100644
--- a/aarch64/Archi.v
+++ b/aarch64/Archi.v
@@ -15,9 +15,8 @@
 
 (** Architecture-dependent parameters for AArch64 *)
 
+From Flocq Require Import Binary Bits.
 Require Import ZArith List.
-(*From Flocq*)
-Require Import Binary Bits.
 
 Definition ptr64 := true.
 
diff --git a/arm/Archi.v b/arm/Archi.v
index 16d6c71d..2ca79710 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -16,9 +16,8 @@
 
 (** Architecture-dependent parameters for ARM *)
 
+From Flocq Require Import Binary Bits.
 Require Import ZArith List.
-(*From Flocq*)
-Require Import Binary Bits.
 
 Definition ptr64 := false.
 
diff --git a/configure b/configure
index a02e561f..a71901b8 100755
--- a/configure
+++ b/configure
@@ -27,6 +27,8 @@ clightgen=false
 install_coqdev=false
 responsefile="gnu"
 ignore_coq_version=false
+library_Flocq=local
+library_MenhirLib=local
 
 usage='Usage: ./configure [options] target
 For help on options and targets, do: ./configure -help
@@ -84,6 +86,8 @@ Options:
   -libdir <dir>        Install libraries in <dir>
   -coqdevdir <dir>     Install Coq development (.vo files) in <dir>
   -toolprefix <pref>   Prefix names of tools ("gcc", etc) with <pref>
+  -use-external-Flocq  Use an already-installed Flocq library
+  -use-external-MenhirLib  Use an already-installed MenhirLib library
   -no-runtime-lib      Do not compile nor install the runtime support library
   -no-standard-headers Do not install nor use the standard .h headers
   -clightgen           Also compile and install the clightgen tool
@@ -124,6 +128,10 @@ while : ; do
         ignore_coq_version=true;;
     -install-coqdev|--install-coqdev|-install-coq-dev|--install-coq-dev)
         install_coqdev=true;;
+    -use-external-Flocq|--use-external-Flocq)
+        library_Flocq=external;;
+    -use-external-MenhirLib|--use-external-MenhirLib)
+        library_MenhirLib=external;;
     -help|--help)
         echo "$help"; exit 0;;
     -*)
@@ -611,47 +619,6 @@ if $missingtools; then
   exit 2
 fi
 
-cat > .merlin <<EOF
-S lib
-S common
-S $arch
-S backend
-S cfrontend
-S driver
-S debug
-S exportclight
-S cparser
-S extraction
-
-B lib
-B common
-B $arch
-B backend
-B cfrontend
-B driver
-B debug
-B exportclight
-B cparser
-B extraction
-
-EOF
-
-echo "-R lib compcert.lib \
--R common compcert.common \
--R ${arch} compcert.${arch} \
--R backend compcert.backend \
--R cfrontend compcert.cfrontend \
--R driver compcert.driver \
--R flocq compcert.flocq \
--R exportclight compcert.exportclight \
--R cparser compcert.cparser \
--R MenhirLib compcert.MenhirLib" > _CoqProject
-case $arch in
-    x86)
-        echo "-R x86_${bitsize} compcert.x86_${bitsize}" >> _CoqProject
-        ;;
-esac
-
 #
 # Generate Makefile.config
 #
@@ -694,6 +661,8 @@ LIBMATH=$libmath
 MODEL=$model
 SYSTEM=$system
 RESPONSEFILE=$responsefile
+LIBRARY_FLOCQ=$library_Flocq
+LIBRARY_MENHIRLIB=$library_MenhirLib
 EOF
 else
 cat >> Makefile.config <<'EOF'
@@ -787,10 +756,42 @@ CLIGHTGEN=false
 # Whether the other tools support responsefiles in gnu syntax
 RESPONSEFILE="none"
 
+# Whether to use the local copies of Flocq and MenhirLib
+LIBRARY_FLOCQ=local      # external
+LIBRARY_MENHIRLIB=local  # external
 EOF
 fi
 
 #
+# Generate Merlin and CoqProject files to simplify development
+#
+cat > .merlin <<EOF
+S lib
+S common
+S $arch
+S backend
+S cfrontend
+S driver
+S debug
+S exportclight
+S cparser
+S extraction
+
+B lib
+B common
+B $arch
+B backend
+B cfrontend
+B driver
+B debug
+B exportclight
+B cparser
+B extraction
+EOF
+
+make CoqProject
+
+#
 # Clean up target-dependent files to force their recompilation
 #
 rm -f .depend $arch/Archi.vo ${arch}_${bitsize}/Archi.vo runtime/*.o
@@ -828,6 +829,8 @@ CompCert configuration:
     Math library.................. $libmath
     Build command to use.......... $make
     Menhir API library............ $menhir_dir
+    The Flocq library............. $library_Flocq
+    The MenhirLib library......... $library_MenhirLib
     Binaries installed in......... $bindirexp
     Runtime library provided...... $has_runtime_lib
     Library files installed in.... $libdirexp
@@ -846,4 +849,3 @@ EOF
 fi
 
 fi
-
diff --git a/lib/Floats.v b/lib/Floats.v
index 6a126c3f..b7769420 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -17,8 +17,7 @@
 (** Formalization of floating-point numbers, using the Flocq library. *)
 
 Require Import Coqlib Zbits Integers.
-(*From Flocq*)
-Require Import Binary Bits Core.
+From Flocq Require Import Binary Bits Core.
 Require Import IEEE754_extra.
 Require Import Program.
 Require Archi.
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index c23149be..18313ec1 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -17,11 +17,11 @@
 (** Additional operations and proofs about IEEE-754 binary
     floating-point numbers, on top of the Flocq library. *)
 
+From Flocq Require Import Core Digits Operations Round Bracket Sterbenz
+                          Binary Round_odd.
 Require Import Psatz.
 Require Import Bool.
 Require Import Eqdep_dec.
-(*From Flocq *)
-Require Import Core Digits Operations Round Bracket Sterbenz Binary Round_odd.
 
 Local Open Scope Z_scope.
 
diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index 10f38391..ae10c54c 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -16,9 +16,8 @@
 
 (** Architecture-dependent parameters for PowerPC *)
 
+From Flocq Require Import Binary Bits.
 Require Import ZArith List.
-(*From Flocq*)
-Require Import Binary Bits.
 
 Definition ptr64 := false.
 
diff --git a/riscV/Archi.v b/riscV/Archi.v
index 61d129d0..1b24e732 100644
--- a/riscV/Archi.v
+++ b/riscV/Archi.v
@@ -16,9 +16,8 @@
 
 (** Architecture-dependent parameters for RISC-V *)
 
+From Flocq Require Import Binary Bits.
 Require Import ZArith List.
-(*From Flocq*)
-Require Import Binary Bits.
 
 Parameter ptr64 : bool.
 
diff --git a/test/clightgen/Makefile b/test/clightgen/Makefile
index bf4a044b..fdfbc3fb 100644
--- a/test/clightgen/Makefile
+++ b/test/clightgen/Makefile
@@ -5,8 +5,12 @@ ARCHDIRS=$(ARCH)
 else
 ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH)
 endif
-RECDIRS=lib common $(ARCHDIRS) cfrontend flocq  exportclight
-COQINCLUDES=$(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d))
+RECDIRS := lib common $(ARCHDIRS) cfrontend  exportclight
+COQINCLUDES := $(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d))
+ifeq ($(LIBRARY_FLOCQ),local)
+COQINCLUDES += -R ../../flocq Flocq
+endif
+
 
 CLIGHTGEN=../../clightgen
 COQC=coqc
diff --git a/x86_32/Archi.v b/x86_32/Archi.v
index e9d05c14..b7e8e586 100644
--- a/x86_32/Archi.v
+++ b/x86_32/Archi.v
@@ -16,9 +16,8 @@
 
 (** Architecture-dependent parameters for x86 in 32-bit mode *)
 
+From Flocq Require Import Binary Bits.
 Require Import ZArith List.
-(*From Flocq*)
-Require Import Binary Bits.
 
 Definition ptr64 := false.
 
diff --git a/x86_64/Archi.v b/x86_64/Archi.v
index 959d8dc1..6dc0044f 100644
--- a/x86_64/Archi.v
+++ b/x86_64/Archi.v
@@ -16,9 +16,8 @@
 
 (** Architecture-dependent parameters for x86 in 64-bit mode *)
 
+From Flocq Require Import Binary Bits.
 Require Import ZArith List.
-(*From Flocq*)
-Require Import Binary Bits.
 
 Definition ptr64 := true.