From 77e22783cf3dac95ea9f122b84e011bf348c9893 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 17 Feb 2009 00:05:53 +0000
Subject: Made hack to have Drop and #use"include" working with ocaml 3.10
 public

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11929 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/doc/debugging.txt                  | 15 +++++++++++++--
 dev/doc/patch.ocaml-3.10.drop.rectypes | 29 +++++++++++++++++++++++++++++
 2 files changed, 42 insertions(+), 2 deletions(-)
 create mode 100644 dev/doc/patch.ocaml-3.10.drop.rectypes

(limited to 'dev')

diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index e5c831396d..6e9f817f9e 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -3,9 +3,11 @@ Debugging from Coq toplevel using Caml trace mechanism
 
   1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte)
   2. Access Ocaml toplevel using vernacular command 'Drop.'
+  2.5 If with ocaml >= 3.11, use #rectypes to activate the option rectypes 
+     in the toplevel
   3. Install load paths and pretty printers for terms, idents, ... using
-     Ocaml command '#use "base_include";;' (use '#use "include";;' for a rawer
-     term pretty printer)
+     Ocaml command '#use "base_include";;' (use '#use "include";;' for 
+     installing the advanced term pretty printers)
   4. Use #trace to tell which function(s) to trace
   5. Go back to Coq toplevel with 'go();;'
   6. Test your Coq command and observe the result of tracing your functions
@@ -15,6 +17,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
 ============================
 
diff --git a/dev/doc/patch.ocaml-3.10.drop.rectypes b/dev/doc/patch.ocaml-3.10.drop.rectypes
new file mode 100644
index 0000000000..fd804b728c
--- /dev/null
+++ b/dev/doc/patch.ocaml-3.10.drop.rectypes
@@ -0,0 +1,29 @@
+Index: scripts/coqmktop.ml
+===================================================================
+--- scripts/coqmktop.ml	(révision 11904)
++++ scripts/coqmktop.ml	(copie de travail)
+@@ -235,11 +235,23 @@
+      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.11\"
++       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=Topdirs.dir_load ppf;
+         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 (); Toploop.loop ppf) };;\n"
+ 
+ (* create a temporary main file to link *)
+ let create_tmp_main_file modules =
-- 
cgit v1.2.3