diff --git a/.gitignore b/.gitignore
index c4b33fc92e226858a5f4fb5a212f2a87ea822bb4..72f531eeb2b3c76d1b79515b7d7218802d2dd42b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -121,8 +121,10 @@ why3.conf
 /doc/stdlibdoc/
 
 # /lib
-/lib/why3-cpulimit
-/lib/why3-cpulimit.exe
+/lib/why3cpulimit
+/lib/why3cpulimit.exe
+/lib/why3server
+/lib/why3server.exe
 
 # /lib/why3/
 /lib/why3/META
diff --git a/Makefile.in b/Makefile.in
index 61bed57f5e66ef0dd82d3dd1a0694a568b2ee3c2..1f0cc0afb64ffaed51cf42cd65c11e20dc82b9f3 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -248,7 +248,7 @@ opt:  lib/why3/why3.cmxa
 
 lib/why3/why3.cma: lib/why3/why3.cmo
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
-	    $(OCAMLC)  -a $(BFLAGS) -o $@ $^
+	    $(OCAMLC) -a $(BFLAGS) -o $@ $^
 
 lib/why3/why3.cmxa: lib/why3/why3.cmx
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
@@ -614,46 +614,38 @@ clean::
 # Why3server #
 ##############
 
-SERVER_MODULES:= logging arraylist options queue readbuf request writebuf server_main
-SERVER_C:= $(addprefix src/tools/, $(addsuffix .c, $(SERVER_MODULES)))
-SERVER_H:= $(addprefix src/tools/, $(addsuffix .h, $(SERVER_MODULES)))
-SERVER_O:= $(addprefix src/tools/, $(addsuffix .o, $(SERVER_MODULES)))
+SERVER_MODULES := logging arraylist options queue readbuf request \
+		  writebuf server-unix server-win
+
+CPULIM_MODULES := cpulimit-unix cpulimit-win
+
+SERVER_O := $(addprefix src/server/, $(addsuffix .o, $(SERVER_MODULES)))
+
+CPULIM_O := $(addprefix src/server/, $(addsuffix .o, $(CPULIM_MODULES)))
 
-opt: lib/why3server$(EXE)
+TOOLS = lib/why3server$(EXE) lib/why3cpulimit$(EXE)
+
+byte opt: $(TOOLS)
 
 lib/why3server$(EXE): $(SERVER_O)
-	gcc -o $@ $^
+	$(CC) -Wall -o $@ $^
+
+lib/why3cpulimit$(EXE): $(CPULIM_O)
+	$(CC) -Wall -o $@ $^
 
 %.o: %.c %.h
-	gcc -c -Wall -g -o $@ $<
-%.o: %.c
-	gcc -c -Wall -g -o $@ $<
+	$(CC) -c -Wall -g -o $@ $<
 
-src/tools/main.o:: src/tools/server-unix.c src/tools/server-win.c
+%.o: %.c
+	$(CC) -c -Wall -g -o $@ $<
 
 install_no_local::
 	cp -f lib/why3server$(EXE) $(LIBDIR)/why3/why3server$(EXE)
+	cp -f lib/why3cpulimit$(EXE) $(LIBDIR)/why3/why3cpulimit$(EXE)
+	cp -f lib/why3-call-pvs $(LIBDIR)/why3/why3-call-pvs
 
 clean::
