diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 156 |
1 files changed, 81 insertions, 75 deletions
@@ -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 @@ -48,11 +50,11 @@ Supported targets: armeb-hardfloat (ARM, EABI using hardware FP registers, big endian) x86_32-linux (x86 32 bits, Linux) x86_32-bsd (x86 32 bits, BSD) - x86_32-macosx (x86 32 bits, MacOS X) x86_32-cygwin (x86 32 bits, Cygwin environment under Windows) x86_64-linux (x86 64 bits, Linux) x86_64-bsd (x86 64 bits, BSD) x86_64-macosx (x86 64 bits, MacOS X) + x86_64-cygwin (x86 64 bits, Cygwin environment under Windows) rv32-linux (RISC-V 32 bits, Linux) rv64-linux (RISC-V 64 bits, Linux) kvx-mbr (Kalray KVX, bare runtime) @@ -87,6 +89,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 @@ -127,6 +131,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;; -*) @@ -332,29 +340,6 @@ if test "$arch" = "x86" -a "$bitsize" = "32"; then libmath="-lm" system="linux" ;; - macosx) - # kernel major versions count upwards from 4 for OSX 10.0 to 15 for OSX 10.11 - kernel_major=`uname -r | cut -d "." -f 1` - - abi="macosx" - casm="${toolprefix}gcc" - casm_options="-arch i386 -c" - cc="${toolprefix}gcc -arch i386" - clinker="${toolprefix}gcc" - clinker_needs_no_pie=false - cprepro="${toolprefix}gcc" - cprepro_options="-std=c99 -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -E" - libmath="" - system="macosx" - - if [[ $kernel_major -gt 11 ]]; then - # OSX >= 10.8 - clinker_options="-arch i386 -Wl,-no_pie" - else - # OSX <= 10.7 - clinker_options="-arch i386" - fi - ;; *) echo "Error: invalid eabi/system '$target' for architecture IA32/X86_32." 1>&2 echo "$usage" 1>&2 @@ -407,6 +392,18 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then libmath="" system="macosx" ;; + cygwin) + abi="standard" + casm="${toolprefix}gcc" + casm_options="-m64 -c" + cc="${toolprefix}gcc -m64" + clinker="${toolprefix}gcc" + clinker_options="-m64" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -m64 -U__GNUC__ '-D__attribute__(x)=' -E" + libmath="-lm" + system="cygwin" + ;; *) echo "Error: invalid eabi/system '$target' for architecture X86_64." 1>&2 echo "$usage" 1>&2 @@ -568,24 +565,24 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2) + 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" if $ignore_coq_version; then echo "Warning: this version of Coq is unsupported, proceed at your own risks." else - echo "Error: CompCert requires one of the following Coq versions: 8.11.1, 8.11.0, 8.10.2, 8.10.1, 8.10.0, 8.9.1, 8.9.0" + echo "Error: CompCert requires a version of Coq between 8.8.0 and 8.12.1" missingtools=true fi;; "") echo "NOT FOUND" - echo "Error: make sure Coq version 8.9.1 is installed." + echo "Error: make sure Coq version 8.11.2 is installed." missingtools=true;; esac echo "Testing OCaml... " | tr -d '\n' -ocaml_ver=`ocamlopt -version 2>/dev/null` +ocaml_ver=`ocamlc -version 2>/dev/null` case "$ocaml_ver" in 4.00.*|4.01.*| 4.02.*|4.03.*|4.04.*) echo "version $ocaml_ver -- UNSUPPORTED" @@ -603,9 +600,19 @@ case "$ocaml_ver" in missingtools=true;; esac +echo "Testing OCaml native-code compiler..." | tr -d '\n' +ocamlopt_ver=`ocamlopt -version 2>/dev/null` +if test "$ocamlopt_ver" = "$ocaml_ver"; then + echo "yes" + ocaml_native_comp=true +else + echo "no, will build to bytecode only" + ocaml_native_comp=false +fi + echo "Testing OCaml .opt compilers... " | tr -d '\n' -ocaml_opt_ver=`ocamlopt.opt -version 2>/dev/null` -if test "$ocaml_opt_ver" = "$ocaml_ver"; then +ocamlopt_opt_ver=`ocamlopt.opt -version 2>/dev/null` +if test "$ocamlopt_opt_ver" = "$ocaml_ver"; then echo "yes" ocaml_opt_comp=true else @@ -620,8 +627,11 @@ case "$menhir_ver" in 20[0-9][0-9][0-9][0-9][0-9][0-9]) if test "$menhir_ver" -ge $MENHIR_REQUIRED; then echo "version $menhir_ver -- good!" - menhir_dir=$(menhir --suggest-menhirLib | tr -d '\r' | tr '\\' '/') - if test -z "$menhir_dir"; then + menhir_dir=$(ocamlfind query menhirLib 2>/dev/null) || \ + menhir_dir=$(menhir --suggest-menhirLib) || \ + menhir_dir="" + menhir_dir=$(echo "$menhir_dir" | tr -d '\r' | tr '\\' '/') + if test ! -d "$menhir_dir"; then echo "Error: cannot determine the location of the Menhir API library." echo "This can be due to an incorrect Menhir package." echo "Consider using the OPAM package for Menhir." @@ -660,49 +670,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 scheduling compcert.scheduling \ --R cfrontend compcert.cfrontend \ --R driver compcert.driver \ --R flocq compcert.flocq \ --R exportclight compcert.exportclight \ --R cparser compcert.cparser \ --R MenhirLib compcert.MenhirLib --R Impure lib.Impure" > _CoqProject -case $arch in - x86) - echo "-R x86_${bitsize} compcert.x86_${bitsize}" >> _CoqProject - ;; -esac - # # Generate Makefile.config # @@ -716,6 +683,7 @@ LIBDIR=$libdir MANDIR=$sharedir/man SHAREDIR=$sharedir COQDEVDIR=$coqdevdir +OCAML_NATIVE_COMP=$ocaml_native_comp OCAML_OPT_COMP=$ocaml_opt_comp MENHIR_DIR=$menhir_dir COMPFLAGS=-bin-annot @@ -744,6 +712,8 @@ LIBMATH=$libmath MODEL=$model SYSTEM=$system RESPONSEFILE=$responsefile +LIBRARY_FLOCQ=$library_Flocq +LIBRARY_MENHIRLIB=$library_MenhirLib EOF else cat >> Makefile.config <<'EOF' @@ -837,6 +807,9 @@ 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 @@ -851,6 +824,7 @@ BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v # TODO: UPDATE THIS # DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v +EXTRA_EXTRACTION= Asmgen.Asmgen_expand.loadimm32 Asmgen.Asmgen_expand.addimm64 Asmgen.Asmgen_expand.storeptr EOF fi @@ -869,6 +843,35 @@ 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 @@ -905,6 +908,9 @@ CompCert configuration: Linker needs '-no-pie'........ $clinker_needs_no_pie 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 |