[camlp5] Remove dependency on camlp5.

.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"

.merlin.in

@@ -53,4 +53,4 @@ B dev
 S plugins/**
 B plugins/**
 
-PKG threads.posix camlp5
+PKG threads.posix

.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

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

INSTALL

@@ -39,24 +39,21 @@ 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
 
    - 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 <options>
@@ -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
 

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    = ""

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"

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,78 +321,23 @@ 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)
 ###########################################################################
 
 .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

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
 ###########################################################################

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 $@
 
 ####################

checker/include

@@ -13,7 +13,6 @@
 #directory "kernel";;
 #directory "checker";;
 #directory "+threads";;
-#directory "+camlp5";;
 
 #load "unix.cma";;
 #load"threads.cma";;

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 *)