Revert "remove -rectypes except for term.ml"

Preparing landing of the native compiler, which requires -rectypes flag.

This reverts commit f975575.



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

Makefile.build

@@ -675,12 +675,12 @@ install-latex:
 source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
 
 $(OCAMLDOCDIR)/coq.tex:: $(DOCMLIS:.mli=.cmi)
-	$(OCAMLDOC) -latex -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+	$(OCAMLDOC) -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
 	$(DOCMLIS) -t "Coq mlis documentation" \
 	-intro $(OCAMLDOCDIR)/docintro -o $@
 
 mli-doc:: $(DOCMLIS:.mli=.cmi)
-	$(OCAMLDOC) -html -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+	$(OCAMLDOC) -html -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
 	$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
 	-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
 	-css-style style.css
@@ -693,9 +693,9 @@ ml-dot:: $(MLEXTRAFILES)
 	$(DOT) -Tpng $< -o $@
 
 %_types.dot: %.mli
-	$(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< 
 
-OCAMLDOC_MLLIBD = $(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
+OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
   $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib))))
 
 %.dot: | %.mllib.d
@@ -714,7 +714,7 @@ tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d
 	$(OCAMLDOC_MLLIBD)
 
 %.dot: %.mli
-	$(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $<
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< 
 
 $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
 	(cd $(OCAMLDOCDIR) ; pdflatex $*.tex && pdflatex $*.tex)
@@ -746,19 +746,6 @@ ide/coqide_main_opt.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
 	$(SHOW)'CAMLP4O   $<'
 	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -D$(IDEOPTINT) -impl $< -o $@
 
-# Specific rule for term.ml which uses -rectypes
-# Since term.mli doesn't need -rectypes, this doesn't impact the other ml files
-
-TERM:=kernel/term
-
-$(TERM).cmo: $(TERM).ml | $(TERM).ml.d
-	$(SHOW)'OCAMLC -rectypes $<'
-	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -rectypes -c $<
-
-$(TERM).cmx: $(TERM).ml | $(TERM).ml.d
-	$(SHOW)'OCAMLOPT -rectypes $<'
-	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -intf-suffix .cmi -rectypes -c $<
-
 # pretty printing of the revision number when compiling a checked out
 # source tree
 .PHONY: revision

_tags

@@ -22,10 +22,6 @@
 
 <grammar/grammar.{cma,cmxa}> : use_unix
 
-## tags for ml files
-
-"kernel/term.ml": rectypes
-
 ## tags for camlp4 files 
 
 "toplevel/whelp.ml4": use_grammar

configure

@@ -1142,7 +1142,7 @@ CAMLLINK="$bytecamlc"
 CAMLOPTLINK="$nativecamlc"
 
 # Caml flags
-CAMLFLAGS=$coq_annotate_flag
+CAMLFLAGS=-rectypes $coq_annotate_flag
 TYPEREX=$coq_typerex_wrapper
 
 # Compilation debug flags

dev/doc/debugging.txt

@@ -21,6 +21,15 @@ Debugging from Coq toplevel using Caml trace mechanism
   notations, ...), use "Set Printing All". It will affect the #trace
   printers too.
 
+Note for Ocaml 3.10.x: Ocaml 3.10.x requires that modules compiled
+with -rectypes are loaded in an environment with -rectypes set but
+there is no way to tell the toplevel to support -rectypes. To make it
+works, use "patch -p0 < dev/doc/patch.ocaml-3.10.drop.rectypes" to
+hack script/coqmktop.ml, then recompile coqtop.byte. The procedure
+above then works as soon as coqtop.byte is called with at least one
+argument (add neutral option -byte to ensure at least one argument).
+
+
 Debugging from Caml debugger
 ============================
 

dev/doc/patch.ocaml-3.10.drop.rectypes

