aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-17 23:45:26 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-24 13:21:59 +0200
commit5a564f986b5dcb74e347fbdc571d9e1a9980c2a4 (patch)
tree0b056da1338cb98e07bfc2271e58054c7ec298d2 /Makefile.build
parent9392d7ed7c1dfe3ad2b3d6b0f5e039353fbd6517 (diff)
[ide] Move common protocol library to its own folder/object.
The `ide` folder contains two different binaries, the language server `coqidetop` and `coqide` itself. Even if these binaries are in the same folder, the only thing they have in common is that they link to the protocol files. In the OCaml world, having "doubly" linked files in the same project is considered a bit of an ugly practice, and some build tools such as Dune disallow it.q Thus, to clean up the build, we move the common protocol files to its own library `ideprotocol`. This helps towards Dune integration and towards having an IDE standalone target, such as the one that was implemented here: https://github.com/ejgallego/coqide-exp
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build11
1 files changed, 4 insertions, 7 deletions
diff --git a/Makefile.build b/Makefile.build
index 7454e1b0c..036a3126b 100644
--- a/Makefile.build
+++ b/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/utils)
+DEPFLAGS=$(LOCALINCLUDES)$(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)
@@ -551,14 +551,11 @@ $(COQWORKMGRBYTE): $(COQWORKMGRCMO)
# fake_ide : for debugging or test-suite purpose, a fake ide simulating
# a connection to coqidetop
-FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/document.cmo \
- ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo \
- ide/xml_printer.cmo ide/richpp.cmo ide/xmlprotocol.cmo \
- tools/fake_ide.cmo
+FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo tools/fake_ide.cmo
$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP)
$(SHOW)'OCAMLBEST -o $@'
- $(HIDE)$(call bestocaml, -I ide -package str -package dynlink)
+ $(HIDE)$(call bestocaml, -I ide -I ide/protocol -package str -package dynlink)
$(FAKEIDEBYTE): $(FAKEIDECMO) | $(IDETOPLOOPCMA)
$(SHOW)'OCAMLC -o $@'
@@ -659,7 +656,7 @@ kernel/kernel.cmxa: kernel/kernel.mllib
$(SHOW)'OCAMLOPT -pack -o $@'
$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
-COND_IDEFLAGS=$(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,)
+COND_IDEFLAGS=$(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,)
COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,)
COND_BYTEFLAGS= \