-	 rm -f $(SERVER_O)
-
-install_spark2014:
-	mkdir -p $(BINDIR)
-	mkdir -p $(DATADIR)/why3
-	mkdir -p $(DATADIR)/why3/theories
-	mkdir -p $(DATADIR)/why3/drivers
-	mkdir -p $(DATADIR)/why3/modules
-	mkdir -p $(DATADIR)/why3/libs
-	cp -f theories/*.why $(DATADIR)/why3/theories
-	cp -f modules/*.mlw $(DATADIR)/why3/modules
-	cp -f drivers/*.drv drivers/*.gen drivers/*.aux $(DATADIR)/why3/drivers
-	cp -f share/why3session.dtd $(DATADIR)/why3
-	cp -f lib/why3server$(EXE) $(BINDIR)/why3server$(EXE)
-	cp -f bin/gnatwhy3.@OCAMLBEST@ $(BINDIR)/gnatwhy3$(EXE)
-	cp -f bin/why3realize.@OCAMLBEST@ $(BINDIR)/why3realize$(EXE)
-	cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config$(EXE)
-	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
-	cp -rf lib/coq $(DATADIR)/why3/libs
+	rm -f $(SERVER_O) $(CPULIM_O) $(TOOLS)
 
 ##########
 # gallery
@@ -873,7 +865,7 @@ lib/coq-tactic/why3tac.cmxs: lib/why3/why3.cmxa $(COQPCMX)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
 
-lib/coq-tactic/why3tac.cma: src/driver/vc_client.o lib/why3/why3.cma $(COQPCMO)
+lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLC) -a $(BFLAGS) -o $@ $^
 
@@ -1442,24 +1434,6 @@ clean::
 
 endif
 
-#######
-# tools
-#######
-
-TOOLS = lib/why3-cpulimit$(EXE)
-
-byte opt: $(TOOLS)
-
-lib/why3-cpulimit$(EXE): src/tools/@CPULIMIT@.c
-	$(CC) -Wall -o $@ $^
-
-clean::
-	rm -f lib/why3-cpulimit$(EXE)
-
-install_no_local::
-	cp -f lib/why3-cpulimit$(EXE) $(LIBDIR)/why3/why3-cpulimit$(EXE)
-	cp -f lib/why3-call-pvs $(LIBDIR)/why3/why3-call-pvs
-
 #########
 # why3doc
 #########
diff --git a/configure.in b/configure.in
index a37d8f97641e252e68ff4fa815c8620c652fa31e..872a0d6e73b483c88d7f2a7209ac6dbfcf4d9f4d 100644
--- a/configure.in
+++ b/configure.in
@@ -140,18 +140,15 @@ AC_MSG_CHECKING(executable suffix)
 if uname -s | grep -q CYGWIN ; then
   EXE=.exe
   STRIP='echo "no strip "'
-  CPULIMIT=cpulimit-win
   AC_MSG_RESULT(.exe <Cygwin>)
 else
 if uname -s | grep -q MINGW ; then
   EXE=.exe
   STRIP=strip
-  CPULIMIT=cpulimit-win
   AC_MSG_RESULT(.exe <MinGW>)
 else
   EXE=
   STRIP=strip
-  CPULIMIT=cpulimit
   AC_MSG_RESULT(<none>)
 fi
 fi
@@ -719,7 +716,6 @@ AC_SUBST(enable_verbose_make)
 
 AC_SUBST(EXE)
 AC_SUBST(STRIP)
-AC_SUBST(CPULIMIT)
 
 AC_SUBST(OCAMLC)
 AC_SUBST(OCAMLOPT)
diff --git a/src/driver/call_provers.ml b/src/driver/call_provers.ml
index f4fcac9f422ac1ed87343f7c0cf743cbbd13eb78..d4c8bb220e3a3c119abdfa520e29957e4556362d 100644
--- a/src/driver/call_provers.ml
+++ b/src/driver/call_provers.ml
@@ -267,7 +267,7 @@ let actualcommand command ~use_why3cpulimit limit interactive file =
   in
   let args =
     if use_why3cpulimit && not interactive then
-      let cpulimit_bin = Filename.concat Config.libdir "why3-cpulimit" in
+      let cpulimit_bin = Filename.concat Config.libdir "why3cpulimit" in
       let cpulimit_time =
         (* for steps limit use 2 * t + 1 time *)
         if limit.limit_steps <> None then string_of_int (2 * timelimit + 1)
diff --git a/src/driver/prove_client.ml b/src/driver/prove_client.ml
index 2bcfa1a704962d165ec25044e06e816928d69f99..b13b7961402b1c7bf3b3b84bdbb073257bd76105 100644
--- a/src/driver/prove_client.ml
+++ b/src/driver/prove_client.ml
@@ -76,9 +76,9 @@ let run_server () =
 let force_connect () =
   match !socket with
   | None when !standalone ->
-      run_server ();
-      (* sleep is needed before connecting, or the server will not be ready
-         yet *)
+      let _pid = run_server () in
+      (* sleep is needed before connecting,
+         or the server will not be ready yet *)
       ignore (Unix.select [] [] [] 0.1);
       connect()
   | _ -> ()
diff --git a/src/tools/server_main.c b/src/server/README.server
similarity index 96%
rename from src/tools/server_main.c
rename to src/server/README.server
index 7e103bd67959e461e85e3ff96232be186c742168..4baa3439d9e87e023214594a235e9fbdcb9ce916 100644
--- a/src/tools/server_main.c
+++ b/src/server/README.server
@@ -48,9 +48,3 @@
 // events are incoming clients, read/write operations on sockets, and
 // terminating child processes. Lists of child processes and connected clients
 // are maintained.
-
-#ifdef _WIN32
-# include "server-win.c"
-#else
-# include "server-unix.c"
-#endif
diff --git a/src/tools/arraylist.c b/src/server/arraylist.c
similarity index 100%
rename from src/tools/arraylist.c
rename to src/server/arraylist.c
diff --git a/src/tools/arraylist.h b/src/server/arraylist.h
similarity index 100%
rename from src/tools/arraylist.h
rename to src/server/arraylist.h
diff --git a/src/tools/cpulimit.c b/src/server/cpulimit-unix.c
similarity index 99%
rename from src/tools/cpulimit.c
rename to src/server/cpulimit-unix.c
index 8f91269ec2f117c38ecd6a50402c594e2ab01615..c9102e3d0ed1b24ea37662b5be4a6b589704c8dd 100644
--- a/src/tools/cpulimit.c
+++ b/src/server/cpulimit-unix.c
@@ -9,6 +9,8 @@
 /*                                                                  */
 /********************************************************************/
 
