From f3a7d021e6b347c2c0edf3c07f3206f22dcdf39a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Dec 2018 14:58:15 +0100 Subject: unignore Makefile.install Relevant for gitignore aware tools like ag (silversearcher) --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index da675309e5..8b81037a14 100644 --- a/.gitignore +++ b/.gitignore @@ -178,3 +178,4 @@ theories/*/dune theories/*/*/dune theories/*/*/*/dune *.install +!Makefile.install -- cgit v1.2.3 From e3a2a5d4fc3ad29462f2e4548c32ac00b4fbd05f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 26 Nov 2018 15:04:09 +0100 Subject: Rename generated directory gramlib__pack -> gramlib/.pack It's a bit cleaner this way, especially wrt the number of toplevel directories. Also fix warning about undefined GRAMMARCMA while we're at it. --- .gitignore | 3 +-- .merlin.in | 4 ++-- META.coq.in | 2 +- Makefile | 8 ++++---- Makefile.build | 26 +++++++++++++------------- Makefile.common | 4 ++-- Makefile.install | 9 ++++++--- configure.ml | 2 +- dev/ocamldebug-coq.run | 2 +- 9 files changed, 31 insertions(+), 29 deletions(-) diff --git a/.gitignore b/.gitignore index 8b81037a14..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 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 \ -- cgit v1.2.3