[ide] [dune] [test-suite] Reorganize fake_ide build.

Even if `fake_ide` was under tools, it depended on libraries from
`ide`. Thus, we move `fake_ide` to `ide`, and make it "private" to the
test-suite [this means `test-suite` depends on the `ide` folder then].

In the Dune side, we reorganize libraries so `fake_ide` doesn't depend
on GTK anymore, this allows to run the test-suite when GTK is not
available.

In order to achieve this, we had to split the `coqide` package in a
server and client version.

.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:

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= \

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 ] ]

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" }
 ]

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))

tools/fake_ide.ml → 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";

ide/protocol/dune

@@ -1,6 +1,6 @@
 (library
  (name protocol)
- (public_name coqide.protocol)
+ (public_name coqide-server.protocol)
  (wrapped false)
  (libraries coq.lib))