aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.build23
-rw-r--r--_tags4
-rwxr-xr-xconfigure2
-rw-r--r--dev/doc/debugging.txt9
-rw-r--r--dev/doc/patch.ocaml-3.10.drop.rectypes31
-rw-r--r--myocamlbuild.ml5
-rw-r--r--scripts/coqmktop.ml15
-rw-r--r--tools/coq_makefile.ml16
8 files changed, 69 insertions, 36 deletions
diff --git a/Makefile.build b/Makefile.build
index 24f024df4..2f0a398f3 100644
--- a/Makefile.build
+++ b/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
diff --git a/_tags b/_tags
index f998dd76f..8404c91cd 100644
--- a/_tags
+++ b/_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
diff --git a/configure b/configure
index cb00667ac..c799254ad 100755
--- a/configure
+++ b/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
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index 83512c658..2480b8edb 100644
--- a/dev/doc/debugging.txt
+++ b/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
============================
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 000000000..ba7a3e950
--- /dev/null
+++ b/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 =
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index b08e54673..42ac31763 100644
--- a/myocamlbuild.ml
+++ b/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"]
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 99fa8f6eb..6f05683dd 100644
--- a/scripts/coqmktop.ml
+++ b/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;
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index c3261c1a7..060bd3d37 100644
--- a/tools/coq_makefile.ml
+++ b/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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 11:48:06 +0000