From aa151dbc7aa501bac78b835a80f9a25c5316d2dc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 8 Nov 2018 03:11:06 +0100 Subject: [PATCH] [camlp5] Remove dependency on camlp5. --- .gitlab-ci.yml | 2 +- .merlin.in | 2 +- .travis.yml | 5 +- CHANGES.md | 19 ++- INSTALL | 24 +-- META.coq.in | 14 +- Makefile | 1 - Makefile.build | 73 +-------- Makefile.common | 2 - Makefile.ide | 4 +- checker/include | 1 - config/coq_config.mli | 5 - configure.ml | 118 +-------------- coq.opam | 1 - default.nix | 2 +- dev/base_include | 3 +- dev/build/windows/makecoq_mingw.sh | 4 +- dev/ci/README.md | 8 +- dev/ci/appveyor.sh | 2 +- dev/ci/docker/bionic_coq/Dockerfile | 14 +- dev/doc/README.md | 1 - dev/doc/changes.md | 10 ++ dev/ocamldebug-coq.run | 3 +- gramlib/gramlib.mllib | 4 + grammar/argextend.mlp | 221 ---------------------------- grammar/dune | 41 ------ grammar/q_util.mli | 54 ------- grammar/q_util.mlp | 150 ------------------- grammar/tacextend.mlp | 72 --------- grammar/vernacextend.mlp | 115 --------------- lib/envars.ml | 4 - tools/CoqMakefile.in | 22 +-- 32 files changed, 64 insertions(+), 937 deletions(-) create mode 100644 gramlib/gramlib.mllib delete mode 100644 grammar/argextend.mlp delete mode 100644 grammar/dune delete mode 100644 grammar/q_util.mli delete mode 100644 grammar/q_util.mlp delete mode 100644 grammar/tacextend.mlp delete mode 100644 grammar/vernacextend.mlp diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ea7eccb47f79..0ebac839fc9e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-10-30-V1" + CACHEKEY: "bionic_coq-V2018-11-08-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/.merlin.in b/.merlin.in index eade4d19f97e..db7259dd6f7e 100644 --- a/.merlin.in +++ b/.merlin.in @@ -53,4 +53,4 @@ B dev S plugins/** B plugins/** -PKG threads.posix camlp5 +PKG threads.posix diff --git a/.travis.yml b/.travis.yml index 6f625b1c75bf..02b94f4a8ec6 100644 --- a/.travis.yml +++ b/.travis.yml @@ -20,7 +20,6 @@ env: - NJOBS=2 - COMPILER="4.07.0" - DUNE_VER=".1.2.1" - - CAMLP5_VER=".7.06" - FINDLIB_VER=".1.8.0" - LABLGTK="lablgtk.2.18.6 conf-gtksourceview.2" - NATIVE_COMP="yes" @@ -56,7 +55,7 @@ matrix: - opam switch "$COMPILER" && opam update - eval $(opam config env) - opam config list - - opam install -j "$NJOBS" -y num ocamlfind${FINDLIB_VER} dune${DUNE_VER} camlp5${CAMLP5_VER} ${EXTRA_OPAM} + - opam install -j "$NJOBS" -y num ocamlfind${FINDLIB_VER} dune${DUNE_VER} ${EXTRA_OPAM} - opam list - if: NOT (type = pull_request) @@ -81,7 +80,7 @@ matrix: - opam switch "$COMPILER" && opam update - eval $(opam config env) - opam config list - - opam install -j "$NJOBS" -y num ocamlfind${FINDLIB_VER} dune${DUNE_VER} camlp5${CAMLP5_VER} ${EXTRA_OPAM} + - opam install -j "$NJOBS" -y num ocamlfind${FINDLIB_VER} dune${DUNE_VER} ${EXTRA_OPAM} - opam list before_deploy: - dev/build/osx/make-macos-dmg.sh diff --git a/CHANGES.md b/CHANGES.md index 9a38b18a258c..6bdb63d4d750 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,20 @@ Changes from 8.9 to 8.10 ======================== +OCaml and dependencies + +- Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the + INSTALL file for more information on dependencies. + +- Coq 8.10 doesn't need Camlp5 to build anymore. It now includes a + fork of the core parsing library that Coq uses, which is a small + subset of the whole Camlp5 distribution. In particular, this subset + doesn't depend on the OCaml AST, allowing easier compilation and + testing on experimental OCaml versions. + + The Coq developers would like to thank Daniel de Rauglaudre for many + years of continued support. + Coqide - CoqIDE now properly sets the module name for a given file based on @@ -13,11 +27,6 @@ Coqtop proper -R/-Q options. For example, given -R Foo foolib using -topfile foolib/bar.v will set the module name to Foo.Bar. -OCaml - -- Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the - INSTALL file for more information on dependencies. - Specification language, type inference - Fixing a missing check in interpreting instances of existential diff --git a/INSTALL b/INSTALL index 6201bc961043..8d8efd4d4df8 100644 --- a/INSTALL +++ b/INSTALL @@ -39,9 +39,6 @@ WHAT DO YOU NEED ? - Findlib (version >= 1.4.1) (available at http://projects.camlcity.org/projects/findlib.html) - - Camlp5 (version >= 7.03) - (available at https://camlp5.github.io/) - - GNU Make version 3.81 or later - a C compiler @@ -49,14 +46,14 @@ WHAT DO YOU NEED ? - for CoqIDE, the lablgtk development files (version >= 2.18.5), and the GTK 2.x libraries including gtksourceview2. - Note that num, camlp5 and lablgtk should be properly registered with + Note that num and lablgtk should be properly registered with findlib/ocamlfind as Coq's makefile will use it to locate the libraries during the build. Opam (https://opam.ocaml.org/) is recommended to install OCaml and the corresponding packages. - $ opam install num ocamlfind camlp5 lablgtk conf-gtksourceview + $ opam install num ocamlfind lablgtk conf-gtksourceview should get you a reasonable OCaml environment to compile Coq. @@ -96,19 +93,14 @@ 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 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 +2- 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 it wherever you want. Just keep in mind that you will need some spare space during the compilation (reckon on about 300 Mb of disk space for the whole system in native-code compilation). Once installed, the binaries take about 30 Mb, and the library about 200 Mb. -4- First you need to configure the system. It is done automatically with +3- First you need to configure the system. It is done automatically with the command: ./configure @@ -171,7 +163,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). c.f. https://caml.inria.fr/mantis/view.php?id=7630 -5- Still in the root directory, do +4- Still in the root directory, do make @@ -183,7 +175,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). it is recommended to compile in parallel, via make -jN where N is your number of cores. -6- You can now install the Coq system. Executables, libraries, manual pages +5- You can now install the Coq system. Executables, libraries, manual pages and emacs mode are copied in some standard places of your system, defined at configuration time (step 3). Just do @@ -192,7 +184,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). Of course, you may need superuser rights to do that. -7- Optionally, you could build the bytecode version of Coq via: +6- Optionally, you could build the bytecode version of Coq via: make byte @@ -204,7 +196,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml toplevel accessible via the Drop command. -8- You can now clean all the sources. (You can even erase them.) +7- You can now clean all the sources. (You can even erase them.) make clean diff --git a/META.coq.in b/META.coq.in index bca37ea74b23..181887bc3d0b 100644 --- a/META.coq.in +++ b/META.coq.in @@ -6,18 +6,6 @@ version = "8.10" directory = "" requires = "" -package "grammar" ( - - description = "Coq Camlp5 Grammar Extensions for Plugins" - version = "8.10" - - requires = "camlp5.gramlib" - directory = "grammar" - - archive(byte) = "grammar.cma" - archive(native) = "grammar.cmxa" -) - package "config" ( description = "Coq Configuration Variables" @@ -155,7 +143,7 @@ package "proofs" ( package "gramlib" ( - description = "Coq Parsing Library" + description = "Coq Grammar Engine" version = "8.10" requires = "" diff --git a/Makefile b/Makefile index 023578f94aa2..330562afb667 100644 --- a/Makefile +++ b/Makefile @@ -125,7 +125,6 @@ help: @echo " make clean" @echo "or make archclean" @echo "For make to be verbose, add VERBOSE=1" - @echo "If you want camlp5 to generate human-readable files, add READABLE_ML4=1" @echo @echo "Bytecode compilation is now a separate target:" @echo " make byte" diff --git a/Makefile.build b/Makefile.build index dedd36cef21d..fb5442d4be46 100644 --- a/Makefile.build +++ b/Makefile.build @@ -22,10 +22,6 @@ # set this variable to 1 (or any non-empty value): VERBOSE ?= -# If set to 1 (or non-empty) then *.ml files corresponding to *.ml4 files -# will be generated in a human-readable format rather than in a binary format. -READABLE_ML4 ?= - # When non-empty, a time command is performed at each .v compilation. # To collect compilation timings of .v and import them in a spreadsheet, # you could hence consider: make TIMED=1 2> timings.csv @@ -199,7 +195,7 @@ COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS)) -MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP5LIB) +MLINCLUDES=$(LOCALINCLUDES) OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) @@ -253,14 +249,6 @@ define ocamlbyte $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^ endef -# Camlp5 settings - -CAMLP5DEPS:=grammar/grammar.cma -CAMLP5USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) - -PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) -# XXX unused but should be used for mlp files - # Main packages linked by Coq. SYSMOD:=-package num,str,unix,dynlink,threads @@ -333,70 +321,15 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h kernel/make_opcodes.sh kernel/ $(SHOW)'CCDEP $<' $(HIDE)$(OCAMLC) -ccopt "-MM -MQ $@ -MQ $(<:.c=.o) -isystem $(CAMLHLIB)" $< $(TOTARGET) -########################################################################### -# grammar/grammar.cma -########################################################################### - -## In this part, we compile grammar/grammar.cma -## without relying on .d dependency files, for bootstraping the creation -## and inclusion of these .d files - -## Explicit dependencies for grammar stuff - -GRAMBASEDEPS := grammar/q_util.cmi -GRAMCMO := grammar/q_util.cmo \ - grammar/argextend.cmo grammar/tacextend.cmo grammar/vernacextend.cmo COQPPCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex)) -grammar/argextend.cmo : $(GRAMBASEDEPS) -grammar/q_util.cmo : $(GRAMBASEDEPS) -grammar/tacextend.cmo : $(GRAMBASEDEPS) grammar/argextend.cmo -grammar/vernacextend.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo \ - grammar/argextend.cmo - coqpp/coqpp_parse.cmi: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmi coqpp/coqpp_lex.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmo -## Ocaml compiler with the right options and -I for grammar - -GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \ - -I $(MYCAMLP5LIB) -I grammar - -## Specific rules for grammar.cma - -grammar/grammar.cma : $(GRAMCMO) - $(SHOW)'Testing $@' - @touch grammar/test.mlp - $(HIDE)$(GRAMC) -pp '$(CAMLP5O) $^ -impl' -impl grammar/test.mlp -o grammar/test - @rm -f grammar/test.* grammar/test - $(SHOW)'OCAMLC -a $@' - $(HIDE)$(GRAMC) $^ -linkall -a -o $@ - $(COQPP): $(COQPPCMO) coqpp/coqpp_main.ml $(SHOW)'OCAMLC -a $@' - $(HIDE)$(GRAMC) -I coqpp $^ -linkall -o $@ - -## Support of Camlp5 and Camlp5 - -COMPATCMO:= -GRAMP4USE:=$(COMPATCMO) pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) -GRAMPP:=$(CAMLP5O) -I $(MYCAMLP5LIB) $(GRAMP4USE) $(CAMLP5COMPAT) -impl - -## Rules for standard .mlp and .mli files in grammar/ - -grammar/%.cmo: grammar/%.mlp | $(COMPATCMO) - $(SHOW)'OCAMLC -c -pp $<' - $(HIDE)$(GRAMC) -c -pp '$(GRAMPP)' -impl $< - -grammar/%.cmo: grammar/%.ml | $(COMPATCMO) - $(SHOW)'OCAMLC -c -pp $<' - $(HIDE)$(GRAMC) -c $< - -grammar/%.cmi: grammar/%.mli - $(SHOW)'OCAMLC -c $<' - $(HIDE)$(GRAMC) -c $< - + $(HIDE)$(OCAMLC) -I coqpp $^ -linkall -o $@ ########################################################################### # Main targets (coqtop.opt, coqtop.byte) @@ -404,7 +337,7 @@ grammar/%.cmi: grammar/%.mli .PHONY: coqbinaries coqbyte -coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) $(GRAMMARCMA) +coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) coqbyte: $(TOPBYTE) $(CHICKENBYTE) # Special rule for coqtop, we imitate `ocamlopt` can delete the target diff --git a/Makefile.common b/Makefile.common index dd91f89ffbef..ca2cb8fee697 100644 --- a/Makefile.common +++ b/Makefile.common @@ -123,8 +123,6 @@ CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/l parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ stm/stm.cma toplevel/toplevel.cma -GRAMMARCMA:=grammar/grammar.cma - ########################################################################### # plugins object files ########################################################################### diff --git a/Makefile.ide b/Makefile.ide index 39af1f854558..cae77ee348e6 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -147,7 +147,7 @@ $(IDETOPEXE): $(IDETOP:.opt=.$(BEST)) $(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \ - $(SYSMOD) -package camlp5.gramlib \ + $(SYSMOD) \ $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@ $(STRIP_HIDE) $@ $(CODESIGN_HIDE) $@ @@ -156,7 +156,7 @@ $(IDETOPBYTE): ide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \ -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \ - $(SYSMOD) -package camlp5.gramlib \ + $(SYSMOD) \ $(LINKCMO) $(IDETOPCMA) $(BYTEFLAGS) $< -o $@ #################### diff --git a/checker/include b/checker/include index da0346359b21..3ffc301724b6 100644 --- a/checker/include +++ b/checker/include @@ -13,7 +13,6 @@ #directory "kernel";; #directory "checker";; #directory "+threads";; -#directory "+camlp5";; #load "unix.cma";; #load"threads.cma";; diff --git a/config/coq_config.mli b/config/coq_config.mli index 22d8c49fd19d..33acceb1f02f 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -25,11 +25,6 @@ val docdirsuffix : string (* doc directory relative to installation prefix *) val ocamlfind : string -val camlp5o : string (* name of the camlp5o executable *) -val camlp5bin : string (* base directory for camlp5 binaries *) -val camlp5lib : string (* where is the library of camlp5 *) -val camlp5compat : string (* compatibility argument to camlp5 *) - val caml_flags : string (* arguments passed to ocamlc (ie. CAMLFLAGS) *) val arch : string (* architecture *) diff --git a/configure.ml b/configure.ml index 714efd1eb12d..ec765acc150b 100644 --- a/configure.ml +++ b/configure.ml @@ -4,6 +4,7 @@ (**********************************) + (** This file should be run via: ocaml configure.ml You could also use our wrapper ./configure *) @@ -188,34 +189,6 @@ let which prog = let program_in_path prog = try let _ = which prog in true with Not_found -> false -(** Choose a command among a list of candidates - (command name, mandatory arguments, arguments for this test). - Chooses the first one whose execution outputs a non-empty (first) line. - Dies with message [msg] if none is found. *) - -let select_command msg candidates = - let rec search = function - | [] -> die msg - | (p, x, y) :: tl -> - if fst (tryrun p (x @ y)) <> "" - then List.fold_left (Printf.sprintf "%s %s") p x - else search tl - in search candidates - -(** As per bug #4828, ocamlfind on Windows/Cygwin barfs if you pass it - a quoted path to camlp5o via -pp. So we only quote camlp5o on not - Windows, and warn on Windows if the path contains spaces *) -let contains_suspicious_characters str = - List.fold_left (fun b ch -> String.contains str ch || b) false [' '; '\t'] - -let win_aware_quote_executable str = - if not (os_type_win32 || os_type_cygwin) then - sprintf "%S" str - else - let _ = if contains_suspicious_characters str then - warn "The string %S contains suspicious characters; ocamlfind might fail" str in - Str.global_replace (Str.regexp "\\\\") "/" str - (** * Date *) (** The short one is displayed when starting coqtop, @@ -254,7 +227,6 @@ type preferences = { coqdocdir : string option; ocamlfindcmd : string option; lablgtkdir : string option; - camlp5dir : string option; arch : string option; natdynlink : bool; coqide : ide option; @@ -292,7 +264,6 @@ let default = { coqdocdir = None; ocamlfindcmd = None; lablgtkdir = None; - camlp5dir = None; arch = None; natdynlink = true; coqide = None; @@ -399,8 +370,6 @@ let args_options = Arg.align [ " Specifies the ocamlfind command to use"; "-lablgtkdir", arg_string_option (fun p lablgtkdir -> { p with lablgtkdir }), " Specifies the path to the Lablgtk library"; - "-camlp5dir", arg_string_option (fun p camlp5dir -> { p with camlp5dir }), - " Specifies where is the Camlp5 library and tells to use it"; "-flambda-opts", arg_string_list ' ' (fun p flambda_flags -> { p with flambda_flags }), " Specifies additional flags to be passed to the flambda optimizing compiler"; "-arch", arg_string_option (fun p arch -> { p with arch }), @@ -580,8 +549,6 @@ let camlbin, caml_version, camllib, findlib_version = then reset_caml_top camlexec (camlbin / "ocaml") in camlbin, caml_version, camllib, findlib_version -let camlp5compat = "-loc loc" - (** Caml version as a list of string, e.g. ["4";"00";"1"] *) let caml_version_list = numeric_prefix_list caml_version @@ -660,76 +627,12 @@ let caml_flags = let coq_caml_flags = coq_warn_error -(** * Camlp5 configuration *) - -(* Convention: we use camldir as a prioritary location for camlp5, if given *) -(* i.e., in the case of camlp5, we search for a copy of camlp5o which *) -(* answers the right camlp5 lib dir *) - -let strip_slash dir = - let n = String.length dir in - if n>0 && dir.[n - 1] = '/' then String.sub dir 0 (n-1) else dir - -let which_camlp5o_for camlp5lib = - let camlp5o = Filename.concat camlbin "camlp5o" in - let camlp5lib = strip_slash camlp5lib in - if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else - let camlp5o = which "camlp5o" in - if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else - die ("Error: cannot find Camlp5 binaries corresponding to Camlp5 library " ^ camlp5lib) - -let which_camlp5 base = - let file = Filename.concat camlbin base in - if is_executable file then file else which base - -(* TODO: camlp5dir should rather be the *binary* location, just as camldir *) -(* TODO: remove the late attempts at finding gramlib.cma *) - -let check_camlp5 testcma = match !prefs.camlp5dir with - | Some dir -> - if Sys.file_exists (dir/testcma) then - let camlp5o = - try which_camlp5o_for dir - with Not_found -> die "Error: cannot find Camlp5 binaries in path.\n" in - dir, camlp5o - else - let msg = - sprintf "Cannot find camlp5 libraries in '%s' (%s not found)." - dir testcma - in die msg - | None -> - try - let camlp5o = which_camlp5 "camlp5o" in - let dir,_ = tryrun camlp5o ["-where"] in - dir, camlp5o - with Not_found -> - die "No Camlp5 installation found." - -let check_camlp5_version camlp5o = - let version_line, _ = run ~err:StdOut camlp5o ["-v"] in - let version = List.nth (string_split ' ' version_line) 2 in - match numeric_prefix_list version with - | major::minor::_ when s2i major > 6 || (s2i major, s2i minor) >= (6,6) -> - cprintf "You have Camlp5 %s. Good!" version; version - | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n" - -let config_camlp5 () = - let camlp5mod = "gramlib" in - let camlp5libdir, camlp5o = check_camlp5 (camlp5mod^".cma") in - let camlp5_version = check_camlp5_version camlp5o in - camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version - -let camlp5o, camlp5bindir, fullcamlp5libdir, - camlp5mod, camlp5_version = config_camlp5 () - let shorten_camllib s = if starts_with s (camllib^"/") then let l = String.length camllib + 1 in "+" ^ String.sub s l (String.length s - l) else s -let camlp5libdir = shorten_camllib fullcamlp5libdir - (** * Native compiler *) let msg_byteonly = @@ -738,9 +641,6 @@ let msg_byteonly = let msg_no_ocamlopt () = warn "Cannot find the OCaml native-code compiler.\n%s" msg_byteonly -let msg_no_camlp5_cmxa () = - warn "Cannot find the native-code library of camlp5.\n%s" msg_byteonly - let msg_no_dynlink_cmxa () = warn "Cannot find native-code dynlink library.\n%s" msg_byteonly; cprintf "For building a native-code Coq, you may try to first"; @@ -751,8 +651,6 @@ let check_native () = let () = if !prefs.byteonly then raise Not_found in let version, _ = tryrun camlexec.find ["opt";"-version"] in if version = "" then let () = msg_no_ocamlopt () in raise Not_found - else if not (Sys.file_exists (fullcamlp5libdir/camlp5mod^".cmxa")) - then let () = msg_no_camlp5_cmxa () in raise Not_found else if fst (tryrun camlexec.find ["query";"dynlink"]) = "" then let () = msg_no_dynlink_cmxa () in raise Not_found else @@ -771,7 +669,6 @@ let hasnatdynlink = !prefs.natdynlink && best_compiler = "opt" let natdynlinkflag = if hasnatdynlink then "true" else "false" - (** * OS dependent libraries *) let operating_system = @@ -1111,9 +1008,6 @@ let print_summary () = pr " OCaml binaries in : %s\n" (esc camlbin); pr " OCaml library in : %s\n" (esc camllib); pr " OCaml flambda flags : %s\n" (String.concat " " !prefs.flambda_flags); - pr " Camlp5 version : %s\n" camlp5_version; - pr " Camlp5 binaries in : %s\n" (esc camlp5bindir); - pr " Camlp5 library in : %s\n" (esc camlp5libdir); if best_compiler = "opt" then pr " Native dynamic link support : %B\n" hasnatdynlink; if coqide <> "no" then @@ -1153,7 +1047,6 @@ let write_dbg_wrapper f = pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure #\n\n"; pr "export COQTOP=%S\n" coqtop; pr "OCAMLDEBUG=%S\n" (camlbin^"/ocamldebug"); - pr "CAMLP5LIB=%S\n\n" camlp5libdir; pr ". $COQTOP/dev/ocamldebug-coq.run\n"; close_out o; Unix.chmod f 0o555 @@ -1185,10 +1078,6 @@ let write_configml f = pr_p "datadirsuffix" datadirsuffix; pr_p "docdirsuffix" docdirsuffix; pr_s "ocamlfind" camlexec.find; - pr_s "camlp5o" camlp5o; - pr_s "camlp5bin" camlp5bindir; - pr_s "camlp5lib" camlp5libdir; - pr_s "camlp5compat" camlp5compat; pr_s "caml_flags" caml_flags; pr_s "version" coq_version; pr_s "caml_version" caml_version; @@ -1295,11 +1184,6 @@ let write_makefile f = pr "CAMLDEBUGOPT=%s\n\n" coq_debug_flag; pr "# Compilation profile flag\n"; pr "CAMLTIMEPROF=%s\n\n" coq_profile_flag; - pr "# Camlp5 : flavor, binaries, libraries ...\n"; - pr "# NB : avoid using CAMLP5LIB (conflict under Windows)\n"; - pr "CAMLP5O=%s\n" (win_aware_quote_executable camlp5o); - pr "CAMLP5COMPAT=%s\n" camlp5compat; - pr "MYCAMLP5LIB=%S\n\n" camlp5libdir; pr "# Your architecture\n"; pr "# Can be obtain by UNIX command arch\n"; pr "ARCH=%s\n" arch; diff --git a/coq.opam b/coq.opam index ab18119ac4d0..ae1f68831258 100644 --- a/coq.opam +++ b/coq.opam @@ -22,7 +22,6 @@ depends: [ "ocaml" { >= "4.05.0" } "dune" { build & >= "1.4.0" } "num" - "camlp5" { >= "7.03" } ] build-env: [ diff --git a/default.nix b/default.nix index 7c8113c9ab37..589d1fff81bd 100644 --- a/default.nix +++ b/default.nix @@ -48,7 +48,7 @@ stdenv.mkDerivation rec { python2 time # coq-makefile timing tools dune ] - ++ (with ocamlPackages; [ ocaml findlib camlp5 num ]) + ++ (with ocamlPackages; [ ocaml findlib num ]) ++ optional buildIde ocamlPackages.lablgtk ++ optionals buildDoc [ # Sphinx doc dependencies diff --git a/dev/base_include b/dev/base_include index d2e8f6d092e0..48feeec1472f 100644 --- a/dev/base_include +++ b/dev/base_include @@ -8,6 +8,7 @@ #directory "toplevel";; #directory "library";; #directory "kernel";; +#directory "gramlib";; #directory "engine";; #directory "pretyping";; #directory "lib";; @@ -18,8 +19,6 @@ #directory "stm";; #directory "vernac";; -#directory "+camlp5";; (* Gramext is found in top_printers.ml *) - #use "top_printers.ml";; #use "vm_printers.ml";; diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 0dcabc0b97f9..d0b5f4be4753 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1076,7 +1076,7 @@ function make_ocaml { function make_ocaml_tools { make_findlib - make_camlp5 + # make_camlp5 } ##### OCAML EXTRA LIBRARIES ##### @@ -1386,7 +1386,7 @@ function make_coq { make_ocaml make_num make_findlib - make_camlp5 + # make_camlp5 make_lablgtk if case $COQ_VERSION in diff --git a/dev/ci/README.md b/dev/ci/README.md index 7ed90f524c6d..bc49e3e76b90 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -84,10 +84,10 @@ unless these tests pass. We are currently running tests on the following platforms: -- GitLab CI is the main CI platform. It tests the compilation of Coq, of the - documentation, and of CoqIDE on Linux with several versions of OCaml / - camlp5, and with warnings as errors; it runs the test-suite and tests the - compilation of several external developments. +- GitLab CI is the main CI platform. It tests the compilation of Coq, + of the documentation, and of CoqIDE on Linux with several versions + of OCaml and with warnings as errors; it runs the test-suite and + tests the compilation of several external developments. - Travis CI is used to test the compilation of Coq and run the test-suite on macOS. It also runs a linter that checks whitespace discipline. A diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index 84fec71f7a1e..abeb039c0e9e 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -10,6 +10,6 @@ bash opam64/install.sh opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH eval "$(opam config env)" -opam install -y num ocamlfind camlp5 ounit +opam install -y num ocamlfind ounit cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 4ddb58241406..3fc6dce4e5e6 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-10-30-V1" +# CACHEKEY: "bionic_coq-V2018-11-08-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -41,29 +41,27 @@ ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. -ENV CAMLP5_VER="7.03" \ - COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" +ENV COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" # base switch RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \ - opam install $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM + opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM # base+32bit switch RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ - opam install $BASE_OPAM camlp5.$CAMLP5_VER + opam install $BASE_OPAM # EDGE switch ENV COMPILER_EDGE="4.07.1" \ - CAMLP5_VER_EDGE="7.06.10-g84ce6cc4" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ BASE_OPAM_EDGE="dune-release.1.1.0" RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ - opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE + opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \ - opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM + opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE $CI_OPAM RUN opam clean -a -c diff --git a/dev/doc/README.md b/dev/doc/README.md index 223cf6286edc..c764455aed41 100644 --- a/dev/doc/README.md +++ b/dev/doc/README.md @@ -16,7 +16,6 @@ $ opam init --comp ~/.bashrc and ~/.ocamlinit files. $ source ~/.bashrc -$ opam install camlp5 # needed if you want to build "coqide" target diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 30a2967259cc..acb0d80c185a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,5 +1,15 @@ ## Changes between Coq 8.9 and Coq 8.10 +### ML4 Pre Processing + +- Support for `.ml4` files, processed by camlp5 has been removed in + favor of `.mlg` files processed by `coqpp`. + + Porting is usually straightforward, and involves renaming the + `file.ml4` file to `file.mlg` and adding a few brackets. + + See "Transitioning away from Camlp5" below for update instructions. + ### ML API General deprecation diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index d330f517bee2..707c7f07ce95 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -8,14 +8,13 @@ # here are some reasonable default values [ -z "$OCAMLDEBUG" ] && OCAMLDEBUG=ocamldebug -[ -z "$CAMLP5LIB" ] && CAMLP5LIB=+camlp5 [ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD [ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD` export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH exec $OCAMLDEBUG \ - -I $CAMLP5LIB -I +threads \ + -I +threads \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ diff --git a/gramlib/gramlib.mllib b/gramlib/gramlib.mllib new file mode 100644 index 000000000000..4c915b2b05b6 --- /dev/null +++ b/gramlib/gramlib.mllib @@ -0,0 +1,4 @@ +Ploc +Plexing +Gramext +Grammar diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp deleted file mode 100644 index 715b8cd23f1a..000000000000 --- a/grammar/argextend.mlp +++ /dev/null @@ -1,221 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* > *) - -let declare_arg loc s e = - declare_str_items loc [ - <:str_item< value ($lid:"wit_"^s$, $lid:s$) = $e$ >>; - (** Prevent the unused variable warning *) - <:str_item< value _ = ($lid:"wit_"^s$, $lid:s$) >>; - ] - -let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >> - -let rec make_wit loc = function - | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >> - | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> - | PairArgType (t1,t2) -> - <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >> - | ExtraArgType s -> mk_extraarg loc s - -let is_self s = function -| ExtraArgType s' -> s = s' -| _ -> false - -let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >> -let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >> -let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >> - -let make_act loc act pil = - let rec make = function - | [] -> <:expr< (fun loc -> $act$) >> - | ExtNonTerminal (_, None) :: tl -> <:expr< (fun $lid:"_"$ -> $make tl$) >> - | ExtNonTerminal (_, Some p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> - | ExtTerminal _ :: tl -> - <:expr< (fun _ -> $make tl$) >> in - make (List.rev pil) - -let make_prod_item self = function - | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >> - | ExtNonTerminal (Uentry e, _) when e = self -> <:expr< Extend.Aself >> - | ExtNonTerminal (g, _) -> - let base s = <:expr< $lid:s$ >> in - mlexpr_of_prod_entry_key base g - -let rec make_prod self = function -| [] -> <:expr< Extend.Stop >> -| item :: prods -> <:expr< Extend.Next $make_prod self prods$ $make_prod_item self item$ >> - -let make_rule loc self (prods,act) = - <:expr< Extend.Rule $make_prod self (List.rev prods)$ $make_act loc act prods$ >> - -let is_ident x = function -| <:expr< $lid:s$ >> -> (s : string) = x -| _ -> false - -let make_extend loc self cl = match cl with -| [[ExtNonTerminal (Uentry e, Some id)], act] when is_ident id act -> - (** Special handling of identity arguments by not redeclaring an entry *) - <:expr< Vernacextend.Arg_alias $lid:e$ >> -| _ -> - <:expr< Vernacextend.Arg_rules $mlexpr_of_list (make_rule loc self) (List.rev cl)$ >> - -let warning_deprecated prefix s = function -| None -> () -| Some _ -> - Printf.eprintf "Deprecated [%sTYPED AS] clause in [ARGUMENT EXTEND %s]. \ - Use [TYPED AS] instead.\n%!" prefix s - -let get_type s = function -| None -> None -| Some typ -> - if is_self s typ then - let () = Printf.eprintf "Redundant [TYPED AS] clause in [ARGUMENT EXTEND %s].\n%!" s in - None - else Some typ - -let declare_tactic_argument loc s (typ, f, g, h) cl = - let se = mlexpr_of_string s in - let typ, pr = match typ with - | `Uniform (typ, pr) -> - let typ = get_type s typ in - typ, <:expr< ($lid:pr$, $lid:pr$, $lid:pr$) >> - | `Specialized (a, rpr, c, gpr, e, tpr) -> - let () = warning_deprecated "RAW_" s a in - let () = warning_deprecated "GLOB_" s c in - let typ = get_type s e in - typ, <:expr< ($lid:rpr$, $lid:gpr$, $lid:tpr$) >> - in - let glob = match g, typ with - | Some f, (None | Some _) -> - <:expr< Tacentries.ArgInternFun (fun ist v -> (ist, $lid:f$ ist v)) >> - | None, Some typ -> - <:expr< Tacentries.ArgInternWit $make_wit loc typ$ >> - | None, None -> - <:expr< Tacentries.ArgInternFun (fun ist v -> (ist, v)) >> - in - let interp = match f, typ with - | Some f, (None | Some _) -> - <:expr< Tacentries.ArgInterpLegacy $lid:f$ >> - | None, Some typ -> - <:expr< Tacentries.ArgInterpWit $make_wit loc typ$ >> - | None, None -> - <:expr< Tacentries.ArgInterpRet >> - in - let subst = match h, typ with - | Some f, (None | Some _) -> - <:expr< Tacentries.ArgSubstFun $lid:f$ >> - | None, Some typ -> - <:expr< Tacentries.ArgSubstWit $make_wit loc typ$ >> - | None, None -> - <:expr< Tacentries.ArgSubstFun (fun s v -> v) >> - in - let dyn = mlexpr_of_option (fun typ -> <:expr< Geninterp.val_tag $make_topwit loc typ$ >>) typ in - declare_arg loc s <:expr< Tacentries.argument_extend ~{ name = $se$ } { - Tacentries.arg_parsing = $make_extend loc s cl$; - Tacentries.arg_tag = $dyn$; - Tacentries.arg_intern = $glob$; - Tacentries.arg_subst = $subst$; - Tacentries.arg_interp = $interp$; - Tacentries.arg_printer = $pr$ - } >> - -let declare_vernac_argument loc s pr cl = - let se = mlexpr_of_string s in - let pr_rules = match pr with - | None -> <:expr< fun _ -> Pp.str $str:"[No printer for "^s^"]"$ >> - | Some pr -> <:expr< $lid:pr$ >> in - declare_arg loc s <:expr< Vernacextend.vernac_argument_extend ~{ name = $se$ } { - Vernacextend.arg_printer = $pr_rules$; - Vernacextend.arg_parsing = $make_extend loc s cl$ - } >> - -open Pcaml - -EXTEND - GLOBAL: str_item; - str_item: - [ [ "ARGUMENT"; "EXTEND"; s = entry_name; - header = argextend_header; - OPT "|"; l = LIST1 argrule SEP "|"; - "END" -> - declare_tactic_argument loc s header l - | "VERNAC"; "ARGUMENT"; "EXTEND"; s = entry_name; - pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr]; - OPT "|"; l = LIST1 argrule SEP "|"; - "END" -> - declare_vernac_argument loc s pr l ] ] - ; - argextend_specialized: - [ [ rawtyp = OPT [ "RAW_TYPED"; "AS"; rawtyp = argtype -> rawtyp ]; - "RAW_PRINTED"; "BY"; rawpr = LIDENT; - globtyp = OPT [ "GLOB_TYPED"; "AS"; globtyp = argtype -> globtyp ]; - "GLOB_PRINTED"; "BY"; globpr = LIDENT -> - (rawtyp, rawpr, globtyp, globpr) ] ] - ; - argextend_header: - [ [ typ = OPT [ "TYPED"; "AS"; typ = argtype -> typ ]; - "PRINTED"; "BY"; pr = LIDENT; - f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; - g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; - h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ]; - special = OPT argextend_specialized -> - let repr = match special with - | None -> `Uniform (typ, pr) - | Some (rtyp, rpr, gtyp, gpr) -> `Specialized (rtyp, rpr, gtyp, gpr, typ, pr) - in - (repr, f, g, h) ] ] - ; - argtype: - [ "2" - [ e1 = argtype; "*"; e2 = argtype -> PairArgType (e1, e2) ] - | "1" - [ e = argtype; LIDENT "list" -> ListArgType e - | e = argtype; LIDENT "option" -> OptArgType e ] - | "0" - [ e = LIDENT -> - let e = parse_user_entry e "" in - type_of_user_symbol e - | "("; e = argtype; ")" -> e ] ] - ; - argrule: - [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ] - ; - genarg: - [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, Some s) - | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let e = parse_user_entry e sep in - ExtNonTerminal (e, Some s) - | e = LIDENT -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, None) - | s = STRING -> ExtTerminal s - ] ] - ; - entry_name: - [ [ s = LIDENT -> s - | UIDENT -> failwith "Argument entry names must be lowercase" - ] ] - ; - END diff --git a/grammar/dune b/grammar/dune deleted file mode 100644 index 78df2826d600..000000000000 --- a/grammar/dune +++ /dev/null @@ -1,41 +0,0 @@ -(library - (name grammar5) - (synopsis "Coq Camlp5 Grammar Extensions for Plugins") - (public_name coq.grammar) - (flags (:standard -w -58)) - (libraries camlp5)) - -; Custom camlp5! This is a net speedup, and a preparation for using -; Dune's preprocessor abilities. -(rule - (targets coqmlp5) - (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx -o coqmlp5))) - -(rule - (targets coqp5) - (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar5.cmxa} -o coqp5))) - -(install - (section bin) - (package coq) - (files coqp5 coqmlp5)) - -(rule - (targets q_util.ml) - (deps (:mlp-file q_util.mlp)) - (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets}))) - -(rule - (targets argextend.ml) - (deps (:mlp-file argextend.mlp)) - (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets}))) - -(rule - (targets tacextend.ml) - (deps (:mlp-file tacextend.mlp)) - (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets}))) - -(rule - (targets vernacextend.ml) - (deps (:mlp-file vernacextend.mlp)) - (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets}))) diff --git a/grammar/q_util.mli b/grammar/q_util.mli deleted file mode 100644 index b163100fc3ce..000000000000 --- a/grammar/q_util.mli +++ /dev/null @@ -1,54 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* MLast.expr) -> 'a list -> MLast.expr - -val mlexpr_of_pair : - ('a -> MLast.expr) -> ('b -> MLast.expr) - -> 'a * 'b -> MLast.expr - -val mlexpr_of_bool : bool -> MLast.expr - -val mlexpr_of_int : int -> MLast.expr - -val mlexpr_of_string : string -> MLast.expr - -val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr - -val mlexpr_of_name : ('a -> MLast.expr) -> 'a option -> MLast.expr - -val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.expr - -val type_of_user_symbol : user_symbol -> argument_type - -val parse_user_entry : string -> string -> user_symbol - -val mlexpr_of_symbol : user_symbol -> MLast.expr - -val binders_of_tokens : MLast.expr -> extend_token list -> MLast.expr diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp deleted file mode 100644 index a2007d258ccb..000000000000 --- a/grammar/q_util.mlp +++ /dev/null @@ -1,150 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* - let e1 = f e1 in - let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in - <:expr< [$e1$ :: $e2$] >>) - l (let loc = Ploc.dummy in <:expr< [] >>) - -let mlexpr_of_pair m1 m2 (a1,a2) = - let e1 = m1 a1 and e2 = m2 a2 in - let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in - <:expr< ($e1$, $e2$) >> - -(* We don't give location for tactic quotation! *) -let loc = Ploc.dummy - - -let mlexpr_of_bool = function - | true -> <:expr< True >> - | false -> <:expr< False >> - -let mlexpr_of_int n = <:expr< $int:string_of_int n$ >> - -let mlexpr_of_string s = <:expr< $str:s$ >> - -let mlexpr_of_option f = function - | None -> <:expr< None >> - | Some e -> <:expr< Some $f e$ >> - -let mlexpr_of_name f = function - | None -> <:expr< Names.Name.Anonymous >> - | Some e -> <:expr< Names.Name.Name $f e$ >> - -let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >> - -let rec mlexpr_of_prod_entry_key f = function - | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> - | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> - | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> - | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> - | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> - | Uentry e -> <:expr< Extend.Aentry ($f e$) >> - | Uentryl (e, l) -> - (** Keep in sync with Pcoq! *) - assert (e = "tactic"); - if l = 5 then <:expr< Extend.Aentry Pltac.binder_tactic >> - else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_string (string_of_int l)$ >> - -let rec type_of_user_symbol = function -| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> - ListArgType (type_of_user_symbol s) -| Uopt s -> - OptArgType (type_of_user_symbol s) -| Uentry e | Uentryl (e, _) -> ExtraArgType e - -let coincide s pat off = - let len = String.length pat in - let break = ref true in - let i = ref 0 in - while !break && !i < len do - let c = Char.code s.[off + !i] in - let d = Char.code pat.[!i] in - break := c = d; - incr i - done; - !break - -let check_separator sep = - if sep <> "" then failwith "Separator is only for arguments with suffix _list_sep." - -let rec parse_user_entry s sep = - let l = String.length s in - if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then - let entry = parse_user_entry (String.sub s 3 (l-8)) "" in - check_separator sep; - Ulist1 entry - else if l > 12 && coincide s "ne_" 0 && - coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 3 (l-12)) "" in - Ulist1sep (entry, sep) - else if l > 5 && coincide s "_list" (l-5) then - let entry = parse_user_entry (String.sub s 0 (l-5)) "" in - check_separator sep; - Ulist0 entry - else if l > 9 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 0 (l-9)) "" in - Ulist0sep (entry, sep) - else if l > 4 && coincide s "_opt" (l-4) then - let entry = parse_user_entry (String.sub s 0 (l-4)) "" in - check_separator sep; - Uopt entry - else if l = 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then - let n = Char.code s.[6] - 48 in - check_separator sep; - Uentryl ("tactic", n) - else - let s = match s with "hyp" -> "var" | _ -> s in - check_separator sep; - Uentry s - -let rec mlexpr_of_symbol = function -| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >> -| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >> -| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >> -| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >> -| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >> -| Uentry e -> - let wit = <:expr< $lid:"wit_"^e$ >> in - <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >> -| Uentryl (e, l) -> - assert (e = "tactic"); - let wit = <:expr< $lid:"wit_"^e$ >> in - <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>> - -let rec binders_of_tokens e = function -| [] -> e -| ExtNonTerminal(_,None) :: cl -> <:expr< fun _ -> $binders_of_tokens e cl$ >> -| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_tokens e cl$ >> -| ExtTerminal _ :: cl -> binders_of_tokens e cl diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp deleted file mode 100644 index a093f783885a..000000000000 --- a/grammar/tacextend.mlp +++ /dev/null @@ -1,72 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* > - -let rec mlexpr_of_clause = function -| [] -> <:expr< TyNil >> -| ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >> -| ExtNonTerminal (g, _) :: cl -> - <:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> - -open Pcaml - -EXTEND - GLOBAL: str_item; - str_item: - [ [ "TACTIC"; "EXTEND"; s = tac_name; - depr = OPT [ "DEPRECATED"; depr = LIDENT -> depr ]; - level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ]; - OPT "|"; l = LIST1 tacrule SEP "|"; - "END" -> - let level = match level with Some i -> int_of_string i | None -> 0 in - let level = mlexpr_of_int level in - let depr = mlexpr_of_option (fun l -> <:expr< $lid:l$ >>) depr in - let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in - declare_str_items loc [ <:str_item< Tacentries.tactic_extend - $plugin_name$ $str:s$ ~{ level = $level$ } ?{ deprecation = - $depr$ } $l$ >> ] ] ] - ; - tacrule: - [ [ "["; l = LIST1 tacargs; "]"; - "->"; "["; e = Pcaml.expr; "]" -> - let e = <:expr< fun ist -> $e$ >> in - <:expr< TyML($mlexpr_of_clause l$, $binders_of_tokens e l$) >> - ] ] - ; - - tacargs: - [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, Some s) - | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let e = parse_user_entry e sep in - ExtNonTerminal (e, Some s) - | e = LIDENT -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, None) - | s = STRING -> - let () = if s = "" then failwith "Empty terminal." in - ExtTerminal s - ] ] - ; - tac_name: - [ [ s = LIDENT -> s - | s = UIDENT -> s - ] ] - ; - END diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp deleted file mode 100644 index d44eeef6707d..000000000000 --- a/grammar/vernacextend.mlp +++ /dev/null @@ -1,115 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <:expr< Vernacextend.TyNil >> -| ExtTerminal s :: cl -> <:expr< Vernacextend.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >> -| ExtNonTerminal (g, id) :: cl -> - <:expr< Vernacextend.TyNonTerminal ($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> - -let make_rule r = - let ty = mlexpr_of_clause r.r_patt in - let cmd = binders_of_tokens r.r_branch r.r_patt in - let make_classifier c = binders_of_tokens c r.r_patt in - let classif = mlexpr_of_option make_classifier r.r_class in - <:expr< Vernacextend.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >> - -let declare_command loc s c nt cl = - let se = mlexpr_of_string s in - let c = mlexpr_of_option (fun x -> x) c in - let rules = mlexpr_of_list make_rule cl in - declare_str_items loc - [ <:str_item< Vernacextend.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ] - -open Pcaml - -EXTEND - GLOBAL: str_item; - str_item: - [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; c = OPT classification; - OPT "|"; l = LIST1 rule SEP "|"; - "END" -> - declare_command loc s c <:expr> l - | "VERNAC"; "COMMAND"; "FUNCTIONAL"; "EXTEND"; s = UIDENT; c = OPT classification; - OPT "|"; l = LIST1 fun_rule SEP "|"; - "END" -> - declare_command loc s c <:expr> l - | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; c = OPT classification; - OPT "|"; l = LIST1 rule SEP "|"; - "END" -> - declare_command loc s c <:expr> l - | "DECLARE"; "PLUGIN"; name = STRING -> - declare_str_items loc [ - <:str_item< value __coq_plugin_name = $str:name$ >>; - <:str_item< value _ = Mltop.add_known_module __coq_plugin_name >>; - ] - ] ] - ; - classification: - [ [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> - | "CLASSIFIED"; "AS"; "SIDEFF" -> - <:expr< fun _ -> Vernac_classifier.classify_as_sideeff >> - | "CLASSIFIED"; "AS"; "QUERY" -> - <:expr< fun _ -> Vernac_classifier.classify_as_query >> - ] ] - ; - deprecation: - [ [ -> false | "DEPRECATED" -> true ] ] - ; - rule: - [ [ "["; OPT "-"; l = LIST1 args; "]"; - d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in - { r_patt = l; r_class = c; r_branch = b; r_depr = d; } - ] ] - ; - (** The [OPT "-"] argument serves no purpose nowadays, it is left here for - backward compatibility. *) - fun_rule: - [ [ "["; OPT "-"; l = LIST1 args; "]"; - d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - { r_patt = l; r_class = c; r_branch = e; r_depr = d; } - ] ] - ; - classifier: - [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< $c$>> ] ] - ; - args: - [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, Some s) - | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let e = parse_user_entry e sep in - ExtNonTerminal (e, Some s) - | e = LIDENT -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, None) - | s = STRING -> - ExtTerminal s - ] ] - ; - END -;; diff --git a/lib/envars.ml b/lib/envars.ml index 724a3dddc7b8..b5036e73403e 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -177,10 +177,6 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ()); fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); - fprintf f "%sCAMLP5O=%s\n" prefix_var_name Coq_config.camlp5o; - fprintf f "%sCAMLP5BIN=%s/\n" prefix_var_name Coq_config.camlp5bin; - fprintf f "%sCAMLP5LIB=%s\n" prefix_var_name Coq_config.camlp5lib; - fprintf f "%sCAMLP5OPTIONS=%s\n" prefix_var_name Coq_config.camlp5compat; fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 0d1629c3d5cf..b673225e409a 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -20,7 +20,6 @@ include @CONF_FILE@ VFILES := $(COQMF_VFILES) MLIFILES := $(COQMF_MLIFILES) MLFILES := $(COQMF_MLFILES) -ML4FILES := $(COQMF_ML4FILES) MLGFILES := $(COQMF_MLGFILES) MLPACKFILES := $(COQMF_MLPACKFILES) MLLIBFILES := $(COQMF_MLLIBFILES) @@ -37,10 +36,6 @@ LOCAL := $(COQMF_LOCAL) COQLIB := $(COQMF_COQLIB) DOCDIR := $(COQMF_DOCDIR) OCAMLFIND := $(COQMF_OCAMLFIND) -CAMLP5O := $(COQMF_CAMLP5O) -CAMLP5BIN := $(COQMF_CAMLP5BIN) -CAMLP5LIB := $(COQMF_CAMLP5LIB) -CAMLP5OPTIONS := $(COQMF_CAMLP5OPTIONS) CAMLFLAGS := $(COQMF_CAMLFLAGS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) @@ -192,22 +187,11 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP5LIB) +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) # ocamldoc fails with unknown argument otherwise CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) -# FIXME This should be generated by Coq -GRAMMARS:=grammar.cma -CAMLP5EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo - -CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null) -ifeq (,$(CAMLLIB)) -PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.") -else -PP:=-pp '$(CAMLP5O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP5EXTEND) $(GRAMMARS) $(CAMLP5OPTIONS) -impl' -endif - ifneq (,$(TIMING)) TIMING_ARG=-time ifeq (after,$(TIMING)) @@ -774,10 +758,6 @@ printenv:: @echo 'COQLIB = $(COQLIB)' @echo 'DOCDIR = $(DOCDIR)' @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'CAMLP5O = $(CAMLP5O)' - @echo 'CAMLP5BIN = $(CAMLP5BIN)' - @echo 'CAMLP5LIB = $(CAMLP5LIB)' - @echo 'CAMLP5OPTIONS = $(CAMLP5OPTIONS)' @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)'