Merge PR coq#8985: [gramlib] [build] Switch make-based system to pack…

…ed gramlib

.gitignore

@@ -165,6 +165,9 @@ user-contrib
 plugins/ssr/ssrparser.ml
 plugins/ssr/ssrvernac.ml
 
+# gramlib__pack
+gramlib__pack
+
 # ocaml dev files
 .merlin
 META.coq

.merlin.in

@@ -40,6 +40,8 @@ S API
 B API
 S ide
 B ide
+S gramlib__pack
+B gramlib__pack
 
 S tools
 B tools

META.coq.in

@@ -4,7 +4,7 @@ description = "The Coq Proof Assistant Plugin API"
 version = "8.10"
 
 directory = ""
-requires = "camlp5"
+requires = ""
 
 package "grammar" (
 
@@ -153,12 +153,24 @@ package "proofs" (
 
 )
 
+package "gramlib" (
+
+  description = "Coq Parsing Library"
+  version     = "8.10"
+
+  requires    = ""
+  directory   = "gramlib__pack"
+
+  archive(byte)    = "gramlib.cma"
+  archive(native)  = "gramlib.cmxa"
+)
+
 package "parsing" (
 
   description = "Coq Parsing Engine"
   version     = "8.10"
 
-  requires    = "camlp5.gramlib, coq.proofs"
+  requires    = "coq.gramlib, coq.proofs"
   directory   = "parsing"
 
   archive(byte)    = "parsing.cma"

Makefile

@@ -94,6 +94,10 @@ EXISTINGMLI := $(call find, '*.mli')
 ## Files that will be generated
 
 GENMLGFILES:= $(MLGFILES:.mlg=.ml)
+# GRAMFILES must be in linking order
+export GRAMFILES=$(addprefix gramlib__pack/gramlib__,Ploc Plexing Gramext Grammar)
+export GRAMMLFILES := $(addsuffix .ml, $(GRAMFILES)) $(addsuffix .mli, $(GRAMFILES))
+export GENGRAMFILES := $(GRAMMLFILES) gramlib__pack/gramlib.ml
 export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES)  ide/coqide_os_specific.ml kernel/copcodes.ml
 export GENHFILES:=kernel/byterun/coq_jumptbl.h
 export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
@@ -190,12 +194,16 @@ META.coq: META.coq.in
 
 .PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean
 
-clean: objclean cruftclean depclean docclean camldevfilesclean
+clean: objclean cruftclean depclean docclean camldevfilesclean gramlibclean
 
 cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean
 
 objclean: archclean indepclean
 
+.PHONY: gramlibclean
+gramlibclean:
+	rm -rf gramlib__pack/
+
 cruftclean: mlgclean
 	find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} +
 	rm -f gmon.out core
@@ -284,7 +292,7 @@ KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(MLPACKFILES:.mlpack=.ml) \
  $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp))
 KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \
  $(MLIFILES:.mli=.cmi) \
- $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma
+ gramlib__pack/gramlib.cma gramlib__pack/gramlib.cmxa $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma
 ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS))
 
 alienclean:

Makefile.build

@@ -206,7 +206,7 @@ OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
 
 BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
 OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS)
-DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$@),, -I ide -I ide/protocol)
+DEPFLAGS=$(LOCALINCLUDES) -map gramlib__pack/gramlib.ml $(if $(filter plugins/%,$@),, -I ide -I ide/protocol)
 
 # On MacOS, the binaries are signed, except our private ones
 ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin)
@@ -264,9 +264,6 @@ PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo)
 # Main packages linked by Coq.
 SYSMOD:=-package num,str,unix,dynlink,threads
 
-# We do not repeat the dependencies already in SYSMOD here
-P4CMA:=gramlib.cma
-
 ###########################################################################
 # Infrastructure for the rest of the Makefile
 ###########################################################################
@@ -418,7 +415,7 @@ $(COQTOPEXE): $(TOPBINOPT:.opt=.$(BEST))
 bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) \
-			   $(SYSMOD) -package camlp5.gramlib \
+			   $(SYSMOD) \
 			   $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
 	$(STRIP_HIDE) $@
 	$(CODESIGN_HIDE) $@
