make libraries, lexing of more utf8 symbols

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5201 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 180 insertions, 54 deletions

diff --git a/Makefile b/Makefile
index 7ad21c5da7..d38c15e7c1 100644
--- a/Makefile
+++ b/Makefile
@@ -61,7 +61,7 @@ LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \
 	      -I ide -I translate \
               -I contrib/omega -I contrib/romega \
 	      -I contrib/ring -I contrib/xml \
-	      -I contrib/extraction -I contrib/correctness \
+	      -I contrib/extraction \
               -I contrib/interface -I contrib/fourier \
 	      -I contrib/jprover -I contrib/cc \
 	      -I contrib/funind -I contrib/first-order
@@ -231,10 +231,10 @@ INTERFACECMX=$(INTERFACE:.cmo=.cmx)
 ML4FILES += contrib/interface/debug_tac.ml4 contrib/interface/centaur.ml4
 
 PARSERREQUIRES=$(CMO) # Solution de facilité...
-PARSERREQUIRESCMX=$(PARSERREQUIRES:.cmo=.cmx)
+PARSERREQUIRESCMX=$(CMX)
 
 ML4FILES +=\
-  contrib/correctness/psyntax.ml4 contrib/omega/g_omega.ml4 \
+  contrib/omega/g_omega.ml4 \
   contrib/romega/g_romega.ml4 contrib/ring/g_quote.ml4 \
   contrib/ring/g_ring.ml4 \
   contrib/field/field.ml4 contrib/fourier/g_fourier.ml4 \
@@ -278,17 +278,6 @@ EXTRACTIONCMO=\
   contrib/extraction/extract_env.cmo \
   contrib/extraction/g_extraction.cmo
 
-CORRECTNESSCMO=\
-  contrib/correctness/pmisc.cmo					  \
-  contrib/correctness/peffect.cmo contrib/correctness/prename.cmo \
-  contrib/correctness/perror.cmo contrib/correctness/penv.cmo  	  \
-  contrib/correctness/putil.cmo contrib/correctness/pdb.cmo	  \
-  contrib/correctness/pcic.cmo contrib/correctness/pmonad.cmo     \
-  contrib/correctness/pcicenv.cmo  				  \
-  contrib/correctness/pred.cmo contrib/correctness/ptyping.cmo	  \
-  contrib/correctness/pwp.cmo contrib/correctness/pmlize.cmo	  \
-  contrib/correctness/ptactic.cmo  contrib/correctness/psyntax.cmo
-
 JPROVERCMO=\
   contrib/jprover/opname.cmo \
   contrib/jprover/jterm.cmo contrib/jprover/jlogic.cmo \
@@ -311,21 +300,22 @@ ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4 \
 
 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) \
 	$(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \
-	$(CORRECTNESSCMO) $(CCCMO) $(FUNINDCMO) $(FOCMO)
+	$(CCCMO) $(FUNINDCMO) $(FOCMO)
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
 
-CMO=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) \
-    $(INTERP) $(PARSING) $(PROOFS) $(TACTICS) $(TOPLEVEL) \
-    $(HIGHPARSING) $(HIGHTACTICS) $(CONTRIB) $(HIGHPARSINGNEW)
-CMX=$(CMO:.cmo=.cmx)
+CMO=$(CONFIG) lib.cma kernel.cma library.cma pretyping.cma \
+    interp.cma parsing.cma proofs.cma tactics.cma toplevel.cma \
+    highparsing.cma hightactics.cma contrib.cma highparsingnew.cma
+CMOCMXA=$(CMO:.cma=.cmxa)
+CMX=$(CMOCMXA:.cmo=.cmx)
 
 ###########################################################################
 # Main targets (coqmktop, coqtop.opt, coqtop.byte)
 ###########################################################################
 
-COQMKTOP=bin/coqmktop$(EXE)
+COQMKTOP=bin/coqmktop$(EXE) 
 COQC=bin/coqc$(EXE)
 COQTOPBYTE=bin/coqtop.byte$(EXE)
 COQTOPOPT=bin/coqtop.opt$(EXE)
@@ -436,12 +426,12 @@ ide: coqide-$(HASCOQIDE) states
 clean-ide: 
 	rm -f $(OLDCOQIDEVO) $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT)
 
-$(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) $(COQIDECMX)
+$(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) ide.cmxa
 	$(SHOW)'COQMKTOP -o $@'	
 	$(HIDE)$(COQMKTOP) -ide -opt $(OPTFLAGS) -o $@
 	$(STRIP) $@
 
-$(COQIDEBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) $(COQIDECMO)
+$(COQIDEBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) ide.cma
 	$(SHOW)'COQMKTOP -o $@'	
 	$(HIDE)$(COQMKTOP) -g -ide -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@
 
@@ -509,6 +499,121 @@ highparsingnew: $(HIGHPARSINGNEW)
 toplevel: $(TOPLEVEL)
 hightactics: $(HIGHTACTICS)
 
