aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore4
-rw-r--r--.merlin.in4
-rw-r--r--META.coq.in2
-rw-r--r--Makefile8
-rw-r--r--Makefile.build26
-rw-r--r--Makefile.common4
-rw-r--r--Makefile.install9
-rw-r--r--configure.ml2
-rw-r--r--dev/ocamldebug-coq.run2
9 files changed, 32 insertions, 29 deletions
diff --git a/.gitignore b/.gitignore
index da675309e5..0411247abf 100644
--- a/.gitignore
+++ b/.gitignore
@@ -165,8 +165,7 @@ user-contrib
plugins/ssr/ssrparser.ml
plugins/ssr/ssrvernac.ml
-# gramlib__pack
-gramlib__pack
+/gramlib/.pack
# ocaml dev files
.merlin
@@ -178,3 +177,4 @@ theories/*/dune
theories/*/*/dune
theories/*/*/*/dune
*.install
+!Makefile.install
diff --git a/.merlin.in b/.merlin.in
index db7259dd6f..4d646842d8 100644
--- a/.merlin.in
+++ b/.merlin.in
@@ -40,8 +40,8 @@ S API
B API
S ide
B ide
-S gramlib__pack
-B gramlib__pack
+S gramlib/.pack
+B gramlib/.pack
S tools
B tools
diff --git a/META.coq.in b/META.coq.in
index b3a96a8303..c2d3f85b9f 100644
--- a/META.coq.in
+++ b/META.coq.in
@@ -147,7 +147,7 @@ package "gramlib" (
version = "8.10"
requires = "coq.lib"
- directory = "gramlib__pack"
+ directory = "gramlib/.pack"
archive(byte) = "gramlib.cma"
archive(native) = "gramlib.cmxa"
diff --git a/Makefile b/Makefile
index 330562afb6..628ad35ca4 100644
--- a/Makefile
+++ b/Makefile
@@ -95,9 +95,9 @@ EXISTINGMLI := $(call find, '*.mli')
GENMLGFILES:= $(MLGFILES:.mlg=.ml)
# GRAMFILES must be in linking order
-export GRAMFILES=$(addprefix gramlib__pack/gramlib__,Ploc Plexing Gramext Grammar)
+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 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)
@@ -201,7 +201,7 @@ objclean: archclean indepclean
.PHONY: gramlibclean
gramlibclean:
- rm -rf gramlib__pack/
+ rm -rf gramlib/.pack/
cruftclean: mlgclean
find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} +
@@ -291,7 +291,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) \
- gramlib__pack/gramlib.cma gramlib__pack/gramlib.cmxa $(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:
diff --git a/Makefile.build b/Makefile.build
index 8e4b63c364..ec9b81dba4 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -202,7 +202,7 @@ OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS)
-DEPFLAGS=$(LOCALINCLUDES) -map gramlib__pack/gramlib.ml $(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)
@@ -560,38 +560,38 @@ test-suite: world byte $(ALLSTDLIB).v
# Default rules for compiling ML code
###########################################################################
-gramlib__pack:
+gramlib/.pack:
mkdir -p $@
# gramlib.ml contents
-gramlib__pack/gramlib.ml: | gramlib__pack
+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
+gramlib/.pack/gramlib__P%: gramlib/p% | gramlib/.pack
cp -a $< $@
sed -e "1i # 1 \"$<\"" -i $@
-gramlib__pack/gramlib__G%: gramlib/g% | gramlib__pack
+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/%: 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.%: COND_OPENFLAGS=
+gramlib/.pack/gramlib__%: COND_OPENFLAGS=-open Gramlib
-gramlib__pack/gramlib.cma: $(GRAMOBJS) gramlib__pack/gramlib.cmo
+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
+gramlib/.pack/gramlib.cmxa: $(GRAMOBJS:.cmo=.cmx) gramlib/.pack/gramlib.cmx
$(SHOW)'OCAMLOPT -a -o $@'
$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $^
@@ -748,8 +748,8 @@ 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 gramlib__pack/% checker/% plugins/%, $(MLFILES) $(MLIFILES))
-MAINMLLIBFILES := $(filter-out gramlib__pack/% 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) $(GENGRAMFILES)
$(SHOW)'OCAMLDEP MLFILES MLIFILES'
diff --git a/Makefile.common b/Makefile.common
index ca2cb8fee6..a59fbe676e 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -91,7 +91,7 @@ MKDIR:=install -d
CORESRCDIRS:=\
coqpp \
config clib lib kernel kernel/byterun library \
- engine pretyping interp proofs gramlib__pack parsing printing \
+ engine pretyping interp proofs gramlib/.pack parsing printing \
tactics vernac stm toplevel
PLUGINDIRS:=\
@@ -119,7 +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 \
+ gramlib/.pack/gramlib.cma \
parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
stm/stm.cma toplevel/toplevel.cma
diff --git a/Makefile.install b/Makefile.install
index 8233807e03..b6e2ec2aeb 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -92,17 +92,20 @@ install-tools:
INSTALLCMI = $(sort \
$(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \
+ $(filter %.cmi, $(GRAMMLFILES:.mli=.cmi)) gramlib/.pack/gramlib.cmi \
$(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \
- $(PLUGINS:.cmo=.cmi) gramlib__pack/gramlib.cmi
+ $(PLUGINS:.cmo=.cmi)
INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% \
configure.cmx toplevel/coqtop_byte_bin.cmx plugins/extraction/big.cmx, \
- $(MLFILES:.ml=.cmx)))
+ $(filter %.cmx, $(GRAMMLFILES:.ml=.cmx)) $(MLFILES:.ml=.cmx)))
+
+foo:
+ @echo $(INSTALLCMX)
install-devfiles:
$(MKDIR) $(FULLBINDIR)
$(MKDIR) $(FULLCOQLIB)
- $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA)
$(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) # Regular CMI files
$(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMX) # To avoid warning 58 "-opaque"
$(INSTALLSH) $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.cmx) # For static linking of plugins
diff --git a/configure.ml b/configure.ml
index ec765acc15..2559e0a473 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1101,7 +1101,7 @@ let write_configml f =
pr_b "native_compiler" !prefs.nativecompiler;
let core_src_dirs = [ "config"; "lib"; "clib"; "kernel"; "library";
- "engine"; "pretyping"; "interp"; "gramlib__pack"; "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")
""
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index c1dcabb743..a11269e059 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -17,7 +17,7 @@ exec $OCAMLDEBUG \
-I +threads \
-I $COQTOP \
-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
- -I $COQTOP/gramlib__pack \
+ -I $COQTOP/gramlib/.pack \
-I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
-I $COQTOP/library -I $COQTOP/engine \
-I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:19:27 +0000