aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES4
-rw-r--r--INSTALL12
-rw-r--r--Makefile.build44
-rw-r--r--Makefile.dev21
-rw-r--r--configure.ml14
-rw-r--r--tools/coq_makefile.ml6
-rw-r--r--tools/coqmktop.ml13
7 files changed, 20 insertions, 94 deletions
diff --git a/CHANGES b/CHANGES
index 240d71ec0..3b4d26598 100644
--- a/CHANGES
+++ b/CHANGES
@@ -26,6 +26,10 @@ Plugins
- The mathematical proof language (also known as declarative mode) was removed.
+Dependencies
+
+- Support for camlp4 has been removed.
+
Changes from V8.6beta1 to V8.6
==============================
diff --git a/INSTALL b/INSTALL
index 9454bba4a..6b49738b8 100644
--- a/INSTALL
+++ b/INSTALL
@@ -39,8 +39,7 @@ WHAT DO YOU NEED ?
probably available in your distribution and for sure at
http://projects.camlcity.org/projects/findlib.html)
- - Camlp5 (version >= 6.02) (Coq compiles with Camlp4 but might be
- less well supported)
+ - Camlp5 (version >= 6.02)
- GNU Make version 3.81 or later
@@ -74,11 +73,10 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
bigger), you will also need the "ocamlopt" (or its native code version
"ocamlopt.opt") command.
-2- Check that you have Camlp5 (or a supported Camlp4) installed on your
- computer and that the command "camlp5" lies in a directory which
- is present in your $PATH environment variable path.
- (You need Camlp5/4 in both bytecode and native versions if
- your platform supports it).
+2- Check that you have Camlp5 installed on your computer and that the
+ command "camlp5" lies in a directory which is present in your $PATH
+ environment variable path. (You need Camlp5 in both bytecode and
+ native versions if your platform supports it).
3- The uncompression and un-tarring of the distribution file gave birth
to a directory named "coq-8.xx". You can rename this directory and put
diff --git a/Makefile.build b/Makefile.build
index eeb648ba1..56f1fb8b4 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -146,14 +146,10 @@ $(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ $(1) $(addsuffix .cm
$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
endef
-# Camlp4 / Camlp5 settings
+# Camlp5 settings
CAMLP4DEPS:=grammar/compat5.cmo grammar/grammar.cma
-ifeq ($(CAMLP4),camlp5)
CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
-else
-CAMLP4USE=-D$(CAMLVERSION)
-endif
PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo)
@@ -162,11 +158,7 @@ SYSCMA:=$(addsuffix .cma,$(SYSMOD))
SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD))
# We do not repeat the dependencies already in SYSMOD here
-ifeq ($(CAMLP4),camlp5)
P4CMA:=gramlib.cma
-else
-P4CMA:=camlp4lib.cma
-endif
###########################################################################
# Infrastructure for the rest of the Makefile
@@ -243,26 +235,6 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h
$(HIDE)$(OCAMLC) -ccopt "-MM -MQ $@ -MQ $(<:.c=.o) -isystem $(CAMLHLIB)" $< $(TOTARGET)
###########################################################################
-### Special rules (Camlp5 / Camlp4)
-###########################################################################
-
-# Special rule for the compatibility-with-camlp5 extension for camlp4
-#
-# - grammar/compat5.cmo changes 'GEXTEND' into 'EXTEND'. Safe, always loaded
-# - grammar/compat5b.cmo changes 'EXTEND' into 'EXTEND Gram'. Interact badly with
-# syntax such that 'VERNAC EXTEND', we only load it in grammar/
-
-ifeq ($(CAMLP4),camlp4)
-grammar/compat5.cmo: grammar/compat5.mlp
- $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) -impl' -impl $<
-grammar/compat5b.cmo: grammar/compat5b.mlp
- $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) -impl' -impl $<
-else
-grammar/compat5.cmo: grammar/compat5.ml
- $(OCAMLC) -c $<
-endif
-
-###########################################################################
# grammar/grammar.cma
###########################################################################
@@ -299,15 +271,9 @@ grammar/grammar.cma : $(GRAMCMO)
## Support of Camlp5 and Camlp5
-ifeq ($(CAMLP4),camlp4)
- COMPATCMO:=grammar/compat5.cmo grammar/compat5b.cmo
- GRAMP4USE:=$(COMPATCMO) -D$(CAMLVERSION)
- GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl
-else
- COMPATCMO:=
- GRAMP4USE:=$(COMPATCMO) pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
- GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl
-endif
+COMPATCMO:=
+GRAMP4USE:=$(COMPATCMO) pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
+GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl
## Rules for standard .mlp and .mli files in grammar/
@@ -597,7 +563,7 @@ plugins/%.cmx: plugins/%.ml
$(HIDE)$(OCAMLLEX) -o $@ "$*.mll"
%.ml: %.ml4 $(CAMLP4DEPS)
- $(SHOW)'CAMLP4O $<'
+ $(SHOW)'CAMLP5O $<'
$(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) \
$(CAMLP4DEPS) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@
diff --git a/Makefile.dev b/Makefile.dev
index ea6b8b919..5931e46dd 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -20,13 +20,8 @@ DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo
devel: printers
printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp4.dbg
-ifeq ($(CAMLP4),camlp5)
dev/camlp4.dbg:
echo "load_printer gramlib.cma" > $@
-else
-dev/camlp4.dbg:
- echo "load_printer camlp4lib.cma" > $@
-endif
############
# revision
@@ -199,22 +194,6 @@ ltac: $(LTACVO) $(LTACCMO)
.PHONY: omega micromega setoid_ring nsatz extraction
.PHONY: fourier funind cc rtauto btauto ltac
-#################################
-### Misc other development rules
-#################################
-
-# NOTA : otags only accepts camlp4 as preprocessor, so the following rule
-# won't build tags of .ml4 when compiling with camlp5
-
-otags:
- otags $(MLIFILES) $(filter-out configure.ml, $(MLSTATICFILES)) \
- $(if $(filter camlp5,$(CAMLP4)), , \
- -pa op -pa g -pa m -pa rq $(addprefix -pa , $(CAMLP4DEPS)) \
- $(addprefix -impl , $(ML4FILES)))
-
-.PHONY: otags
-
-
# For emacs:
# Local Variables:
# mode: makefile
diff --git a/configure.ml b/configure.ml
index cc63fde70..befd67262 100644
--- a/configure.ml
+++ b/configure.ml
@@ -251,7 +251,6 @@ module Prefs = struct
let coqdocdir = ref (None : string option)
let ocamlfindcmd = ref (None : string option)
let lablgtkdir = ref (None : string option)
- let usecamlp5 = ref true
let camlp5dir = ref (None : string option)
let arch = ref (None : string option)
let natdynlink = ref true
@@ -311,9 +310,9 @@ let args_options = Arg.align [
"-lablgtkdir", arg_string_option Prefs.lablgtkdir,
"<dir> Specifies the path to the Lablgtk library";
"-usecamlp5", Arg.Unit (fun () -> ()),
- " Deprecated";
+ "Deprecated";
"-camlp5dir",
- Arg.String (fun s -> Prefs.usecamlp5:=true; Prefs.camlp5dir:=Some s),
+ Arg.String (fun s -> Prefs.camlp5dir:=Some s),
"<dir> Specifies where is the Camlp5 library and tells to use it";
"-arch", arg_string_option Prefs.arch,
"<arch> Specifies the architecture";
@@ -538,8 +537,6 @@ let which_camlpX base =
(* TODO: camlp5dir should rather be the *binary* location, just as camldir *)
(* TODO: remove the late attempts at finding gramlib.cma *)
-exception NoCamlp5
-
let check_camlp5 testcma = match !Prefs.camlp5dir with
| Some dir ->
if Sys.file_exists (dir/testcma) then
@@ -558,8 +555,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with
let dir,_ = tryrun camlp5o ["-where"] in
dir, camlp5o
with Not_found ->
- let () = printf "No Camlp5 installation found." in
- raise NoCamlp5
+ die "No Camlp5 installation found."
let check_camlp5_version camlp5o =
let version_line, _ = run ~err:StdOut camlp5o ["-v"] in
@@ -570,14 +566,10 @@ let check_camlp5_version camlp5o =
| _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n"
let config_camlpX () =
- try
- if not !Prefs.usecamlp5 then raise NoCamlp5;
let camlp5mod = "gramlib" in
let camlp5libdir, camlp5o = check_camlp5 (camlp5mod^".cma") in
let camlp5_version = check_camlp5_version camlp5o in
"camlp5", camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version
- with NoCamlp5 ->
- die "No Camlp5 installation found.\n"
let camlpX, camlpXo, camlpXbindir, fullcamlpXlibdir, camlpXmod, camlpX_version = config_camlpX ()
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 22b1408c0..ed89bda2c 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -528,11 +528,7 @@ let variables is_install opt (args,defs) =
print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n";
print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n";
print "GRAMMARS?=grammar.cma\n";
- print "ifeq ($(CAMLP4),camlp5)
-CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
-else
-CAMLP4EXTEND=
-endif\n";
+ print "CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo\n";
print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\
$(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
end;
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index 645b3665e..7fa8fd58d 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -62,8 +62,6 @@ let echo = ref false
let no_start = ref false
let is_ocaml4 = Coq_config.caml_version.[0] <> '3'
-let is_camlp5 = Coq_config.camlp4 = "camlp5"
-
(** {6 Includes options} *)
@@ -106,7 +104,7 @@ let incl_all_subdirs dir opts =
(** OCaml + CamlpX libraries *)
let ocaml_libs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"]
-let camlp4_libs = if is_camlp5 then ["gramlib.cma"] else ["camlp4lib.cma"]
+let camlp4_libs = ["gramlib.cma"]
let libobjs = ocaml_libs @ camlp4_libs
(** Toplevel objects *)
@@ -117,14 +115,7 @@ let ocaml_topobjs =
else
["toplevellib.cma"]
-let camlp4_topobjs =
- if is_camlp5 then
- ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"]
- else
- [ "Camlp4Top.cmo";
- "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
- "Camlp4Parsers/Camlp4OCamlParser.cmo";
- "Camlp4Parsers/Camlp4GrammarParser.cmo" ]
+let camlp4_topobjs = ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"]
let topobjs = ocaml_topobjs @ camlp4_topobjs
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 12:06:26 +0000