@@ -427,7 +424,7 @@ bin/%.byte$(EXE): topbin/%_bin.ml $(LINKCMO) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) \
 	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
-			 $(SYSMOD) -package camlp5.gramlib \
+			 $(SYSMOD) \
 			 $(LINKCMO) $(BYTEFLAGS) $< -o $@
 
 COQTOP_BYTE=topbin/coqtop_byte_bin.ml
@@ -438,7 +435,7 @@ $(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(COQTOP_BYTE)
 	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(OCAMLC) -linkall -linkpkg -I lib -I vernac -I toplevel \
 	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
-			 $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \
+			 $(SYSMOD) -package compiler-libs.toplevel \
 			 $(LINKCMO) $(BYTEFLAGS) $(COQTOP_BYTE) -o $@
 
 # For coqc
@@ -630,15 +627,40 @@ test-suite: world byte $(ALLSTDLIB).v
 # Default rules for compiling ML code
 ###########################################################################
 
-# Target for libraries .cma and .cmxa
+gramlib__pack:
+	mkdir -p $@
 
-# The dependency over the .mllib is somewhat artificial, since
-# ocamlc -a won't use this file, hence the $(filter-out ...) below.
-# But this ensures that the .cm(x)a is rebuilt when needed,
-# (especially when removing a module in the .mllib).
-# We used to have a "order-only" dependency over .mllib.d here,
-# but the -include mechanism should already ensure that we have
-# up-to-date dependencies.
+# gramlib.ml contents
+gramlib__pack/gramlib.ml: | gramlib__pack
+	echo " \
+module Ploc    = Gramlib__Ploc \
+module Plexing = Gramlib__Plexing \
+module Gramext = Gramlib__Gramext \
+module Grammar = Gramlib__Grammar" > $@
+
+gramlib__pack/gramlib__P%: gramlib/p% | gramlib__pack
+	cp -a $< $@
+	sed -e "1i # 1 \"$<\"" -i $@
+gramlib__pack/gramlib__G%: gramlib/g% | gramlib__pack
+	cp -a $< $@
+	sed -e "1i # 1 \"$<\"" -i $@
+
+# Specific rules for gramlib to pack it Dune / OCaml 4.08 style
+GRAMOBJS=$(addsuffix .cmo, $(GRAMFILES))
+
+gramlib__pack/%: COND_BYTEFLAGS+=-no-alias-deps -w -49
+gramlib__pack/%: COND_OPTFLAGS+=-no-alias-deps -w -49
+
+gramlib__pack/gramlib.%: COND_OPENFLAGS=
+gramlib__pack/gramlib__%: COND_OPENFLAGS=-open Gramlib
+
+gramlib__pack/gramlib.cma: $(GRAMOBJS) gramlib__pack/gramlib.cmo
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $^
+
+gramlib__pack/gramlib.cmxa: $(GRAMOBJS:.cmo=.cmx) gramlib__pack/gramlib.cmx
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $^
 
 # Specific rule for kernel.cma, with $(VMBYTEFLAGS).
 # This helps loading dllcoqrun.so during an ocamldebug
@@ -651,6 +673,16 @@ kernel/kernel.cmxa: kernel/kernel.mllib
 	$(SHOW)'OCAMLOPT -a -o $@'
 	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -I kernel/byterun/ -cclib -lcoqrun -a -o $@ $(filter-out %.mllib, $^)
 
+# Target for libraries .cma and .cmxa
+
+# The dependency over the .mllib is somewhat artificial, since
+# ocamlc -a won't use this file, hence the $(filter-out ...) below.
+# But this ensures that the .cm(x)a is rebuilt when needed,
+# (especially when removing a module in the .mllib).
+# We used to have a "order-only" dependency over .mllib.d here,
+# but the -include mechanism should already ensure that we have
+# up-to-date dependencies.
+
 %.cma: %.mllib
 	$(SHOW)'OCAMLC -a -o $@'
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
@@ -672,11 +704,14 @@ kernel/kernel.cmxa: kernel/kernel.mllib
 COND_IDEFLAGS=$(if $(filter ide/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,)
 COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,)
 
+# For module packing
+COND_OPENFLAGS=
+
 COND_BYTEFLAGS= \
- $(COND_IDEFLAGS) $(COND_PRINTERFLAGS) $(MLINCLUDES) $(BYTEFLAGS)
+ $(COND_IDEFLAGS) $(COND_PRINTERFLAGS) $(MLINCLUDES) $(BYTEFLAGS) $(COND_OPENFLAGS)
 
 COND_OPTFLAGS= \
- $(COND_IDEFLAGS) $(MLINCLUDES) $(OPTFLAGS)
+ $(COND_IDEFLAGS) $(MLINCLUDES) $(OPTFLAGS) $(COND_OPENFLAGS)
 
 plugins/micromega/%.cmi: plugins/micromega/%.mli
 	$(SHOW)'OCAMLC    $<'
@@ -780,12 +815,13 @@ kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50
 # Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12)
 OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .mlpack
 
-MAINMLFILES := $(filter-out checker/% plugins/%, $(MLFILES) $(MLIFILES))
-MAINMLLIBFILES := $(filter-out checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES))
+MAINMLFILES := $(filter-out gramlib__pack/% checker/% plugins/%, $(MLFILES) $(MLIFILES))
+MAINMLLIBFILES := $(filter-out gramlib__pack/% checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES))
 