+# target for libraries
+
+lib.cma: $(LIBREP)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(LIBREP)
+
+lib.cmxa: $(LIBREP:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(LIBREP:.cmo=.cmx)
+
+kernel.cma: $(KERNEL)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(KERNEL)
+
+kernel.cmxa: $(KERNEL:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(KERNEL:.cmo=.cmx)
+
+library.cma: $(LIBRARY)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(LIBRARY)
+
+library.cmxa: $(LIBRARY:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(LIBRARY:.cmo=.cmx)
+
+pretyping.cma: $(PRETYPING)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PRETYPING)
+
+pretyping.cmxa: $(PRETYPING:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PRETYPING:.cmo=.cmx)
+
+interp.cma: $(INTERP)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(INTERP)
+
+interp.cmxa: $(INTERP:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(INTERP:.cmo=.cmx)
+
+parsing.cma: $(PARSING)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PARSING)
+
+parsing.cmxa: $(PARSING:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PARSING:.cmo=.cmx)
+
+proofs.cma: $(PROOFS)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PROOFS)
+
+proofs.cmxa: $(PROOFS:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PROOFS:.cmo=.cmx)
+
+tactics.cma: $(TACTICS)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(TACTICS)
+
+tactics.cmxa: $(TACTICS:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(TACTICS:.cmo=.cmx)
+
+toplevel.cma: $(TOPLEVEL)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(TOPLEVEL)
+
+toplevel.cmxa: $(TOPLEVEL:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(TOPLEVEL:.cmo=.cmx)
+
+highparsing.cma: $(HIGHPARSING)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHPARSING)
+
+highparsing.cmxa: $(HIGHPARSING:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHPARSING:.cmo=.cmx)
+
+hightactics.cma: $(HIGHTACTICS) $(USERTACCMO)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHTACTICS) $(USERTACCMO)
+
+hightactics.cmxa: $(HIGHTACTICS:.cmo=.cmx) $(USERTACCMO:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHTACTICS:.cmo=.cmx) \
+		$(USERTACCMO:.cmo=.cmx)
+
+contrib.cma: $(CONTRIB)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(CONTRIB)
+
+contrib.cmxa: $(CONTRIB:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(CONTRIB:.cmo=.cmx)
+
+highparsingnew.cma: $(HIGHPARSINGNEW)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHPARSINGNEW)
+
+highparsingnew.cmxa: $(HIGHPARSINGNEW:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHPARSINGNEW:.cmo=.cmx)
+
+ide.cma: $(COQIDECMO)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(COQIDECMO)
+
+ide.cmxa: $(COQIDECMO:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(COQIDECMO:.cmo=.cmx)
+
 # special binaries for debugging
 
 bin/coq-interface$(EXE): $(COQMKTOP) $(CMO) $(USERTACCMO) $(INTERFACE)
@@ -723,15 +828,6 @@ noreal: logic arith bool zarith lists sets intmap relations wellfounded \
 # contribs
 ###########################################################################
 
-CORRECTNESSVO=\
- contrib/correctness/Arrays.vo					\
- contrib/correctness/Correctness.vo				\
- contrib/correctness/Exchange.vo				\
- contrib/correctness/ArrayPermut.vo				\
- contrib/correctness/ProgBool.vo contrib/correctness/ProgInt.vo	\
- contrib/correctness/Sorted.vo	contrib/correctness/Tuples.vo   
-# contrib/correctness/ProgramsExtraction.vo			
-
 OMEGAVO=\
  contrib/omega/OmegaLemmas.vo contrib/omega/Omega.vo
 
@@ -767,7 +863,7 @@ CCVO=\
  contrib/cc/CCSolve.vo
 
 CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
-	    $(CORRECTNESSVO) $(FOURIERVO) \
+	    $(FOURIERVO) \
 	    $(JPROVERVO) $(INTERFACEVO) $(CCVO) $(FUNINDVO)
 
 $(CONTRIBVO): states/initial.coq
@@ -778,7 +874,6 @@ ring: $(RINGVO) $(RINGCMO)
 # xml_ instead of xml to avoid conflict with "make xml"
 xml_: $(XMLVO) $(XMLCMO)
 extraction: $(EXTRACTIONCMO)
-correctness: $(CORRECTNESSCMO) $(CORRECTNESSVO)
 field: $(FIELDVO) $(FIELDCMO)
 fourier: $(FOURIERVO) $(FOURIERCMO)
 jprover: $(JPROVERVO) $(JPROVERCMO)
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 5ffd299841..61f28469c9 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -431,11 +431,20 @@ let rec next_token = parser bp
 	    (try ("", find_keyword id) with Not_found -> ("IDENT", id)),
 	    (bp, ep))
   (* iso 8859-1 accentuated letters *)
-  | [< ' ('\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c);
-      len = ident_tail (store 0 c) >] ep ->
-      let id = get_buff len in
-      comment_stop bp;
-      (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep)
+  | [< ' ('\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c) ; s >] ->
+      if !Options.v7 then
+	begin
+	  match s with parser
+	      [< len = ident_tail (store 0 c) >] ep ->
+		let id = get_buff len in
+		comment_stop bp;
+		(try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep)
+	end
+      else
+	begin
+	  match s with parser
+	      [< t = process_chars bp c >] -> comment_stop bp; t
+	end
   | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep ->
       comment_stop bp;
       (("INT", get_buff len), (bp, ep))
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index a787b1e788..acc5922ea3 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -26,23 +26,27 @@ let libobjs = ocamlobjs @ camlp4objs @ configobjs
 let spaces = Str.regexp "[ \t\n]+"
 let split_cmo l = Str.split spaces l
 
