From d18371174552ed29069a34d81d60530df431ac0f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 1 May 2013 12:37:36 +0000 Subject: Use "-as" to put CompCert modules in a compcert.xxx namespace. Simplified the scripts "coq" and "pg". Updated deps. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- .depend | 14 +++++++------- Makefile | 23 ++++++++++++++++------- coq | 6 ++---- doc/coq2html.mll | 20 ++++++++++++++------ pg | 15 +++++++++++---- 5 files changed, 50 insertions(+), 28 deletions(-) diff --git a/.depend b/.depend index e55e84c..057f4f9 100644 --- a/.depend +++ b/.depend @@ -31,7 +31,7 @@ backend/CminorSel.vo backend/CminorSel.glob backend/CminorSel.v.beautified: back $(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob $(ARCH)/SelectOp.v.beautified: $(ARCH)/SelectOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo backend/SelectLong.vo backend/SelectLong.glob backend/SelectLong.v.beautified: backend/SelectLong.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo common/Errors.vo backend/Selection.vo backend/Selection.glob backend/Selection.v.beautified: backend/Selection.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectLong.vo -$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo +$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectLongproof.vo backend/SelectLongproof.glob backend/SelectLongproof.v.beautified: backend/SelectLongproof.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectLong.vo backend/Selectionproof.vo backend/Selectionproof.glob backend/Selectionproof.v.beautified: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectLong.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo backend/SelectLongproof.vo backend/Registers.vo backend/Registers.glob backend/Registers.v.beautified: backend/Registers.v lib/Coqlib.vo common/AST.vo lib/Maps.vo lib/Ordered.vo @@ -51,13 +51,13 @@ backend/Kildall.vo backend/Kildall.glob backend/Kildall.v.beautified: backend/Ki backend/Liveness.vo backend/Liveness.glob backend/Liveness.v.beautified: backend/Liveness.v lib/Coqlib.vo lib/Maps.vo lib/Lattice.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob $(ARCH)/ConstpropOp.v.beautified: $(ARCH)/ConstpropOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/Constprop.vo backend/Constprop.glob backend/Constprop.v.beautified: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Liveness.vo $(ARCH)/ConstpropOp.vo -$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo +$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo backend/Constpropproof.vo backend/Constpropproof.glob backend/Constpropproof.v.beautified: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Liveness.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOp.glob $(ARCH)/CombineOp.v.beautified: $(ARCH)/CombineOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo $(ARCH)/SelectOp.vo backend/CSE.vo backend/CSE.glob backend/CSE.v.beautified: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo $(ARCH)/CombineOp.vo -$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/CombineOp.vo backend/CSE.vo +$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/RTL.vo $(ARCH)/CombineOp.vo backend/CSE.vo backend/CSEproof.vo backend/CSEproof.glob backend/CSEproof.v.beautified: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOpproof.vo backend/CSE.vo -$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo +$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/Locations.glob backend/Locations.v.beautified: backend/Locations.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo $(ARCH)/$(VARIANT)/Conventions1.vo $(ARCH)/$(VARIANT)/Conventions1.glob $(ARCH)/$(VARIANT)/Conventions1.v.beautified: $(ARCH)/$(VARIANT)/Conventions1.v lib/Coqlib.vo common/AST.vo backend/Locations.vo backend/Conventions.vo backend/Conventions.glob backend/Conventions.v.beautified: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions1.vo @@ -78,10 +78,10 @@ $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/$(VARIANT)/Stacklayout.glob $(ARCH)/$( backend/Stacking.vo backend/Stacking.glob backend/Stacking.v.beautified: backend/Stacking.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Lineartyping.vo backend/Stackingproof.vo backend/Stackingproof.glob backend/Stackingproof.v.beautified: backend/Stackingproof.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo $(ARCH)/Asm.vo $(ARCH)/Asm.glob $(ARCH)/Asm.v.beautified: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo -$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo +$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memdata.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo backend/Asmgenproof0.vo backend/Asmgenproof0.glob backend/Asmgenproof0.v.beautified: backend/Asmgenproof0.v lib/Coqlib.vo lib/Intv.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo -$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo backend/Asmgenproof0.vo -$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo +$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo backend/Conventions.vo +$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo cfrontend/Ctypes.vo cfrontend/Ctypes.glob cfrontend/Ctypes.v.beautified: cfrontend/Ctypes.v lib/Coqlib.vo common/AST.vo common/Errors.vo cfrontend/Cop.vo cfrontend/Cop.glob cfrontend/Cop.v.beautified: cfrontend/Cop.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo cfrontend/Ctypes.vo cfrontend/Csyntax.vo cfrontend/Csyntax.glob cfrontend/Csyntax.v.beautified: cfrontend/Csyntax.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo diff --git a/Makefile b/Makefile index 0db4118..cced7da 100644 --- a/Makefile +++ b/Makefile @@ -13,22 +13,28 @@ include Makefile.config DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver \ - flocq/Core flocq/Prop flocq/Calc flocq/Appli + flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight -INCLUDES=$(patsubst %,-I %, $(DIRS)) +RECDIRS=lib common backend cfrontend driver flocq exportclight -COQC=coqc -q $(INCLUDES) -COQDEP=coqdep $(INCLUDES) +COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) -as compcert.$(d)) \ + -I $(ARCH)/$(VARIANT) -as compcert.$(ARCH).$(VARIANT) \ + -I $(ARCH) -as compcert.$(ARCH) + +CAMLINCLUDES=$(patsubst %,-I %, $(DIRS)) -I extraction -I cparser + +COQC=coqc -q $(COQINCLUDES) +COQDEP=coqdep $(COQINCLUDES) COQDOC=coqdoc -COQEXEC=coqtop $(INCLUDES) -batch -load-vernac-source -COQCHK=coqchk $(INCLUDES) +COQEXEC=coqtop $(COQINCLUDES) -batch -load-vernac-source +COQCHK=coqchk $(COQINCLUDES) OCAMLBUILD=ocamlbuild OCB_OPTIONS=\ -j 2 \ -no-hygiene \ -no-links \ - -I extraction -I cparser $(INCLUDES) + $(CAMLINCLUDES) OCB_OPTIONS_CHECKLINK=\ $(OCB_OPTIONS) \ -I checklink \ @@ -251,6 +257,9 @@ check-admitted: $(FILES) check-proof: $(FILES) $(COQCHK) -admit Integers -admit Floats -admit AST -admit Asm -admit Mach -admit UnionFind Complements +print-includes: + @echo $(COQINCLUDES) + include .depend FORCE: diff --git a/coq b/coq index ce3e1ed..ea08805 100755 --- a/coq +++ b/coq @@ -3,8 +3,7 @@ # Use the Makefile to rebuild dependencies if needed # Recompile the modified file after coqide editing -ARCH=`sed -n -e 's/^ARCH=//p' Makefile.config` -VARIANT=`sed -n -e 's/^VARIANT=//p' Makefile.config` +INCLUDES=`make print-includes` make -q ${1}o || { make -n ${1}o | grep -v "\\b${1}\\b" | \ @@ -13,5 +12,4 @@ make -q ${1}o || { done) } -coqide -I lib -I common -I $ARCH/$VARIANT -I $ARCH -I backend -I cfrontend -I flocq -I flocq/Appli -I flocq/Calc -I flocq/Core -I flocq/Prop $1 \ -&& make ${1}o +coqide $INCLUDES $1 && make ${1}o diff --git a/doc/coq2html.mll b/doc/coq2html.mll index 9c30bea..4f04f98 100644 --- a/doc/coq2html.mll +++ b/doc/coq2html.mll @@ -35,9 +35,11 @@ let path sp id = | _ , _ -> sp ^ "." ^ id let add_module m = + (*eprintf "add_module %s\n" m;*) Hashtbl.add xref_modules m () let add_reference curmod pos dp sp id ty = + (*eprintf "add_reference %s %d %s %s %s %s\n" curmod pos dp sp id ty;*) if not (Hashtbl.mem xref_table (curmod, pos)) then Hashtbl.add xref_table (curmod, pos) (Ref(dp, path sp id, ty)) @@ -51,15 +53,19 @@ let coqlib_url = "http://coq.inria.fr/library/" let re_coqlib = Str.regexp "Coq\\." let re_sane_path = Str.regexp "[A-Za-z0-9_.]+$" +let re_shortname = Str.regexp "^.*\\." + +let shortname m = Str.replace_first re_shortname "" m let crossref m pos = + (*eprintf "crossref %s %d\n" m pos;*) try match Hashtbl.find xref_table (m, pos) with | Def(p, ty) -> Anchor p | Ref(m', p, ty) -> let url = if Hashtbl.mem xref_modules m' then - m' ^ ".html" + shortname m' ^ ".html" else if Str.string_match re_coqlib m' 0 then coqlib_url ^ m' ^ ".html" else @@ -367,7 +373,7 @@ and verbatim = parse and globfile = parse | eof { () } - | "F" (ident as m) space* "\n" + | "F" (path as m) space* "\n" { current_module := m; add_module m; globfile lexbuf } | "R" (integer as pos) ":" (integer as pos2) @@ -394,14 +400,16 @@ let output_name = ref "-" let process_file f = if Filename.check_suffix f ".v" then begin - current_module := Filename.chop_suffix (Filename.basename f) ".v"; + let pref_f = Filename.chop_suffix f ".v" in + let base_f = Filename.basename pref_f in + current_module := + "compcert." ^ Str.global_replace (Str.regexp "/") "." pref_f; let ic = open_in f in if !output_name = "-" then oc := stdout else - oc := open_out (Str.global_replace (Str.regexp "%") !current_module - !output_name); - start_html_page !current_module; + oc := open_out (Str.global_replace (Str.regexp "%") base_f !output_name); + start_html_page base_f; coq_bol (Lexing.from_channel ic); end_html_page(); if !output_name <> "-" then (close_out !oc; oc := stdout); diff --git a/pg b/pg index 9242303..33a70ce 100755 --- a/pg +++ b/pg @@ -4,9 +4,7 @@ # Recompile the modified file after coqide editing PWD=`pwd` -ARCH=$PWD/`sed -n -e 's/^ARCH=//p' Makefile.config` -VARIANT=$ARCH/`sed -n -e 's/^VARIANT=//p' Makefile.config` - +INCLUDES=`make print-includes` make -q ${1}o || { make -n ${1}o | grep -v "\\b${1}\\b" | \ @@ -14,9 +12,18 @@ make -q ${1}o || { sh -c "$cmd" || exit 2 done) } + COQPROGNAME="coqtop" -COQPROGARGS="\"-I\" \"$PWD/lib\" \"-I\" \"$PWD/common\" \"-I\" \"$VARIANT\" \"-I\" \"$ARCH\" \"-I\" \"$PWD/backend\" \"-I\" \"$PWD/cfrontend\" \"-I\" \"$PWD/flocq\" \"-I\" \"$PWD/flocq/Appli\" \"-I\" \"$PWD/flocq/Calc\" \"-I\" \"$PWD/flocq/Core\" \"-I\" \"$PWD/flocq/Prop\"" +COQPROGARGS="" +for arg in $INCLUDES; do + case "$arg" in + -I|-R|-as|compcert*) + COQPROGARGS="$COQPROGARGS \"$arg\"";; + *) + COQPROGARGS="$COQPROGARGS \"$PWD/$arg\"";; + esac +done emacs --eval "(setq coq-prog-name \"$COQPROGNAME\")" \ --eval "(setq coq-prog-args '($COQPROGARGS))" $1 \ -- cgit v1.2.3