-$(MLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLFILES) $(D_DEPEND_AFTER_SRC) $(GENFILES)
+$(MLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLFILES) $(D_DEPEND_AFTER_SRC) $(GENFILES) $(GENGRAMFILES)
 	$(SHOW)'OCAMLDEP  MLFILES MLIFILES'
-	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(MAINMLFILES) $(TOTARGET)
+	$(HIDE)$(OCAMLDEP) $(DEPFLAGS)  -passrest $(MAINMLFILES) -open Gramlib $(GRAMMLFILES) $(TOTARGET)
+#NB: -passrest is needed to avoid ocamlfind reordering the -open Gramlib
 
 $(MLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLLIBFILES) $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES)
 	$(SHOW)'OCAMLLIBDEP  MLLIBFILES MLPACKFILES'

Makefile.common

@@ -91,7 +91,7 @@ MKDIR:=install -d
 CORESRCDIRS:=\
   coqpp                                                                                 \
   config 	clib 		lib		kernel		kernel/byterun	library \
-  engine 	pretyping	interp	proofs	parsing 	printing \
+  engine 	pretyping	interp	proofs	gramlib__pack 	parsing 	printing \
   tactics 	vernac		stm		toplevel
 
 PLUGINDIRS:=\
@@ -119,6 +119,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \
 
 CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
         engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
+	gramlib__pack/gramlib.cma \
         parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
         stm/stm.cma toplevel/toplevel.cma
 

Makefile.install

@@ -93,7 +93,7 @@ install-tools:
 INSTALLCMI = $(sort \
 	$(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \
 	$(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \
-	$(PLUGINS:.cmo=.cmi)
+	$(PLUGINS:.cmo=.cmi) gramlib__pack/gramlib.cmi
 
 INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% \
 	configure.cmx toplevel/coqtop_byte_bin.cmx plugins/extraction/big.cmx, \

configure.ml

@@ -1212,7 +1212,7 @@ let write_configml f =
   pr_b "native_compiler" !prefs.nativecompiler;
 
   let core_src_dirs = [ "config"; "lib"; "clib"; "kernel"; "library";
-                        "engine"; "pretyping"; "interp"; "parsing"; "proofs";
+                        "engine"; "pretyping"; "interp"; "gramlib__pack"; "parsing"; "proofs";
                         "tactics"; "toplevel"; "printing"; "ide"; "stm"; "vernac" ] in
   let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ "  \"" ^ core_src_subdir ^ "\";\n")
                                     ""

dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh

@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8985" ] || [ "$CI_BRANCH" = "build+pack_gramlib" ]; then
+
+    elpi_CI_REF=use_coq_gramlib
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+fi

parsing/cLexer.ml

@@ -11,6 +11,7 @@
 open Pp
 open Util
 open Tok
+open Gramlib
 
 (** Location utilities  *)
 let ploc_file_of_coq_file = function

parsing/cLexer.mli

@@ -40,7 +40,7 @@ where
       tok_text : pattern -> string;
       tok_comm : mutable option (list location) }
  *)
