From 633e40b6f925556e94347c348a2804cdc1068d88 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 8 Mar 2017 14:26:00 +0100 Subject: [camlpX] Enrico's changes to camlp4 removal. This removes some remaining support for camlp4 in the infrastructure and documents the change. --- CHANGES | 4 ++++ INSTALL | 12 +++++------- Makefile.build | 44 +++++--------------------------------------- Makefile.dev | 21 --------------------- configure.ml | 14 +++----------- tools/coq_makefile.ml | 6 +----- tools/coqmktop.ml | 13 ++----------- 7 files changed, 20 insertions(+), 94 deletions(-) diff --git a/CHANGES b/CHANGES index 240d71ec04..3b4d265988 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 9454bba4ab..6b49738b83 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 eeb648ba1e..56f1fb8b49 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 @@ -242,26 +234,6 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h $(SHOW)'CCDEP $<' $(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 ea6b8b9194..5931e46dd0 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 cc63fde702..befd67262c 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, " 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), " Specifies where is the Camlp5 library and tells to use it"; "-arch", arg_string_option Prefs.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 22b1408c0b..ed89bda2cf 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 645b3665e0..7fa8fd58db 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 -- cgit v1.2.3