-let lib = split_cmo Tolink.lib
+let lib = split_cmo Tolink.lib 
 let kernel = split_cmo Tolink.kernel
-let library = split_cmo Tolink.library
-let pretyping = split_cmo Tolink.pretyping
+let library = split_cmo Tolink.library 
+let pretyping = split_cmo Tolink.pretyping 
 let interp = split_cmo Tolink.interp
-let parsing = split_cmo Tolink.parsing
-let proofs = split_cmo Tolink.proofs
-let tactics = split_cmo Tolink.tactics
-let toplevel = split_cmo Tolink.toplevel
-let highparsing = split_cmo Tolink.highparsing
+let parsing = split_cmo Tolink.parsing 
+let proofs = split_cmo Tolink.proofs 
+let tactics = split_cmo Tolink.tactics 
+let toplevel = split_cmo Tolink.toplevel 
+let highparsing = split_cmo Tolink.highparsing 
 let highparsingnew = split_cmo Tolink.highparsingnew
-let ide = split_cmo Tolink.ide
+let ide = split_cmo Tolink.ide 
 
 let core_objs = 
   libobjs @ lib @ kernel @ library @ pretyping @ interp @ parsing @ 
   proofs @ tactics
 
+let core_libs = 
+  libobjs @ [ "lib.cma" ; "kernel.cma" ; "library.cma" ; "pretyping.cma" ;
+  "interp.cma" ; "parsing.cma" ; "proofs.cma" ; "tactics.cma" ]
+
 (* 3. Files only in coqsearchisos (if option -searchisos is used) *)
 let coqsearch = ["version_searchisos.cmo"; "cmd_searchisos_line.cmo"]
 
@@ -55,7 +59,8 @@ let gramobjs = []
 let notopobjs = gramobjs
 
 (* 5. High-level tactics objects *)
-let hightactics = (split_cmo Tolink.hightactics) @ (split_cmo Tolink.contrib)
+let hightactics = 
+ (split_cmo Tolink.hightactics) @ (split_cmo Tolink.contrib) 
 
 (* environment *)
 let src_coqtop = ref Coq_config.coqtop
@@ -103,18 +108,28 @@ let files_to_link userfiles =
     "str.cma"::"threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide 
   else [] 
   in
+  let ide_libs = if !coqide then 
+    ["str.cma" ; "threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ; "ide.cma" ]
+  else [] 
+  in
   let objs = 
     core_objs @ dyn_objs @ toplevel @ highparsing @ highparsingnew @ 
     command_objs @ hightactics @ toplevel_objs @ ide_objs
+  and libs =
+    core_libs @ dyn_objs @ 
+    [ "toplevel.cma" ; "highparsing.cma" ; "highparsingnew.cma" ] @ 
+    command_objs @ [ "hightactics.cma" ; "contrib.cma" ] @ toplevel_objs @ 
+    ide_libs      
   in
-  let tolink =
+  let objstolink,libstolink =
     if !opt then 
-      (List.map native_suffix objs) @ userfiles
+      ((List.map native_suffix objs) @ userfiles,
+       (List.map native_suffix libs) @ userfiles)
     else 
-      objs @ userfiles 
+      (objs @ userfiles ,libs @ userfiles )
   in
-  let modules = List.map module_of_file tolink in
-  (modules, tolink)
+  let modules = List.map module_of_file objstolink in
+  (modules, libstolink)
 
 (* Gives the list of all the directories under [dir].
    Uses [Unix] (it is hard to do without it). *)
@@ -317,7 +332,14 @@ let main () =
     let args = if !top then args @ [ "topstart.cmo" ] else args in
     (* Now, with the .cma, we MUST use the -linkall option *)
     let command = String.concat " " ((prog^" -linkall")::args) in
-    if !echo then begin print_endline command; flush Pervasives.stdout end;
+    if !echo then 
+      begin 
+	print_endline command; 
+	print_endline 
+	  ("(command length is " ^ 
+	   (string_of_int (String.length command)) ^ " characters)");
+	flush Pervasives.stdout 
+      end;
     let retcode = Sys.command command in
     clean main_file;
     (* command gives the exit code in HSB, and signal in LSB !!! *)