diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-23 13:53:39 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-23 13:53:39 +0100 |
commit | 44b63eb13151ca5c3e83ee6a9e7eb6c0049c3758 (patch) | |
tree | 6d70e30186b00d400a1823910b601e7a2dfd24a6 | |
parent | 1e867c804ed11200c8ed1a55a71f416977249363 (diff) | |
download | compcert-44b63eb13151ca5c3e83ee6a9e7eb6c0049c3758.tar.gz compcert-44b63eb13151ca5c3e83ee6a9e7eb6c0049c3758.zip |
Add a switch to generate a _CoqProject file.
-rw-r--r-- | .gitignore | 3 | ||||
-rwxr-xr-x | configure | 22 |
2 files changed, 24 insertions, 1 deletions
@@ -11,7 +11,6 @@ .*.aux *.cmti *.cmt -*.merlin # Emacs saves *~ # Executables and configuration @@ -23,6 +22,8 @@ clightgen.byte tools/ndfun tools/modorder Makefile.config +.merlin +_CoqProject # Generated files .depend .depend.extr @@ -22,6 +22,7 @@ has_standard_headers=true clightgen=false responsefile="gnu" merlin=false +coqproject=false usage='Usage: ./configure [options] target @@ -71,6 +72,7 @@ Options: -no-standard-headers Do not install nor use the standard .h headers -clightgen Also compile the clightgen tool -merlin Generate .merlin file + -coqproject Generate a _CoqProject file for Proof General ' @@ -97,6 +99,8 @@ while : ; do clightgen=true;; -merlin) merlin=true;; + -coqproject) + coqproject=true;; *) if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi target="$1";; @@ -515,6 +519,24 @@ B extraction EOF fi + +if $coqproject; then + 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" > _CoqProject + case $arch in + x86) + echo "-R x86_${bitsize} compcert.x86_${bitsize}" >> _CoqProject + ;; + esac +fi + # # Generate Makefile.config # |