+#ifndef _WIN32
+
 #include <sys/types.h>
 #include <sys/time.h>
 #include <time.h>
@@ -145,3 +147,5 @@ int main(int argc, char *argv[]) {
   return EXIT_FAILURE;
 
 }
+
+#endif /* _WIN32 */
diff --git a/src/tools/cpulimit-win.c b/src/server/cpulimit-win.c
similarity index 99%
rename from src/tools/cpulimit-win.c
rename to src/server/cpulimit-win.c
index 72e91d81a4408e85a57ee5f4c7e8aa2c7e558c7e..242b50721b84ae11daecb27ae94920c300ed6b7b 100644
--- a/src/tools/cpulimit-win.c
+++ b/src/server/cpulimit-win.c
@@ -17,6 +17,8 @@
 
 /* $Id: cpulimit-win.c,v 1.3 2009-12-09 08:28:00 nrousset Exp $ */
 
+#ifdef _WIN32
+
 #include <windows.h>
 #include <stdlib.h>
 #include <stdio.h>
@@ -203,5 +205,7 @@ int main(int argc, char *argv[]) {
   return ex;
 }
 
+#endif /* _WIN32 */
+
 // How to compile under Cygwin (needs make, gcc and win32api):
 //                 gcc -Wall -o cpulimit cpulimit.c
diff --git a/src/tools/logging.c b/src/server/logging.c
similarity index 100%
rename from src/tools/logging.c
rename to src/server/logging.c
diff --git a/src/tools/logging.h b/src/server/logging.h
similarity index 100%
rename from src/tools/logging.h
rename to src/server/logging.h
diff --git a/src/tools/options.c b/src/server/options.c
similarity index 100%
rename from src/tools/options.c
rename to src/server/options.c
diff --git a/src/tools/options.h b/src/server/options.h
similarity index 100%
rename from src/tools/options.h
rename to src/server/options.h
diff --git a/src/tools/queue.c b/src/server/queue.c
similarity index 100%
rename from src/tools/queue.c
rename to src/server/queue.c
diff --git a/src/tools/queue.h b/src/server/queue.h
similarity index 100%
rename from src/tools/queue.h
rename to src/server/queue.h
diff --git a/src/tools/readbuf.c b/src/server/readbuf.c
similarity index 100%
rename from src/tools/readbuf.c
rename to src/server/readbuf.c
diff --git a/src/tools/readbuf.h b/src/server/readbuf.h
similarity index 100%
rename from src/tools/readbuf.h
rename to src/server/readbuf.h
diff --git a/src/tools/request.c b/src/server/request.c
similarity index 100%
rename from src/tools/request.c
rename to src/server/request.c
diff --git a/src/tools/request.h b/src/server/request.h
similarity index 100%
rename from src/tools/request.h
rename to src/server/request.h
diff --git a/src/tools/server-unix.c b/src/server/server-unix.c
similarity index 99%
rename from src/tools/server-unix.c
rename to src/server/server-unix.c
index 12b55ad241cd4cb5af50e0d384e6b01787172bda..aa5b601b2627947df78aff304fe68a6ce9b6168b 100644
--- a/src/tools/server-unix.c
+++ b/src/server/server-unix.c
@@ -5,6 +5,8 @@
 // Contrary to the situation on windows, e.g. a read event means that the next
 // call to read() will not block.
 
+#ifndef _WIN32
+
 #include <sys/types.h>
 #include <unistd.h>
 #include <stdio.h>
@@ -544,3 +546,5 @@ int main(int argc, char **argv) {
     }
   }
 }
+
+#endif /* _WIN32 */
diff --git a/src/tools/server-win.c b/src/server/server-win.c
similarity index 99%
rename from src/tools/server-win.c
rename to src/server/server-win.c
index 1a6448bd25b15350736f05de975210ab85ce2f17..3b04168fa8546413b155c0966438800f6a9faaaf 100644
--- a/src/tools/server-win.c
+++ b/src/server/server-win.c
@@ -5,6 +5,8 @@
 // windows: you need to start them first, and get notified when they are
 // terminated.
 
+#ifdef _WIN32
+
 #include <windows.h>
 #include <stdio.h>
 #include <stdlib.h>
@@ -648,3 +650,5 @@ int main(int argc, char **argv) {
       }
    }
 }
+
+#endif /* _WIN32 */
diff --git a/src/tools/writebuf.c b/src/server/writebuf.c
similarity index 100%
rename from src/tools/writebuf.c
rename to src/server/writebuf.c
diff --git a/src/tools/writebuf.h b/src/server/writebuf.h
similarity index 100%
rename from src/tools/writebuf.h
rename to src/server/writebuf.h