Merge PR #8632: [ide] [dune] [test-suite] Reorganize `fake_ide` build.

7 files changed, 52 insertions, 19 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 6aa2cecbd3..948e4f0a37 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -241,6 +241,7 @@ pkg:opam:
   script:
     - set -e
     - opam pin add coq .
+    - opam pin add coqide-server .
     - opam pin add coqide .
     - set +e
   variables:
diff --git a/Makefile.build b/Makefile.build
index 0faa18b059..ee758fcc5f 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -563,7 +563,7 @@ $(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/protocol/ideprotocol.cma ide/document.cmo tools/fake_ide.cmo
+FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo ide/fake_ide.cmo
 
 $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP)
 	$(SHOW)'OCAMLBEST -o $@'
@@ -668,7 +668,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 -I ide/protocol,)
+COND_IDEFLAGS=$(if $(filter ide/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,)
 COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,)
 
 COND_BYTEFLAGS= \
diff --git a/coqide-server.opam b/coqide-server.opam
new file mode 100644
index 0000000000..546ce75dbd
--- /dev/null
+++ b/coqide-server.opam
@@ -0,0 +1,16 @@
+opam-version: "1.2"
+maintainer: "The Coq development team <coqdev@inria.fr>"
+authors: "The Coq development team, INRIA, CNRS, and contributors."
+homepage: "https://coq.inria.fr/"
+bug-reports: "https://github.com/coq/coq/issues"
+dev-repo: "https://github.com/coq/coq.git"
+license: "LGPL-2.1"
+
+available: [ocaml-version >= "4.05.0"]
+
+depends: [
+  "dune"      { build & >= "1.2.0" }
+  "coq"
+]
+
+build: [ [ "dune" "build" "-p" name "-j" jobs ] ]
diff --git a/coqide.opam b/coqide.opam
index 897177b283..17fb5dbbe2 100644
--- a/coqide.opam
+++ b/coqide.opam
@@ -11,6 +11,7 @@ available: [ocaml-version >= "4.05.0"]
 depends: [
   "dune"               { build & >= "1.2.0" }
   "coq"
+  "coqide-server"
   "conf-gtksourceview"
   "lablgtk"            {         >= "2.18.5" }
 ]
diff --git a/ide/dune b/ide/dune
index 6931a747ac..037b0fcc9e 100644
--- a/ide/dune
+++ b/ide/dune
@@ -1,11 +1,34 @@
+; IDE Server
 (ocamllex utf8_convert config_lexer coq_lex)
 
 (library
  (name core)
- (public_name coqide.core)
+ (public_name coqide-server.core)
  (wrapped false)
- (modules (:standard \ idetop coqide_main))
- (libraries threads str lablgtk2.sourceview2 coq.lib coqide.protocol))
+ (modules document)
+ (libraries coq.lib))
+
+(executable
+ (name fake_ide)
+ (modules fake_ide)
+ (libraries coqide-server.protocol coqide-server.core))
+
+(executable
+ (name idetop)
+ (public_name coqidetop.opt)
+ (package coqide-server)
+ (modules idetop)
+ (libraries coq.toplevel coqide-server.protocol)
+ (link_flags -linkall))
+
+; IDE Client
+(library
+ (name gui)
+ (public_name coqide.gui)
+ (wrapped false)
+ (modules (:standard \ document fake_ide idetop coqide_main))
+ (optional)
+ (libraries coqide-server.protocol coqide-server.core lablgtk2.sourceview2))
 
 (rule
  (targets coqide_main.ml)
@@ -17,12 +40,4 @@
  (public_name coqide)
  (package coqide)
  (modules coqide_main)
- (libraries coqide.core))
-
-(executable
- (name idetop)
- (public_name coqidetop.opt)
- (package coqide)
- (modules idetop)
- (libraries coq.toplevel coqide.protocol)
- (link_flags -linkall))
+ (libraries coqide.gui))
diff --git a/tools/fake_ide.ml b/ide/fake_ide.ml
index 0162011289..521aff6bf6 100644
--- a/tools/fake_ide.ml
+++ b/ide/fake_ide.ml
@@ -195,9 +195,9 @@ module GUILogic = struct
         Document.unfocus doc;
         ignore(Document.cut_at doc tip);
         print_document ()
-  
+
   let at id id' _ = Stateid.equal id' id
-  
+
   let after_edit_at (id,need_unfocus) = function
     | Interface.Fail (_,_,s) -> print_error s; exit 1
     | Interface.Good (Util.Inl ()) ->
@@ -210,13 +210,13 @@ module GUILogic = struct
         Document.focus doc ~cond_top:(at start_id) ~cond_bot:(at stop_id);
         ignore(Document.cut_at doc id);
         print_document ()
-  
+
   let get_id_pred pred =
     try Document.find_id doc pred
     with Not_found -> error "No state found"
 
   let get_id id = get_id_pred (fun _ { name } -> name = id)
-  
+
   let after_fail coq = function
     | Interface.Fail (safe_id,_,s) ->
         prerr_endline "The command failed as expected";
diff --git a/ide/protocol/dune b/ide/protocol/dune
index 9ce4559940..801ceb20ec 100644
--- a/ide/protocol/dune
+++ b/ide/protocol/dune
@@ -1,6 +1,6 @@
 (library
  (name protocol)
- (public_name coqide.protocol)
+ (public_name coqide-server.protocol)
  (wrapped false)
  (libraries coq.lib))