Install Coq development (.vo files) if requested (#232)

.vo files are installed if configure options
-install-coqdev or -clightgen or -coqdevdir are given.

Installation directory is $(PREFIX)/lib/compcert/coq by default and
can be changed by configure option -coqdevdir.

Closes: #227

2 files changed, 36 insertions, 4 deletions

diff --git a/Makefile b/Makefile
index 748c2e29..1f2879cd 100644
--- a/Makefile
+++ b/Makefile
@@ -21,7 +21,7 @@ else
 ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH)
 endif
 
-DIRS=lib common $(ARCHDIRS) backend cfrontend driver debug\
+DIRS=lib common $(ARCHDIRS) backend cfrontend driver \
   flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight \
   cparser cparser/validator
 
@@ -253,6 +253,15 @@ install:
 ifeq ($(CLIGHTGEN),true)
 	install -m 0755 ./clightgen $(BINDIR)
 endif
+ifeq ($(INSTALL_COQDEV),true)
+	install -d $(COQDEVDIR)
+	for d in $(DIRS); do \
+          install -d $(COQDEVDIR)/$$d && \
+          install -m 0644 $$d/*.vo $(COQDEVDIR)/$$d/; \
+	done
+	@(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(COQDEVDIR)/README
+endif
+
 
 clean:
 	rm -f $(patsubst %, %/*.vo, $(DIRS))
diff --git a/configure b/configure
index 03fc1471..4459e9d5 100755
--- a/configure
+++ b/configure
@@ -18,11 +18,13 @@
 prefix='/usr/local'
 bindir='$(PREFIX)/bin'
 libdir='$(PREFIX)/lib/compcert'
+coqdevdir='$(PREFIX)/lib/compcert/coq'
 toolprefix=''
 target=''
 has_runtime_lib=true
 has_standard_headers=true
 clightgen=false
+install_coqdev=false
 responsefile="gnu"
 ignore_coq_version=false
 
@@ -75,10 +77,12 @@ Options:
   -prefix <dir>        Install in <dir>/bin and <dir>/lib/compcert
   -bindir <dir>        Install binaries in <dir>
   -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>
   -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 the clightgen tool
+  -clightgen           Also compile and install the clightgen tool
+  -install-coqdev      Also install the Coq development (implied by -clightgen)
   -ignore-coq-version  Accept to use experimental or unsupported versions of Coq
 '
 
@@ -96,6 +100,8 @@ while : ; do
         bindir="$2"; shift;;
     -libdir|--libdir)
         libdir="$2"; shift;;
+    -coqdevdir|--coqdevdir)
+        coqdevdir="$2"; install_coqdev=true; shift;;
     -toolprefix|--toolprefix)
         toolprefix="$2"; shift;;
     -no-runtime-lib)
@@ -103,9 +109,12 @@ while : ; do
     -no-standard-headers)
         has_standard_headers=false;;
     -clightgen)
-        clightgen=true;;
+        clightgen=true
+        install_coqdev=true;;
     -ignore-coq-version|--ignore-coq-version)
         ignore_coq_version=true;;
+    -install-coqdev|--install-coqdev|-install-coq-dev|--install-coq-dev)
+        install_coqdev=true;;
     *)
         if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi
         target="$1";;
@@ -623,6 +632,7 @@ BINDIR=$bindir
 LIBDIR=$libdir
 MANDIR=$sharedir/man
 SHAREDIR=$sharedir
+COQDEVDIR=$coqdevdir
 OCAML_OPT_COMP=$ocaml_opt_comp
 MENHIR_INCLUDES=$menhir_includes
 COMPFLAGS=-bin-annot
@@ -646,6 +656,7 @@ CPREPRO_OPTIONS=$cprepro_options
 ENDIANNESS=$endianness
 HAS_RUNTIME_LIB=$has_runtime_lib
 HAS_STANDARD_HEADERS=$has_standard_headers
+INSTALL_COQDEV=$install_coqdev
 LIBMATH=$libmath
 MODEL=$model
 SYSTEM=$system
@@ -761,6 +772,7 @@ else
 
 bindirexp=`echo "$bindir" | sed -e "s|\\\$(PREFIX)|$prefix|"`
 libdirexp=`echo "$libdir" | sed -e "s|\\\$(PREFIX)|$prefix|"`
+coqdevdirexp=`echo "$coqdevdir" | sed -e "s|\\\$(PREFIX)|$prefix|"`
 
 cat <<EOF
 
@@ -778,12 +790,23 @@ CompCert configuration:
     Linker........................ $clinker
     Linker needs '-no-pie'........ $clinker_needs_no_pie
     Math library.................. $libmath
+    Build command to use.......... $make
     Binaries installed in......... $bindirexp
     Runtime library provided...... $has_runtime_lib
     Library files installed in.... $libdirexp
     Standard headers provided..... $has_standard_headers
     Standard headers installed in. $libdirexp/include
-    Build command to use.......... $make
+EOF
 
+if $install_coqdev; then
+cat <<EOF
+    Coq development installed in.. $coqdevdirexp
+EOF
+else
+cat <<EOF
+    Coq development will not be installed
 EOF
 fi
+
+fi
+