From 92dd9a78d6c40f80ca3b9b37e8c8184261060ea3 Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Tue, 5 Apr 2016 11:35:35 +0200 Subject: [PATCH] move the server code to a dedicated directory also, do not use server_main.c, compile both .o instead --- .gitignore | 6 +- Makefile.in | 72 ++++++------------- configure.in | 4 -- src/driver/call_provers.ml | 2 +- src/driver/prove_client.ml | 6 +- .../server_main.c => server/README.server} | 6 -- src/{tools => server}/arraylist.c | 0 src/{tools => server}/arraylist.h | 0 .../cpulimit.c => server/cpulimit-unix.c} | 4 ++ src/{tools => server}/cpulimit-win.c | 4 ++ src/{tools => server}/logging.c | 0 src/{tools => server}/logging.h | 0 src/{tools => server}/options.c | 0 src/{tools => server}/options.h | 0 src/{tools => server}/queue.c | 0 src/{tools => server}/queue.h | 0 src/{tools => server}/readbuf.c | 0 src/{tools => server}/readbuf.h | 0 src/{tools => server}/request.c | 0 src/{tools => server}/request.h | 0 src/{tools => server}/server-unix.c | 4 ++ src/{tools => server}/server-win.c | 4 ++ src/{tools => server}/writebuf.c | 0 src/{tools => server}/writebuf.h | 0 24 files changed, 47 insertions(+), 65 deletions(-) rename src/{tools/server_main.c => server/README.server} (96%) rename src/{tools => server}/arraylist.c (100%) rename src/{tools => server}/arraylist.h (100%) rename src/{tools/cpulimit.c => server/cpulimit-unix.c} (99%) rename src/{tools => server}/cpulimit-win.c (99%) rename src/{tools => server}/logging.c (100%) rename src/{tools => server}/logging.h (100%) rename src/{tools => server}/options.c (100%) rename src/{tools => server}/options.h (100%) rename src/{tools => server}/queue.c (100%) rename src/{tools => server}/queue.h (100%) rename src/{tools => server}/readbuf.c (100%) rename src/{tools => server}/readbuf.h (100%) rename src/{tools => server}/request.c (100%) rename src/{tools => server}/request.h (100%) rename src/{tools => server}/server-unix.c (99%) rename src/{tools => server}/server-win.c (99%) rename src/{tools => server}/writebuf.c (100%) rename src/{tools => server}/writebuf.h (100%) diff --git a/.gitignore b/.gitignore index c4b33fc92..72f531eeb 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 61bed57f5..1f0cc0afb 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 a37d8f976..872a0d6e7 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 ) else if uname -s | grep -q MINGW ; then EXE=.exe STRIP=strip - CPULIMIT=cpulimit-win AC_MSG_RESULT(.exe ) else EXE= STRIP=strip - CPULIMIT=cpulimit AC_MSG_RESULT() 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 f4fcac9f4..d4c8bb220 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 2bcfa1a70..b13b79614 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 7e103bd67..4baa3439d 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 8f91269ec..c9102e3d0 100644 --- a/src/tools/cpulimit.c +++ b/src/server/cpulimit-unix.c @@ -9,6 +9,8 @@ /* */ /********************************************************************/ +#ifndef _WIN32 + #include #include #include @@ -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 72e91d81a..242b50721 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 #include #include @@ -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 12b55ad24..aa5b601b2 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 #include #include @@ -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 1a6448bd2..3b04168fa 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 #include #include @@ -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 -- GitLab