-include Grammar.GLexerType with type te = Tok.t
+include Gramlib.Grammar.GLexerType with type te = Tok.t
 
 module Error : sig
   type t

parsing/dune

@@ -2,7 +2,6 @@
  (name parsing)
  (public_name coq.parsing)
  (wrapped false)
- (flags :standard -open Gramlib)
  (libraries coq.gramlib proofs))
 
 (rule

parsing/extend.ml

@@ -10,7 +10,7 @@
 
 (** Entry keys for constr notations *)
 
-type 'a entry = 'a Grammar.GMake(CLexer).Entry.e
+type 'a entry = 'a Gramlib.Grammar.GMake(CLexer).Entry.e
 
 type side = Left | Right
 

parsing/pcoq.ml

@@ -12,6 +12,7 @@ open CErrors
 open Util
 open Extend
 open Genarg
+open Gramlib
 
 let curry f x y = f (x, y)
 let uncurry f (x,y) = f x y

parsing/pcoq.mli

@@ -13,6 +13,7 @@ open Extend
 open Genarg
 open Constrexpr
 open Libnames
+open Gramlib
 
 (** The parser of Coq *)
 

plugins/funind/plugin_base.dune

@@ -2,5 +2,4 @@
  (name recdef_plugin)
  (public_name coq.plugins.recdef)
  (synopsis "Coq's functional induction plugin")
- (flags :standard -open Gramlib)
  (libraries coq.plugins.extraction))

plugins/ltac/plugin_base.dune

@@ -3,7 +3,6 @@
  (public_name coq.plugins.ltac)
  (synopsis "Coq's LTAC tactic language")
  (modules :standard \ tauto)
- (flags :standard -open Gramlib)
  (libraries coq.stm))
 
 (library

plugins/ssr/ssrcommon.ml

@@ -1092,8 +1092,8 @@ let tclDO n tac =
         let _, info = CErrors.push e in
         let e' = CErrors.UserError (l, prefix i ++ s) in
         Util.iraise (e', info)
-    | Ploc.Exc(loc, CErrors.UserError (l, s))  -> 
-        raise (Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
+    | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s))  ->
+        raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
   let rec loop i gl =
     if i = n then tac_err_at i gl else
     (tclTHEN (tac_err_at i) (loop (i + 1))) gl in

plugins/ssr/ssrelim.ml

@@ -404,7 +404,7 @@ let equality_inj l b id c gl =
   let msg = ref "" in
   try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
   with
-    | Ploc.Exc(_,CErrors.UserError (_,s))
+    | Gramlib.Ploc.Exc(_,CErrors.UserError (_,s))
     | CErrors.UserError (_,s)
   when msg := Pp.string_of_ppcmds s;
        !msg = "Not a projectable equality but a discriminable one." ||

plugins/ssrmatching/plugin_base.dune

@@ -2,5 +2,4 @@
  (name ssrmatching_plugin)
  (public_name coq.plugins.ssrmatching)
  (synopsis "Coq ssrmatching plugin")
- (flags :standard -open Gramlib)
  (libraries coq.plugins.ltac))

printing/dune

@@ -2,6 +2,5 @@
  (name printing)
  (synopsis "Coq's Term Pretty Printing Library")
  (public_name coq.printing)
- (flags :standard -open Gramlib)
  (wrapped false)
  (libraries parsing proofs))

printing/proof_diffs.ml

@@ -88,7 +88,7 @@ let tokenize_string s =
   let st = CLexer.get_lexer_state () in
   try
     let istr = Stream.of_string s in
-    let lex = CLexer.lexer.Plexing.tok_func istr in
+    let lex = CLexer.lexer.Gramlib.Plexing.tok_func istr in
     let toks = stream_tok [] (fst lex) in
     CLexer.set_lexer_state st;
     toks

tools/CoqMakefile.in

@@ -99,7 +99,7 @@ BEFORE ?=
 AFTER ?=
 
 # FIXME this should be generated by Coq (modules already linked by Coq)
-CAMLDONTLINK=camlp5.gramlib,unix,str
+CAMLDONTLINK=unix,str
 
 # OCaml binaries
 CAMLC       ?= "$(OCAMLFIND)" ocamlc   -c