@@ -0,0 +1,31 @@
+Index: scripts/coqmktop.ml
+===================================================================
+--- scripts/coqmktop.ml	(révision 12084)
++++ scripts/coqmktop.ml	(copie de travail)
+@@ -231,12 +231,25 @@
+      end;;
+
+      let ppf = Format.std_formatter;;
++     let set_rectypes_hack () =
++       if String.length (Sys.ocaml_version) >= 4 &
++          String.sub (Sys.ocaml_version) 0 4 = \"3.10\"
++       then
++         (* ocaml 3.10 does not have #rectypes but needs it *)
++         (* simulate a call with option -rectypes before *)
++         (* jumping to the ocaml toplevel *)
++         for i = 1 to Array.length Sys.argv - 1 do
++           Sys.argv.(i) <- \"-rectypes\"
++         done
++       else
++         () in
++
+      Mltop.set_top
+        {Mltop.load_obj=
+          (fun f -> if not (Topdirs.load_file ppf f) then failwith \"error\");
+         Mltop.use_file=Topdirs.dir_use ppf;
+         Mltop.add_dir=Topdirs.dir_directory;
+-        Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n"
++        Mltop.ml_loop=(fun () -> set_rectypes_hack(); Topmain.main()) };;\n"
+
+ (* create a temporary main file to link *)
+ let create_tmp_main_file modules =

myocamlbuild.ml

@@ -302,9 +302,8 @@ let extra_rules () = begin
 (** All caml files are compiled with +camlp4/5
     and ide files need +lablgtk2 *)
 
-  flag ["compile"; "ocaml"; "rectypes" ] (A "-rectypes");
-  flag ["compile"; "ocaml"] camlp4incl;
-  flag ["link"; "ocaml"] camlp4incl;
+  flag ["compile"; "ocaml"] (S [A"-rectypes"; camlp4incl]);
+  flag ["link"; "ocaml"] (S [A"-rectypes"; camlp4incl]);
   flag ["ocaml"; "ide"; "compile"] lablgtkincl;
   flag ["ocaml"; "ide"; "link"] lablgtkincl;
   flag ["ocaml"; "ide"; "link"; "byte"]

scripts/coqmktop.ml

@@ -221,7 +221,18 @@ let tmp_dynlink()=
 let declare_loading_string () =
   if not !top then
     "Mltop.remove ();;"
-  else "let ppf = Format.std_formatter;;\
+  else
+    "begin try\
+\n       (* Enable rectypes in the toplevel if it has the directive #rectypes *)\
+\n       begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\
+\n         | Toploop.Directive_none f -> f ()\
+\n         | _ -> ()\
+\n       end\
+\n     with\
+\n       | Not_found -> ()\
+\n     end;;\
+\n\
+\n     let ppf = Format.std_formatter;;\
 \n     Mltop.set_top\
 \n       {Mltop.load_obj=\
 \n         (fun f -> if not (Topdirs.load_file ppf f) then Errors.error (\"Could not load plugin \"^f));\
@@ -288,7 +299,7 @@ let main () =
     (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
     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::args) in
+    let command = String.concat " " (prog::"-rectypes"::args) in
       if !echo then
 	begin
 	  print_endline command;

tools/coq_makefile.ml

@@ -409,12 +409,12 @@ let variables is_install opt (args,defs) =
   -I \"$(COQLIB)proofs\" -I \"$(COQLIB)tactics\" -I \"$(COQLIB)tools\" \\
   -I \"$(COQLIB)toplevel\" -I \"$(COQLIB)grammar\"";
     List.iter (fun c -> print " \\
-  -I \"$(COQLIB)\""; print c) Coq_config.plugins_dirs; print "\n";
-    print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I \"$(CAMLP4LIB)\"\n\n";
-    print "CAMLC?=$(OCAMLC) -c\n";
-    print "CAMLOPTC?=$(OCAMLOPT) -c\n";
-    print "CAMLLINK?=$(OCAMLC)\n";
-    print "CAMLOPTLINK?=$(OCAMLOPT)\n";
+  -I $(COQLIB)/"; print c) Coq_config.plugins_dirs; print "\n";
+    print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
+    print "CAMLC?=$(OCAMLC) -c -rectypes\n";
+    print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes\n";
+    print "CAMLLINK?=$(OCAMLC) -rectypes\n";
+    print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes\n";
     print "GRAMMARS?=grammar.cma\n";
     print "ifeq ($(CAMLP4),camlp5)
 CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
@@ -610,9 +610,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
     begin
       print "mlihtml: $(MLIFILES:.mli=.cmi)\n";
       print "\t mkdir $@ || rm -rf $@/*\n";
-      print "\t$(OCAMLDOC) -html -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+      print "\t$(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
       print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n";
-      print "\t$(OCAMLDOC) -latex -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+      print "\t$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
     end;
   if !some_vfile then
     begin