Commit f682fef1 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'getopt' into 'master'

Make the parsing of command line getopt-compliant.

See merge request !157
parents 3c843538 12704b1f
......@@ -273,8 +273,6 @@ pvsbin/
/examples/*/*.tex
/examples/*/*/*.tex
/examples/*/*/*/*.tex
/examples/use_api/runstrat/makejob.opt
/examples/use_api/runstrat/runstrat.opt
/examples/vstte10_max_sum/vstte10_max_sum.ml
/examples/euler001/euler001.ml
/examples/sudoku/sudoku.ml
......
......@@ -219,7 +219,7 @@ LIBGENERATED = src/util/config.ml \
LIB_UTIL = config bigInt mlmpfr_wrapper util opt lists strings \
pp extmap extset exthtbl weakhtbl diffmap \
hashcons wstdlib exn_printer \
hashcons wstdlib exn_printer getopt \
json_base json_parser json_lexer \
debug loc lexlib print_tree \
cmdline warning sysutil rc plugin bigInt number constant vector pqueue
......@@ -619,8 +619,8 @@ bin/why3realize.opt: $(WHY3CMXA) src/tools/why3realize.cmx
bin/why3realize.byte: $(WHY3CMA) src/tools/why3realize.cmo
bin/why3replay.opt: $(WHY3CMXA) src/tools/why3replay.cmx
bin/why3replay.byte: $(WHY3CMA) src/tools/why3replay.cmo
bin/why3wc.opt: src/tools/why3wc.cmx
bin/why3wc.byte: src/tools/why3wc.cmo
bin/why3wc.opt: $(WHY3CMXA) src/tools/why3wc.cmx
bin/why3wc.byte: $(WHY3CMA) src/tools/why3wc.cmo
uninstall-bin::
rm -f $(BINDIR)/why3$(EXE)
......@@ -1809,9 +1809,6 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
@echo ""
@echo "=== Checking extraction ==="
$(MAKE) test-ocaml-extraction
# desactivé car requiert findlib
# if test -d examples/runstrat ; then \
# $(MAKE) test-runstrat.@OCAMLBEST@ ; fi
bench-api:
@echo ""
......@@ -1950,17 +1947,6 @@ test-ce.opt: examples/use_api/counterexample.ml lib/why3/why3.cmxa
printf "Test of Why3 API calls for counterexamples failed. Please fix it"; exit 2)
@rm -f test-ce.opt why3session.xml why3shapes why3shapes.gz
#only test the compilation of runstrat
test-runstrat.byte: lib/why3/why3.cma lib/why3/META
OCAMLPATH=$(PWD)/lib $(MAKE) -C examples/use_api/runstrat clean
OCAMLPATH=$(PWD)/lib $(MAKE) -C examples/use_api/runstrat byte
test-runstrat.opt: lib/why3/why3.cmxa lib/why3/META
OCAMLPATH=$(PWD)/lib $(MAKE) -C examples/use_api/runstrat clean
OCAMLPATH=$(PWD)/lib $(MAKE) -C examples/use_api/runstrat opt
test-runstrat: test-runstrat.@OCAMLBEST@
test-ocaml-extraction: bin/why3.opt bin/why3extract.opt
@echo "driver ocaml64"
@bin/why3extract.opt -D ocaml64 -L tests \
......@@ -2035,7 +2021,7 @@ endif
.PHONY: apidoc apidot
MODULESTODOC = \
util/util util/opt util/lists util/strings \
util/util util/opt util/lists util/strings util/getopt \
util/extmap util/extset util/exthtbl \
util/weakhtbl util/wstdlib util/rc util/debug \
util/loc util/pp util/bigInt util/number \
......@@ -2147,7 +2133,7 @@ stdlibdoc: $(STDLIBFILES) bin/why3doc.@OCAMLBEST@
sed -e "s/use Int/use int.Int/" stdlib/int.mlw > int.mlw
rm -f doc/stdlibdoc/style.css
WHY3CONFIG="" bin/why3doc.@OCAMLBEST@ $(LOCAL_STDLIB) \
-o doc/stdlibdoc --title "Why3 Standard Library" \
-o doc/stdlibdoc --title="Why3 Standard Library" \
$(subst stdlib/int.mlw,int.mlw,$(STDLIBFILES))
rm int.mlw
cd doc/stdlibdoc; \
......
......@@ -104,9 +104,9 @@ drivers () {
if [[ $f == drivers/cakeml.drv ]]; then continue; fi
printf " $f... "
# running Why
if ! echo "theory Test goal G : 1=2 end" | $pgm -F whyml --driver $f - > /dev/null; then
if ! echo "theory Test goal G : 1=2 end" | $pgm -F whyml --driver=$f - > /dev/null; then
echo "why FAILED"
echo "theory Test goal G : 1=2 end" | $pgm -F whyml --driver $f -
echo "theory Test goal G : 1=2 end" | $pgm -F whyml --driver=$f -
exit 1
fi
echo "ok"
......@@ -321,7 +321,7 @@ goods bench/typing/x-good --parse-only
bads bench/typing/x-good --type-only
goods bench/programs/good
goods bench/ce
goods src/trywhy3/examples "--debug ignore_missing_diverges"
goods src/trywhy3/examples "--debug=ignore_missing_diverges"
goods examples/bts
goods examples/tests
goods examples/tests-provers
......@@ -337,7 +337,7 @@ goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_201
goods examples/double_wp "-L examples/double_wp"
goods examples/in_progress/ring_decision "-L examples/in_progress/ring_decision"
goods examples/multiprecision "-L examples/multiprecision"
goods examples/prover "-L examples/prover --debug ignore_unused_vars"
goods examples/prover "-L examples/prover --debug=ignore_unused_vars"
goods examples/in_progress
plugins tests/python --type-only py
plugins tests/microc --type-only c
......@@ -452,7 +452,7 @@ replay examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_20
replay examples/double_wp "-L examples/double_wp --merging-only"
#replay examples/in_progress/ring_decision "-L examples/in_progress/ring_decision --merging-only"
replay examples/multiprecision "-L examples/multiprecision --merging-only"
replay examples/prover "-L examples/prover --merging-only --debug ignore_unused_vars"
replay examples/prover "-L examples/prover --merging-only --debug=ignore_unused_vars"
#replay examples/in_progress --merging-only
echo ""
......
......@@ -100,11 +100,11 @@ run () {
else
f="${file_path}_$1_SP"
oracle_file="$2/oracles/$3_$1_SP.oracle"
wp_sp=" --debug vc_sp"
wp_sp=" --debug=vc_sp"
echo "Strongest Postcondition" > "$f.out"
printf "Strongest Postcondition ${file_path} ($1)... "
fi
$dir/../bin/why3prove.opt --json --debug print_model_attrs${wp_sp} -P "$1,counterexamples" --timelimit 1 -a split_vc "${file_path}.mlw" | \
$dir/../bin/why3prove.opt --json --debug=print_model_attrs${wp_sp} -P "$1,counterexamples" --timelimit=1 -a split_vc "${file_path}.mlw" | \
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
sed 's/ ([0-9]\+\.[0-9]\+s)//' | \
......
......@@ -32,7 +32,7 @@ run () {
file_path="$1/$2"
oracle_file="$1/oracles/$2.oracle"
echo "$file_path"
xvfb-run -a bin/why3ide --batch "down;down;type split_vc;wait 1;down;down;color;" "${file_path}.mlw" > "${file_path}.out"
xvfb-run -a bin/why3ide --batch="down;down;type split_vc;wait 1;down;down;color;" "${file_path}.mlw" > "${file_path}.out"
str_oracle=$(tr -d ' \n' < "${oracle_file}")
str_out=$(tr -d ' \n' < "${file_path}.out")
if [ "$str_oracle" = "$str_out" ] ; then
......
......@@ -59,15 +59,15 @@ needed.
The commands accept a common subset of command-line options. In
particular, option :option:`--help` displays the usage and options.
.. option:: -L <dir>, --library <dir>
.. option:: -L <dir>, --library=<dir>
Add ``<dir>`` in the load path, to search for theories.
.. option:: -C <file>, --config <file>
.. option:: -C <file>, --config=<file>
Read the configuration from the given file. See :numref:`sec.whyconffile`.
.. option:: --extra-config <file>
.. option:: --extra-config=<file>
Read additional configuration from the given file.
......@@ -99,9 +99,9 @@ particular, option :option:`--help` displays the usage and options.
Set all debug flags (except flags that change the behavior).
.. option:: --debug <flag>
.. option:: --debug=<flag>,...
Set a specific debug flag.
Set some specific debug flags.
.. option:: --help
......@@ -164,7 +164,7 @@ Options
Imply both :option:`--detect-provers` and :option:`--detect-plugins`.
Also reset the loadpath.
.. option:: --add-prover <id> <shortcut> <file>
.. option:: --add-prover=<id>,<shortcut>,<file>
Check the executable program ``<file>`` against the provers of family
``<id>``, and register it as ``<shortcut>``.
......@@ -174,7 +174,7 @@ Options
::
why3 config --add-prover alt-ergo new-ae /home/me/bin/alt-ergo-trunk
why3 config --add-prover=alt-ergo,new-ae,/home/me/bin/alt-ergo-trunk
.. option:: --list-prover-families
......@@ -259,35 +259,35 @@ Invalid
Options
~~~~~~~
.. option:: -F <format>, --format <format>
.. option:: -F <format>, --format=<format>
Select the given input format.
.. option:: -T <theory>, --theory <theory>
.. option:: -T <theory>, --theory=<theory>
Focus on the given theory. If the argument is not qualified, the
theory is searched in the input file.
.. option:: -G <goal>, --goal <goal>
.. option:: -G <goal>, --goal=<goal>
Focus on the given goal. The goal is searched in the theory given
by :option:`--theory`, if any. Otherwise, it is searched in the
toplevel namespace of the input file.
.. option:: -a <transform>, --apply-transform <transform>
.. option:: -a <transform>, --apply-transform=<transform>
Apply the given transformation to the goals.
.. option:: -P <prover>, --prover <prover>
.. option:: -P <prover>, --prover=<prover>
Execute the given prover on the goals.
.. option:: -D <driver>, --driver <driver>
.. option:: -D <driver>, --driver=<driver>
Output the tasks obtained by applying the given driver to the goals.
This option conflicts with :option:`--prover`.
.. option:: --extra-expl-prefix <s>
.. option:: --extra-expl-prefix=<s>
Specify *s* as an additional prefix for labels that denotes VC
explanations. The option can be used several times to specify
......@@ -318,7 +318,7 @@ detailed in introduction to this chapter, plus the specific option
already described for the :why3:tool:`prove` command in
:numref:`sec.proveoptions`.
.. .. option:: --extra-expl-prefix <s>
.. .. option:: --extra-expl-prefix=<s>
At least one anonymous argument must be specified on the command line.
More precisely, the first anonymous argument must be the directory of
......@@ -740,11 +740,8 @@ displayed in the *Counterexample* tab of the bottom right window, this time inte
with the code, as shown in :numref:`fig.ce_example0_p2`.
.. %%Generation of the screenshots:
.. %%Those commands follow the style of starting.tex. To execute them one needs to
.. %%do make update-doc-png.
.. %EXECUTE bin/why3 ide --batch "down;down;type cvc4;wait 2;down;snap -crop 1024x600+0+0 doc/images/ce_example0_p1.png" doc/cedoc.mlw
.. %EXECUTE bin/why3 ide --batch "down;down;type cvc4;wait 2;down;type get-ce;wait 2;down;faketype get-ce;snap -crop 1024x600+0+0 doc/images/ce_example0_p2.png" doc/cedoc.mlw
.. %EXECUTE bin/why3 ide --batch="down;down;type cvc4;wait 2;down;snap -crop 1024x600+0+0 doc/images/ce_example0_p1.png" doc/cedoc.mlw
.. %EXECUTE bin/why3 ide --batch="down;down;type cvc4;wait 2;down;type get-ce;wait 2;down;faketype get-ce;snap -crop 1024x600+0+0 doc/images/ce_example0_p2.png" doc/cedoc.mlw
.. _fig.ce_example0_p1:
......@@ -909,11 +906,11 @@ Options are:
Replay the proofs only if the session contains obsolete proof
attempts.
.. option:: --smoke-detector {none|top|deep}
.. option:: --smoke-detector[=none|top|deep]
Try to detect if the context is self-contradicting.
Try to detect if the context is self-contradicting (default: top).
.. option:: --prover <prover>
.. option:: --prover=<prover>
Restrict the replay to the selected provers only.
......@@ -1114,24 +1111,24 @@ tabular environment in LaTeX, one tabular for each theory, one per file.
The specific options are
.. option:: -style <n>
.. option:: --style=<n>
set output style (1 or 2, default 1) Option ``-style 2`` produces
Set output style (1 or 2, default 1). Option ``--style=2`` produces
an alternate version of LaTeX output, with a different layout of the
tables.
.. option:: -o <dir>
indicate where to produce LaTeX files (default: the session
Indicate where to produce LaTeX files (default: the session
directory).
.. option:: -longtable
.. option:: --longtable
use the ‘longtable’ environment instead of ‘tabular’.
Use the ``longtable`` environment instead of ``tabular``.
.. option :: -e <elem>
produce a table for the given element, which is either a file, a
Produce a table for the given element, which is either a file, a
theory or a root goal. The element must be specified using its path
in dot notation, e.g., ``file.theory.goal``. The file produced is named
accordingly, e.g., :file:`file.theory.goal.tex`. This option can be given
......@@ -1225,10 +1222,10 @@ HTML tags such as ``<ul>`` and ``<li>``.
Specific options for this command are as follows.
.. option:: --style <style>
.. option:: --style=[simpletree|table]
Set the style to use, among ``simpletree`` and ``table``; defaults
to ``table``.
Set the style to use, among ``simpletree`` and ``table`` (default:
``table``).
.. option:: -o <dir>
......@@ -1243,7 +1240,7 @@ Specific options for this command are as follows.
directory all the needed external files. It is incompatible with stdout
output.
.. option:: --add_pp <suffix> <cmd> <out_suffix>
.. option:: --add_pp=<suffix>,<cmd>,<out_suffix>
Set a specific pretty-printer for files with the given suffix.
Produced files use *<out_suffix>* as suffix. *<cmd>* must
......@@ -1253,7 +1250,7 @@ Specific options for this command are as follows.
.. option:: --coqdoc
use the :program:`coqdoc` command to display Coq proof scripts. This is
equivalent to ``--add_pp .v coqdoc --no-index --html -o %o %i .html``
equivalent to ``--add_pp=.v,coqdoc --no-index --html -o %o %i,.html``
.. why3:tool:: session update
......@@ -1265,7 +1262,7 @@ Command ``update``
The :program:`why3 session update` command permits to modify the session
contents, depending on the following specific options.
.. option:: -rename-file <src> <dst>
.. option:: --rename-file=<src>:<dst>
rename the file *<src>* to *<dst>* in the session. The file *<src>*
itself is also renamed to *<dst>* in your filesystem.
......@@ -1299,7 +1296,7 @@ identifier use to its definition.
Options
~~~~~~~
.. option:: -o <dir>, --output <dir>
.. option:: -o <dir>, --output=<dir>
Define the directory where to output the HTML files.
......@@ -1312,11 +1309,11 @@ Options
Prevent the generation of an index file.
.. option:: --title <title>
.. option:: --title=<title>
Set title of the index page.
.. option:: --stdlib-url <url>
.. option:: --stdlib-url=<url>
Set a URL for files found in load path, so that links to
definitions can be added.
......@@ -1354,7 +1351,7 @@ output is specified using the ``--output`` option.
::
why3 pp [--output=latex|mlw|dep] [--kind=inductive] [--prefix <prefix>] \
why3 pp [--output=latex|mlw|dep] [--kind=inductive] [--prefix=<prefix>] \
<filename> <file>[.<Module>].<ind_type> ...
.. option:: --output=<output>
......@@ -1460,7 +1457,7 @@ symbol, in order to state where to look for file :file:`f.mlw`.
Output extracted code to the given file (for :option:`--flat`) or
directory (for :option:`--modular`).
.. option:: -D <driver>, --driver <driver>
.. option:: -D <driver>, --driver=<driver>
Use the given driver.
......
......@@ -40,7 +40,7 @@ and check the validity of goals with external provers, in a friendly
way. This section presents the basic use of this GUI. Please refer to
:numref:`sec.ideref` for a more complete description.
.. %EXECUTE bin/why3 ide --batch "snap doc/images/gui-1.png" doc/hello_proof.why
.. %EXECUTE bin/why3 ide --batch="snap doc/images/gui-1.png" doc/hello_proof.why
.. _fig.gui1:
......@@ -64,7 +64,7 @@ displays the content of this file. Now click on the row corresponding to
goal ``G1``, and then click on the “Task” tab of the top-right pane, so
that it displays the corresponding *task*, as show on :numref:`fig.gui2`.
.. %EXECUTE bin/why3 ide --batch "type next;view task;snap -crop 1024x384+0+0 doc/images/gui-2.png" doc/hello_proof.why
.. %EXECUTE bin/why3 ide --batch="type next;view task;snap -crop 1024x384+0+0 doc/images/gui-2.png" doc/hello_proof.why
.. _fig.gui2:
......@@ -88,7 +88,7 @@ parent file.
Let us now select the theory “HelloProof” and run the Alt-Ergo prover.
After a short time, you should get the display of :numref:`fig.gui3`.
.. %EXECUTE bin/why3 ide --batch "type alt-ergo;view source;wait 3;type next;snap -crop 1024x384+0+0 doc/images/gui-3.png" doc/hello_proof.why
.. %EXECUTE bin/why3 ide --batch="type alt-ergo;view source;wait 3;type next;snap -crop 1024x384+0+0 doc/images/gui-3.png" doc/hello_proof.why
.. _fig.gui3:
......@@ -116,7 +116,7 @@ proved. This can be done by the menu :menuselection:`View --> Collapse
proved goals`, or even better by its shortcut :kbd:`!`. You
should now see what is displayed on :numref:`fig.gui4`.
.. %EXECUTE bin/why3 ide --batch "type alt-ergo;wait 3;type next;type split_vc;wait 1;type up;type alt-ergo;wait 3;type next;snap -crop 1024x384+0+0 doc/images/gui-4.png;save;wait 1" doc/hello_proof.why
.. %EXECUTE bin/why3 ide --batch="type alt-ergo;wait 3;type next;type split_vc;wait 1;type up;type alt-ergo;wait 3;type next;snap -crop 1024x384+0+0 doc/images/gui-4.png;save;wait 1" doc/hello_proof.why
.. _fig.gui4:
......@@ -136,7 +136,7 @@ blanks. Note that the comments themselves should not be removed, as they
are needed to properly regenerate the file when the goal is changed. See
:numref:`sec.coq` for more details.
.. %EXECUTE bin/why3 ide --batch "type next;type coq;wait 1;save;wait 1" doc/hello_proof.why
.. %EXECUTE bin/why3 ide --batch="type next;type coq;wait 1;save;wait 1" doc/hello_proof.why
.. _fig.coqide:
......@@ -165,7 +165,7 @@ Refresh session`, or the shortcut :kbd:`Control-r`. You get the tree view
shown on :numref:`fig.gui5`.
.. %EXECUTE sed -i -e 's/true -> false/false -> false/' doc/hello_proof.why
.. %EXECUTE bin/why3 ide --batch "type next;type expand;snap -crop 1024x384+0+0 doc/images/gui-5.png" doc/hello_proof.why
.. %EXECUTE bin/why3 ide --batch="type next;type expand;snap -crop 1024x384+0+0 doc/images/gui-5.png" doc/hello_proof.why
.. _fig.gui5:
......
......@@ -42,7 +42,7 @@ build/extracted: $(addsuffix .mlw, $(MLWFILES))
mkdir -p build
rm -f $@
$(WHY3) extract -D wmpn.drv -D c -L . --recursive --modular --interface -o build/ \
--debug c_no_error_msgs wmpn.mlw
--debug=c_no_error_msgs wmpn.mlw
touch $@
build/sqrtinit.h: sqrtinit.ml
......
BINDIR=/usr/local/bin
OCAMLFIND = ocamlfind
OCAMLFIND_OPT = $(addprefix -package ,$(PACKAGES)) -annot
OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLFIND_OPT)
OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLFIND_OPT)
OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAMLFIND_OPT)
PACKAGES = unix str
all:makejob runstrat
opt: makejob.opt runstrat.opt
byte: makejob.byte runstrat.byte
printconf:
echo $(OCAMLPATH)
ocamlfind printconf
makeproto.cmo: makeproto.cmi
makeproto.cmx: makeproto.cmi
makejob.opt: makeproto.cmx makejob.ml
makejob.byte: makeproto.cmo makejob.ml
makejob: makejob.opt
@rm -f makejob
ln -s makejob.opt makejob
runstrat.opt runstrat.byte: PACKAGES += why3
runstrat.opt: makeproto.cmx runstrat.ml
runstrat.byte: makeproto.cmo runstrat.ml
runstrat: runstrat.opt
@rm -f runstrat
ln -s runstrat.opt runstrat
install:
mkdir -p $(BINDIR)
cp runstrat.opt $(BINDIR)/runstrat
cp makejob.opt $(BINDIR)/makejob
clean:
rm -f *.cmo *.cma *.cmx *.cmi *.o *.annot *.opt
rm -f runstrat makejob
### Tests ###
.PHONY: test_makejob %.test_makejob_aux
TEST_MAKEJOB=$(addsuffix .test_makejob_aux , $(shell seq 5 -1 1))
test_makejob: $(TEST_MAKEJOB)
@echo Done $(TEST_MAKEJOB)
%.test_makejob_aux: makejob
@echo Run $*
+./run_wait.ml e 10 ./echo_wait.ml $*
@echo Done $*
################
# generic rules
################
%.cmi: %.mli
$(SHOW) 'Ocamlc $<'
$(HIDE)$(OCAMLC) -c $<
%.cmo: %.ml
$(SHOW) 'Ocamlc $<'
$(HIDE)$(OCAMLC) -c $<
%.cmx: %.ml
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -c $<
%.dep: %.ml
$(SHOW) 'Ocamldep $<'
$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< $<i $(TOTARGET)
%.opt:
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -linkpkg -o $@ $^
%.byte:
$(SHOW) 'Ocamlc $<'
$(HIDE)$(OCAMLC) -linkpkg -o $@ $^
#!/usr/bin/env ocaml
#load "unix.cma";;
open Format
let print_args fmt =
for i = 1 to Array.length Sys.argv - 1 do
fprintf fmt "%s" Sys.argv.(i);
if i <> Array.length Sys.argv - 1
then fprintf fmt " "
done
let max_sleep =
try float_of_string (Sys.argv.(1))
with _ -> 1.0
let () =
Random.self_init ();
let sleep = Random.float max_sleep in
printf "echo %f wait %t@." sleep print_args;
ignore (Unix.select [] [] [] sleep);
printf "echo done %t@." print_args
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2012 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(** This simple program implement the client side of the make
jobserver protocole. It ask for a job token and release it after completion
of the command
http://mad-scientist.net/make/jobserver.html
*)
(** ./makejob fdid_in fdid_out command [command options]
fdid_in and fdid_out are valid filedescriptor given by the caller
*)
open Format
let print_usage fmt =
fprintf fmt "usage: %s fdid_in fdid_out command [command options]@."
Sys.argv.(0)
(** Test there is enough arguments *)
let () = if Array.length Sys.argv < 4
then begin
print_usage err_formatter; exit 1;
end
let cmd,args = Sys.argv.(3),Array.sub Sys.argv 3 (Array.length Sys.argv - 3)
(** How should I do that? *)
let fd_of_int : int -> Unix.file_descr = Obj.magic
(** parse the file descriptor *)
let pipe =
let fdid_in, fdid_out =
try int_of_string Sys.argv.(1), int_of_string Sys.argv.(2)
with Invalid_argument _ ->
eprintf "The first two argument must be the number of a file descriptor%t"
print_usage;
exit 1
in
Makeproto.from_fd_id fdid_in fdid_out
let run_job f =
Makeproto.wait_worker pipe;
try
let res = f () in
Makeproto.release_worker pipe;
res
with exn ->
Makeproto.release_worker pipe;
raise exn
(** Execute the command *)
let () =
let ps = run_job (fun () ->
let pid = Unix.create_process cmd args
Unix.stdin Unix.stdout Unix.stderr in
let rpid,ps = Unix.waitpid [] pid in
assert (pid = rpid);
ps) in
match ps with
| Unix.WEXITED i -> exit i
| Unix.WSIGNALED i ->
(** Should not appear on windows ? *)
Unix.kill (Unix.getpid ()) Sys.sigterm
| Unix.WSTOPPED _ ->
(** Not possible since we doesn't wait for that *)
assert false
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2012 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)