diff options
-rw-r--r-- | Makefile | 30 | ||||
-rw-r--r-- | aarch64/Archi.v | 3 | ||||
-rw-r--r-- | arm/Archi.v | 3 | ||||
-rwxr-xr-x | configure | 86 | ||||
-rw-r--r-- | lib/Floats.v | 3 | ||||
-rw-r--r-- | lib/IEEE754_extra.v | 4 | ||||
-rw-r--r-- | powerpc/Archi.v | 3 | ||||
-rw-r--r-- | riscV/Archi.v | 3 | ||||
-rw-r--r-- | test/clightgen/Makefile | 8 | ||||
-rw-r--r-- | x86_32/Archi.v | 3 | ||||
-rw-r--r-- | x86_64/Archi.v | 3 |
11 files changed, 82 insertions, 67 deletions
@@ -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. @@ -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. |