Mock Version: 1.1.39 Mock Version: 1.1.39 ENTER do(['bash', '--login', '-c', 'rpmbuild -bs --target x86_64 --nodeps builddir/build/SPECS/why3.spec'], False, '/var/lib/mock/f21-build-2148422-392991/root/', None, 86400, True, False, 1000, 425, None, False, {'LANG': 'en_US.UTF-8', 'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'echo -n ""', 'HOME': '/builddir', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin'}, logger=) Executing command: ['bash', '--login', '-c', 'rpmbuild -bs --target x86_64 --nodeps builddir/build/SPECS/why3.spec'] with env {'LANG': 'en_US.UTF-8', 'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'echo -n ""', 'HOME': '/builddir', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin'} warning: Could not canonicalize hostname: buildhw-03.phx2.fedoraproject.org Building target platforms: x86_64 Building for target x86_64 Wrote: /builddir/build/SRPMS/why3-0.83-7.fc21.src.rpm Child return code was: 0 LEAVE do --> ENTER do(['bash', '--login', '-c', 'rpmbuild -bb --target x86_64 --nodeps builddir/build/SPECS/why3.spec'], False, '/var/lib/mock/f21-build-2148422-392991/root/', None, 86400, True, False, 1000, 425, None, False, {'LANG': 'en_US.UTF-8', 'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'echo -n ""', 'HOME': '/builddir', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin'}, logger=) Executing command: ['bash', '--login', '-c', 'rpmbuild -bb --target x86_64 --nodeps builddir/build/SPECS/why3.spec'] with env {'LANG': 'en_US.UTF-8', 'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'echo -n ""', 'HOME': '/builddir', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin'} Building target platforms: x86_64 Building for target x86_64 Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.unphiK + umask 022 + cd /builddir/build/BUILD + cd /builddir/build/BUILD + rm -rf why3-0.83 + /usr/bin/gzip -dc /builddir/build/SOURCES/why3-0.83.tar.gz + /usr/bin/tar -xf - + STATUS=0 + '[' 0 -ne 0 ']' + cd why3-0.83 + /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w . + cd /builddir/build/BUILD + cd why3-0.83 + /usr/bin/xz -dc /builddir/build/SOURCES/why3-man.tar.xz + /usr/bin/tar -xf - + STATUS=0 + '[' 0 -ne 0 ']' + /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w . Patch #0 (why3-fixes.patch): + echo 'Patch #0 (why3-fixes.patch):' + /usr/bin/cat /builddir/build/SOURCES/why3-fixes.patch + /usr/bin/patch -p1 --fuzz=0 patching file modules/mach/int.mlw patching file theories/map.why patching file configure.in patching file configure + sed -e 's/-Wall/-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -mtune=generic/' -e 's/cp /cp -p /' -e 's/Aer-29/& -ccopt -Wl,-z,relro,-z,now/' -i Makefile.in + find -O3 examples -type f -perm /0111 + xargs chmod a-x + for fil in examples/logic/einstein.why + iconv -f iso8859-1 -t utf-8 examples/logic/einstein.why + touch -r examples/logic/einstein.why examples/logic/einstein.why.utf8 + mv -f examples/logic/einstein.why.utf8 examples/logic/einstein.why + exit 0 Executing(%build): /bin/sh -e /var/tmp/rpm-tmp.NM22Ha + umask 022 + cd /builddir/build/BUILD + cd why3-0.83 + CFLAGS='-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -mtune=generic' + export CFLAGS + CXXFLAGS='-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -mtune=generic' + export CXXFLAGS + FFLAGS='-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -mtune=generic -I/usr/lib64/gfortran/modules' + export FFLAGS + FCFLAGS='-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -mtune=generic -I/usr/lib64/gfortran/modules' + export FCFLAGS + LDFLAGS='-Wl,-z,relro ' + export LDFLAGS + '[' 1 = 1 ']' ++ find . -name config.guess -o -name config.sub + '[' 1 = 1 ']' + '[' x '!=' x ']' + ./configure --build=x86_64-redhat-linux-gnu --host=x86_64-redhat-linux-gnu --program-prefix= --disable-dependency-tracking --prefix=/usr --exec-prefix=/usr --bindir=/usr/bin --sbindir=/usr/sbin --sysconfdir=/etc --datadir=/usr/share --includedir=/usr/include --libdir=/usr/lib64 --libexecdir=/usr/libexec --localstatedir=/var --sharedstatedir=/var/lib --mandir=/usr/share/man --infodir=/usr/share/info configure: WARNING: unrecognized options: --disable-dependency-tracking checking executable suffix... checking for x86_64-redhat-linux-gnu-gcc... no checking for gcc... gcc checking whether the C compiler works... yes checking for C compiler default output file name... a.out checking for suffix of executables... checking whether we are cross compiling... no checking for suffix of object files... o checking whether we are using the GNU C compiler... yes checking whether gcc accepts -g... yes checking for gcc option to accept ISO C89... none needed checking for ocamlc... ocamlc ocaml version is 4.01.0 ocaml library path is /usr/lib64/ocaml checking for ocamlopt... ocamlopt checking ocamlopt version... ok checking for ocamlc.opt... ocamlc.opt checking ocamlc.opt version... ok checking for ocamlopt.opt... ocamlopt.opt checking ocamlc.opt version... ok checking for ocamldep... ocamldep checking for ocamldep.opt... ocamldep.opt checking for ocamllex... ocamllex checking for ocamllex.opt... ocamllex.opt checking for ocamlyacc... ocamlyacc checking for ocamldoc... ocamldoc checking for ocamldoc.opt... ocamldoc.opt checking for camlp5o... camlp5o checking for ocamlfind... yes checking for rubber... rubber checking for hevea... hevea checking for hacha... hacha ocamlfind found zarith in /usr/lib64/ocaml/zarith ocamlfind found lablgtk2 in /usr/lib64/ocaml/lablgtk2 ocamlfind found lablgtksourceview2 in /usr/lib64/ocaml/lablgtk2 ocamlfind found sqlite3 in /usr/lib64/ocaml/sqlite3 checking for coqc... coqc checking Coq version... 8.4pl4 checking for /usr/lib64/coq/kernel/term.cmi... yes checking for coqdep... coqdep checking for Flocq... yes checking for pvs... no configure: WARNING: Cannot find pvs. checking for isabelle... no configure: WARNING: Cannot find isabelle. ocamlfind found ocamlgraph in /usr/lib64/ocaml/ocamlgraph configure: creating ./config.status config.status: creating Makefile config.status: creating src/config.sh config.status: creating doc/version.tex config.status: creating lib/why3/META config.status: creating src/jessie/Makefile config.status: executing chmod commands Summary configure: WARNING: unrecognized options: --disable-dependency-tracking ----------------------------------------- Verbose make : no OCaml compiler : yes Version : 4.01.0 Library path : /usr/lib64/ocaml Native compilation : yes Profiling : no Zarith : yes IDE : yes Bench tool : yes Documentation : yes HTML : yes Coq support : yes Version : 8.4pl4 Library path : /usr/lib64/coq "why3" tactic : yes Realization support : yes FP arithmetic : yes PVS support : no (pvs not found) Isabelle support : no (isabelle not found) Frama-C support : no (disabled by default) Hypothesis selection : yes Installable : yes Binary path : /usr/bin Lib path : /usr/lib64/why3 Data path : ${prefix}/share/why3 Ocaml Library : /usr/lib64/ocaml/why3 Relocatable : no + make Makefile:207: src/util/config.dep: No such file or directory Makefile:207: src/util/bigInt.dep: No such file or directory Makefile:207: src/util/util.dep: No such file or directory Makefile:207: src/util/opt.dep: No such file or directory Makefile:207: src/util/lists.dep: No such file or directory Makefile:207: src/util/strings.dep: No such file or directory Makefile:207: src/util/extmap.dep: No such file or directory Makefile:207: src/util/extset.dep: No such file or directory Makefile:207: src/util/exthtbl.dep: No such file or directory Makefile:207: src/util/weakhtbl.dep: No such file or directory Makefile:207: src/util/hashcons.dep: No such file or directory Makefile:207: src/util/stdlib.dep: No such file or directory Makefile:207: src/util/exn_printer.dep: No such file or directory Makefile:207: src/util/pp.dep: No such file or directory Makefile:207: src/util/debug.dep: No such file or directory Makefile:207: src/util/loc.dep: No such file or directory Makefile:207: src/util/print_tree.dep: No such file or directory Makefile:207: src/util/cmdline.dep: No such file or directory Makefile:207: src/util/warning.dep: No such file or directory Makefile:207: src/util/sysutil.dep: No such file or directory Makefile:207: src/util/rc.dep: No such file or directory Makefile:207: src/util/plugin.dep: No such file or directory Makefile:207: src/util/bigInt.dep: No such file or directory Makefile:207: src/util/number.dep: No such file or directory Makefile:207: src/util/pqueue.dep: No such file or directory Makefile:207: src/core/ident.dep: No such file or directory Makefile:207: src/core/ty.dep: No such file or directory Makefile:207: src/core/term.dep: No such file or directory Makefile:207: src/core/pattern.dep: No such file or directory Makefile:207: src/core/decl.dep: No such file or directory Makefile:207: src/core/theory.dep: No such file or directory Makefile:207: src/core/task.dep: No such file or directory Makefile:207: src/core/pretty.dep: No such file or directory Makefile:207: src/core/dterm.dep: No such file or directory Makefile:207: src/core/env.dep: No such file or directory Makefile:207: src/core/trans.dep: No such file or directory Makefile:207: src/core/printer.dep: No such file or directory Makefile:207: src/parser/ptree.dep: No such file or directory Makefile:207: src/parser/glob.dep: No such file or directory Makefile:207: src/parser/parser.dep: No such file or directory Makefile:207: src/parser/typing.dep: No such file or directory Makefile:207: src/parser/lexer.dep: No such file or directory Makefile:207: src/driver/call_provers.dep: No such file or directory Makefile:207: src/driver/driver_ast.dep: No such file or directory Makefile:207: src/driver/driver_parser.dep: No such file or directory Makefile:207: src/driver/driver_lexer.dep: No such file or directory Makefile:207: src/driver/driver.dep: No such file or directory Makefile:207: src/driver/whyconf.dep: No such file or directory Makefile:207: src/driver/autodetection.dep: No such file or directory Makefile:207: src/transform/simplify_formula.dep: No such file or directory Makefile:207: src/transform/inlining.dep: No such file or directory Makefile:207: src/transform/split_goal.dep: No such file or directory Makefile:207: src/transform/induction.dep: No such file or directory Makefile:207: src/transform/eliminate_definition.dep: No such file or directory Makefile:207: src/transform/eliminate_algebraic.dep: No such file or directory Makefile:207: src/transform/eliminate_inductive.dep: No such file or directory Makefile:207: src/transform/eliminate_let.dep: No such file or directory Makefile:207: src/transform/eliminate_if.dep: No such file or directory Makefile:207: src/transform/libencoding.dep: No such file or directory Makefile:207: src/transform/discriminate.dep: No such file or directory Makefile:207: src/transform/encoding.dep: No such file or directory Makefile:207: src/transform/encoding_select.dep: No such file or directory Makefile:207: src/transform/encoding_guards_full.dep: No such file or directory Makefile:207: src/transform/encoding_tags_full.dep: No such file or directory Makefile:207: src/transform/encoding_guards.dep: No such file or directory Makefile:207: src/transform/encoding_tags.dep: No such file or directory Makefile:207: src/transform/encoding_twin.dep: No such file or directory Makefile:207: src/transform/encoding_sort.dep: No such file or directory Makefile:207: src/transform/simplify_array.dep: No such file or directory Makefile:207: src/transform/filter_trigger.dep: No such file or directory Makefile:207: src/transform/introduction.dep: No such file or directory Makefile:207: src/transform/abstraction.dep: No such file or directory Makefile:207: src/transform/close_epsilon.dep: No such file or directory Makefile:207: src/transform/lift_epsilon.dep: No such file or directory Makefile:207: src/transform/eliminate_epsilon.dep: No such file or directory Makefile:207: src/transform/eval_match.dep: No such file or directory Makefile:207: src/transform/instantiate_predicate.dep: No such file or directory Makefile:207: src/transform/smoke_detector.dep: No such file or directory Makefile:207: src/printer/alt_ergo.dep: No such file or directory Makefile:207: src/printer/why3printer.dep: No such file or directory Makefile:207: src/printer/smtv1.dep: No such file or directory Makefile:207: src/printer/smtv2.dep: No such file or directory Makefile:207: src/printer/coq.dep: No such file or directory Makefile:207: src/printer/pvs.dep: No such file or directory Makefile:207: src/printer/isabelle.dep: No such file or directory Makefile:207: src/printer/simplify.dep: No such file or directory Makefile:207: src/printer/gappa.dep: No such file or directory Makefile:207: src/printer/cvc3.dep: No such file or directory Makefile:207: src/printer/yices.dep: No such file or directory Makefile:207: src/printer/mathematica.dep: No such file or directory Makefile:207: src/session/xml.dep: No such file or directory Makefile:207: src/session/termcode.dep: No such file or directory Makefile:207: src/session/session.dep: No such file or directory Makefile:207: src/session/session_tools.dep: No such file or directory Makefile:207: src/session/session_scheduler.dep: No such file or directory Makefile:207: src/whyml/mlw_ty.dep: No such file or directory Makefile:207: src/whyml/mlw_expr.dep: No such file or directory Makefile:207: src/whyml/mlw_decl.dep: No such file or directory Makefile:207: src/whyml/mlw_pretty.dep: No such file or directory Makefile:207: src/whyml/mlw_wp.dep: No such file or directory Makefile:207: src/whyml/mlw_module.dep: No such file or directory Makefile:207: src/whyml/mlw_dexpr.dep: No such file or directory Makefile:207: src/whyml/mlw_typing.dep: No such file or directory Makefile:207: src/whyml/mlw_driver.dep: No such file or directory Makefile:207: src/whyml/mlw_ocaml.dep: No such file or directory Makefile:207: src/whyml/mlw_main.dep: No such file or directory Makefile:207: src/whyml/mlw_interp.dep: No such file or directory Makefile:375: plugins/parser/genequlin.dep: No such file or directory Makefile:375: plugins/parser/dimacs.dep: No such file or directory Makefile:375: plugins/transform/hypothesis_selection.dep: No such file or directory Makefile:375: plugins/tptp/tptp_ast.dep: No such file or directory Makefile:375: plugins/tptp/tptp_parser.dep: No such file or directory Makefile:375: plugins/tptp/tptp_typing.dep: No such file or directory Makefile:375: plugins/tptp/tptp_lexer.dep: No such file or directory Makefile:375: plugins/tptp/tptp_printer.dep: No such file or directory Makefile:416: src/main.dep: No such file or directory Makefile:530: src/why3config/why3config.dep: No such file or directory Makefile:592: src/ide/gconfig.dep: No such file or directory Makefile:592: src/ide/gmain.dep: No such file or directory Makefile:645: src/why3replayer/replay.dep: No such file or directory Makefile:698: src/why3session/why3session_lib.dep: No such file or directory Makefile:698: src/why3session/why3session_copy.dep: No such file or directory Makefile:698: src/why3session/why3session_info.dep: No such file or directory Makefile:698: src/why3session/why3session_latex.dep: No such file or directory Makefile:698: src/why3session/why3session_html.dep: No such file or directory Makefile:698: src/why3session/why3session_rm.dep: No such file or directory Makefile:698: src/why3session/why3session_output.dep: No such file or directory Makefile:698: src/why3session/why3session_run.dep: No such file or directory Makefile:698: src/why3session/why3session_csv.dep: No such file or directory Makefile:698: src/why3session/why3session.dep: No such file or directory Makefile:753: src/why3bench/worker.dep: No such file or directory Makefile:753: src/why3bench/db.dep: No such file or directory Makefile:753: src/why3bench/bench.dep: No such file or directory Makefile:753: src/why3bench/benchrc.dep: No such file or directory Makefile:753: src/why3bench/benchdb.dep: No such file or directory Makefile:753: src/why3bench/why3bench.dep: No such file or directory Makefile:827: src/coq-tactic/coqCompat.dep: No such file or directory Makefile:827: src/coq-tactic/why3tac.dep: No such file or directory Makefile:827: src/coq-tactic/g_why3tac.dep: No such file or directory Makefile:952: lib/coq/BuiltIn.vd: No such file or directory Makefile:952: lib/coq/int/Exponentiation.vd: No such file or directory Makefile:952: lib/coq/int/Abs.vd: No such file or directory Makefile:952: lib/coq/int/ComputerDivision.vd: No such file or directory Makefile:952: lib/coq/int/Div2.vd: No such file or directory Makefile:952: lib/coq/int/EuclideanDivision.vd: No such file or directory Makefile:952: lib/coq/int/Int.vd: No such file or directory Makefile:952: lib/coq/int/MinMax.vd: No such file or directory Makefile:952: lib/coq/int/Power.vd: No such file or directory Makefile:952: lib/coq/bool/Bool.vd: No such file or directory Makefile:952: lib/coq/real/Abs.vd: No such file or directory Makefile:952: lib/coq/real/ExpLog.vd: No such file or directory Makefile:952: lib/coq/real/FromInt.vd: No such file or directory Makefile:952: lib/coq/real/MinMax.vd: No such file or directory Makefile:952: lib/coq/real/PowerInt.vd: No such file or directory Makefile:952: lib/coq/real/Real.vd: No such file or directory Makefile:952: lib/coq/real/Square.vd: No such file or directory Makefile:952: lib/coq/real/RealInfix.vd: No such file or directory Makefile:952: lib/coq/number/Divisibility.vd: No such file or directory Makefile:952: lib/coq/number/Gcd.vd: No such file or directory Makefile:952: lib/coq/number/Parity.vd: No such file or directory Makefile:952: lib/coq/number/Prime.vd: No such file or directory Makefile:952: lib/coq/number/Coprime.vd: No such file or directory Makefile:952: lib/coq/set/Set.vd: No such file or directory Makefile:952: lib/coq/map/Map.vd: No such file or directory Makefile:952: lib/coq/map/Occ.vd: No such file or directory Makefile:952: lib/coq/map/MapPermut.vd: No such file or directory Makefile:952: lib/coq/map/MapInjection.vd: No such file or directory Makefile:952: lib/coq/list/List.vd: No such file or directory Makefile:952: lib/coq/list/Length.vd: No such file or directory Makefile:952: lib/coq/list/Mem.vd: No such file or directory Makefile:952: lib/coq/list/Nth.vd: No such file or directory Makefile:952: lib/coq/list/NthLength.vd: No such file or directory Makefile:952: lib/coq/list/HdTl.vd: No such file or directory Makefile:952: lib/coq/list/NthHdTl.vd: No such file or directory Makefile:952: lib/coq/list/Append.vd: No such file or directory Makefile:952: lib/coq/list/NthLengthAppend.vd: No such file or directory Makefile:952: lib/coq/list/Reverse.vd: No such file or directory Makefile:952: lib/coq/option/Option.vd: No such file or directory Makefile:952: lib/coq/floating_point/GenFloat.vd: No such file or directory Makefile:952: lib/coq/floating_point/Rounding.vd: No such file or directory Makefile:952: lib/coq/floating_point/SingleFormat.vd: No such file or directory Makefile:952: lib/coq/floating_point/Single.vd: No such file or directory Makefile:952: lib/coq/floating_point/DoubleFormat.vd: No such file or directory Makefile:952: lib/coq/floating_point/Double.vd: No such file or directory Makefile:1215: lib/ocaml/why3__BigInt.dep: No such file or directory Makefile:1215: lib/ocaml/why3__IntAux.dep: No such file or directory Makefile:1215: lib/ocaml/why3__Array.dep: No such file or directory Makefile:1340: src/why3doc/doc_html.dep: No such file or directory Makefile:1340: src/why3doc/doc_def.dep: No such file or directory Makefile:1340: src/why3doc/doc_lexer.dep: No such file or directory Makefile:1340: src/why3doc/doc_main.dep: No such file or directory Ocamllex src/why3doc/doc_lexer.mll 105 states, 991 transitions, table size 4594 bytes 1665 additional bytes used for bindings Ocamldep src/why3doc/doc_main.ml Ocamldep src/why3doc/doc_lexer.ml Ocamldep src/why3doc/doc_def.ml Ocamldep src/why3doc/doc_html.ml cp -p lib/ocaml/why3__BigInt_zarith.ml lib/ocaml/why3__BigInt.ml Ocamldep lib/ocaml/why3__Array.ml Ocamldep lib/ocaml/why3__IntAux.ml Ocamldep lib/ocaml/why3__BigInt.ml Coqdep lib/coq/floating_point/Double.v Coqdep lib/coq/floating_point/DoubleFormat.v Coqdep lib/coq/floating_point/Single.v Coqdep lib/coq/floating_point/SingleFormat.v Coqdep lib/coq/floating_point/Rounding.v Coqdep lib/coq/floating_point/GenFloat.v Coqdep lib/coq/option/Option.v Coqdep lib/coq/list/Reverse.v Coqdep lib/coq/list/NthLengthAppend.v Coqdep lib/coq/list/Append.v Coqdep lib/coq/list/NthHdTl.v Coqdep lib/coq/list/HdTl.v Coqdep lib/coq/list/NthLength.v Coqdep lib/coq/list/Nth.v Coqdep lib/coq/list/Mem.v Coqdep lib/coq/list/Length.v Coqdep lib/coq/list/List.v Coqdep lib/coq/map/MapInjection.v Coqdep lib/coq/map/MapPermut.v Coqdep lib/coq/map/Occ.v Coqdep lib/coq/map/Map.v Coqdep lib/coq/set/Set.v Coqdep lib/coq/number/Coprime.v Coqdep lib/coq/number/Prime.v Coqdep lib/coq/number/Parity.v Coqdep lib/coq/number/Gcd.v Coqdep lib/coq/number/Divisibility.v Coqdep lib/coq/real/RealInfix.v Coqdep lib/coq/real/Square.v Coqdep lib/coq/real/Real.v Coqdep lib/coq/real/PowerInt.v Coqdep lib/coq/real/MinMax.v Coqdep lib/coq/real/FromInt.v Coqdep lib/coq/real/ExpLog.v Coqdep lib/coq/real/Abs.v Coqdep lib/coq/bool/Bool.v Coqdep lib/coq/int/Power.v Coqdep lib/coq/int/MinMax.v Coqdep lib/coq/int/Int.v Coqdep lib/coq/int/EuclideanDivision.v Coqdep lib/coq/int/Div2.v Coqdep lib/coq/int/ComputerDivision.v Coqdep lib/coq/int/Abs.v Coqdep lib/coq/int/Exponentiation.v Coqdep lib/coq/BuiltIn.v Camlp5 src/coq-tactic/g_why3tac.ml4 cp -p -f src/coq-tactic/coqCompat.8.4.ml src/coq-tactic/coqCompat.ml Ocamldep src/coq-tactic/g_why3tac.ml Ocamldep src/coq-tactic/why3tac.ml Ocamldep src/coq-tactic/coqCompat.ml Ocamldep src/why3bench/why3bench.ml Ocamldep src/why3bench/benchdb.ml Ocamldep src/why3bench/benchrc.ml Ocamldep src/why3bench/bench.ml Ocamldep src/why3bench/db.ml Ocamldep src/why3bench/worker.ml Ocamldep src/why3session/why3session.ml Ocamldep src/why3session/why3session_csv.ml Ocamldep src/why3session/why3session_run.ml Ocamldep src/why3session/why3session_output.ml Ocamldep src/why3session/why3session_rm.ml Ocamldep src/why3session/why3session_html.ml Ocamldep src/why3session/why3session_latex.ml Ocamldep src/why3session/why3session_info.ml Ocamldep src/why3session/why3session_copy.ml Ocamldep src/why3session/why3session_lib.ml Ocamldep src/why3replayer/replay.ml Ocamldep src/ide/gmain.ml Ocamldep src/ide/gconfig.ml Ocamldep src/why3config/why3config.ml Ocamldep src/main.ml Ocamllex plugins/tptp/tptp_lexer.mll 101 states, 1563 transitions, table size 6858 bytes 3126 additional bytes used for bindings Ocamlyacc plugins/tptp/tptp_parser.mly Ocamllex plugins/parser/dimacs.mll 34 states, 434 transitions, table size 1940 bytes 1293 additional bytes used for bindings Ocamldep plugins/tptp/tptp_printer.ml Ocamldep plugins/tptp/tptp_lexer.ml Ocamldep plugins/tptp/tptp_typing.ml Ocamldep plugins/tptp/tptp_parser.ml Ocamldep plugins/tptp/tptp_ast.ml Ocamldep plugins/transform/hypothesis_selection.ml Ocamldep plugins/parser/dimacs.ml Ocamldep plugins/parser/genequlin.ml Generate src/util/config.ml Ocamllex src/util/rc.mll 48 states, 1889 transitions, table size 7844 bytes 3073 additional bytes used for bindings Ocamllex src/parser/lexer.mll 143 states, 3137 transitions, table size 13406 bytes 7548 additional bytes used for bindings Ocamlyacc src/parser/parser.mly Ocamlyacc src/driver/driver_parser.mly Ocamllex src/driver/driver_lexer.mll 29 states, 1101 transitions, table size 4578 bytes Ocamllex src/session/xml.mll 114 states, 1396 transitions, table size 6268 bytes 3538 additional bytes used for bindings Ocamldep src/whyml/mlw_interp.ml Ocamldep src/whyml/mlw_main.ml Ocamldep src/whyml/mlw_ocaml.ml Ocamldep src/whyml/mlw_driver.ml Ocamldep src/whyml/mlw_typing.ml Ocamldep src/whyml/mlw_dexpr.ml Ocamldep src/whyml/mlw_module.ml Ocamldep src/whyml/mlw_wp.ml Ocamldep src/whyml/mlw_pretty.ml Ocamldep src/whyml/mlw_decl.ml Ocamldep src/whyml/mlw_expr.ml Ocamldep src/whyml/mlw_ty.ml Ocamldep src/session/session_scheduler.ml Ocamldep src/session/session_tools.ml Ocamldep src/session/session.ml Ocamldep src/session/termcode.ml Ocamldep src/session/xml.ml Ocamldep src/printer/mathematica.ml Ocamldep src/printer/yices.ml Ocamldep src/printer/cvc3.ml Ocamldep src/printer/gappa.ml Ocamldep src/printer/simplify.ml Ocamldep src/printer/isabelle.ml Ocamldep src/printer/pvs.ml Ocamldep src/printer/coq.ml Ocamldep src/printer/smtv2.ml Ocamldep src/printer/smtv1.ml Ocamldep src/printer/why3printer.ml Ocamldep src/printer/alt_ergo.ml Ocamldep src/transform/smoke_detector.ml Ocamldep src/transform/instantiate_predicate.ml Ocamldep src/transform/eval_match.ml Ocamldep src/transform/eliminate_epsilon.ml Ocamldep src/transform/lift_epsilon.ml Ocamldep src/transform/close_epsilon.ml Ocamldep src/transform/abstraction.ml Ocamldep src/transform/introduction.ml Ocamldep src/transform/filter_trigger.ml Ocamldep src/transform/simplify_array.ml Ocamldep src/transform/encoding_sort.ml Ocamldep src/transform/encoding_twin.ml Ocamldep src/transform/encoding_tags.ml Ocamldep src/transform/encoding_guards.ml Ocamldep src/transform/encoding_tags_full.ml Ocamldep src/transform/encoding_guards_full.ml Ocamldep src/transform/encoding_select.ml Ocamldep src/transform/encoding.ml Ocamldep src/transform/discriminate.ml Ocamldep src/transform/libencoding.ml Ocamldep src/transform/eliminate_if.ml Ocamldep src/transform/eliminate_let.ml Ocamldep src/transform/eliminate_inductive.ml Ocamldep src/transform/eliminate_algebraic.ml Ocamldep src/transform/eliminate_definition.ml Ocamldep src/transform/induction.ml Ocamldep src/transform/split_goal.ml Ocamldep src/transform/inlining.ml Ocamldep src/transform/simplify_formula.ml Ocamldep src/driver/autodetection.ml Ocamldep src/driver/whyconf.ml Ocamldep src/driver/driver.ml Ocamldep src/driver/driver_lexer.ml Ocamldep src/driver/driver_parser.ml Ocamldep src/driver/driver_ast.ml Ocamldep src/driver/call_provers.ml Ocamldep src/parser/lexer.ml Ocamldep src/parser/typing.ml Ocamldep src/parser/parser.ml Ocamldep src/parser/glob.ml Ocamldep src/parser/ptree.ml Ocamldep src/core/printer.ml Ocamldep src/core/trans.ml Ocamldep src/core/env.ml Ocamldep src/core/dterm.ml Ocamldep src/core/pretty.ml Ocamldep src/core/task.ml Ocamldep src/core/theory.ml Ocamldep src/core/decl.ml Ocamldep src/core/pattern.ml Ocamldep src/core/term.ml Ocamldep src/core/ty.ml Ocamldep src/core/ident.ml Ocamldep src/util/pqueue.ml Ocamldep src/util/number.ml Ocamldep src/util/bigInt.ml Ocamldep src/util/plugin.ml Ocamldep src/util/rc.ml Ocamldep src/util/sysutil.ml Ocamldep src/util/warning.ml Ocamldep src/util/cmdline.ml Ocamldep src/util/print_tree.ml Ocamldep src/util/loc.ml Ocamldep src/util/debug.ml Ocamldep src/util/pp.ml Ocamldep src/util/exn_printer.ml Ocamldep src/util/stdlib.ml Ocamldep src/util/hashcons.ml Ocamldep src/util/weakhtbl.ml Ocamldep src/util/exthtbl.ml Ocamldep src/util/extset.ml Ocamldep src/util/extmap.ml Ocamldep src/util/strings.ml Ocamldep src/util/lists.ml Ocamldep src/util/opt.ml Ocamldep src/util/util.ml Ocamldep src/util/config.ml cp -p lib/ocaml/why3__BigInt_zarith.ml lib/ocaml/why3__BigInt.ml Ocamlopt src/util/config.ml Ocamlc src/util/bigInt.mli Ocamlopt src/util/bigInt.ml Ocamlc src/util/util.mli Ocamlopt src/util/util.ml Ocamlc src/util/opt.mli Ocamlopt src/util/opt.ml Ocamlc src/util/lists.mli Ocamlopt src/util/lists.ml Ocamlc src/util/strings.mli Ocamlopt src/util/strings.ml Ocamlc src/util/extmap.mli Ocamlopt src/util/extmap.ml Ocamlc src/util/extset.mli Ocamlopt src/util/extset.ml Ocamlc src/util/exthtbl.mli Ocamlopt src/util/exthtbl.ml Ocamlc src/util/weakhtbl.mli Ocamlopt src/util/weakhtbl.ml Ocamlc src/util/hashcons.mli Ocamlopt src/util/hashcons.ml Ocamlc src/util/stdlib.mli Ocamlopt src/util/stdlib.ml Ocamlc src/util/exn_printer.mli Ocamlopt src/util/exn_printer.ml Ocamlc src/util/pp.mli Ocamlopt src/util/pp.ml Ocamlc src/util/debug.mli Ocamlopt src/util/debug.ml Ocamlc src/util/loc.mli Ocamlopt src/util/loc.ml Ocamlc src/util/print_tree.mli Ocamlopt src/util/print_tree.ml Ocamlc src/util/cmdline.mli Ocamlopt src/util/cmdline.ml Ocamlc src/util/warning.mli Ocamlopt src/util/warning.ml Ocamlc src/util/sysutil.mli Ocamlopt src/util/sysutil.ml Ocamlc src/util/rc.mli Ocamlopt src/util/rc.ml Ocamlc src/util/plugin.mli Ocamlopt src/util/plugin.ml Ocamlc src/util/number.mli Ocamlopt src/util/number.ml Ocamlc src/util/pqueue.mli Ocamlopt src/util/pqueue.ml Ocamlc src/core/ident.mli Ocamlopt src/core/ident.ml Ocamlc src/core/ty.mli Ocamlopt src/core/ty.ml Ocamlc src/core/term.mli Ocamlopt src/core/term.ml Ocamlc src/core/pattern.mli Ocamlopt src/core/pattern.ml Ocamlc src/core/decl.mli Ocamlopt src/core/decl.ml Ocamlc src/core/theory.mli Ocamlopt src/core/theory.ml Ocamlc src/core/task.mli Ocamlopt src/core/task.ml Ocamlc src/core/pretty.mli Ocamlopt src/core/pretty.ml Ocamlc src/core/dterm.mli Ocamlopt src/core/dterm.ml Ocamlc src/core/env.mli Ocamlopt src/core/env.ml Ocamlc src/core/trans.mli Ocamlopt src/core/trans.ml Ocamlc src/core/printer.mli Ocamlopt src/core/printer.ml Ocamlopt src/parser/ptree.ml Ocamlc src/parser/glob.mli Ocamlopt src/parser/glob.ml Ocamlc src/parser/parser.mli Ocamlopt src/parser/parser.ml Ocamlc src/parser/typing.mli Ocamlopt src/parser/typing.ml Ocamlc src/parser/lexer.mli Ocamlopt src/parser/lexer.ml Ocamlc src/driver/call_provers.mli Ocamlopt src/driver/call_provers.ml Ocamlopt src/driver/driver_ast.ml Ocamlc src/driver/driver_parser.mli Ocamlopt src/driver/driver_parser.ml Ocamlc src/driver/driver_lexer.mli Ocamlopt src/driver/driver_lexer.ml Ocamlc src/driver/driver.mli Ocamlopt src/driver/driver.ml Ocamlc src/driver/whyconf.mli Ocamlopt src/driver/whyconf.ml Ocamlc src/driver/autodetection.mli Ocamlopt src/driver/autodetection.ml Ocamlc src/transform/simplify_formula.mli Ocamlopt src/transform/simplify_formula.ml Ocamlc src/transform/inlining.mli Ocamlopt src/transform/inlining.ml Ocamlc src/transform/split_goal.mli Ocamlopt src/transform/split_goal.ml Ocamlc src/transform/induction.mli Ocamlopt src/transform/induction.ml Ocamlc src/transform/eliminate_definition.mli Ocamlopt src/transform/eliminate_definition.ml Ocamlc src/transform/eliminate_algebraic.mli Ocamlopt src/transform/eliminate_algebraic.ml Ocamlc src/transform/eliminate_inductive.mli Ocamlopt src/transform/eliminate_inductive.ml Ocamlc src/transform/eliminate_let.mli Ocamlopt src/transform/eliminate_let.ml Ocamlc src/transform/eliminate_if.mli Ocamlopt src/transform/eliminate_if.ml Ocamlc src/transform/libencoding.mli Ocamlopt src/transform/libencoding.ml Ocamlc src/transform/discriminate.mli Ocamlopt src/transform/discriminate.ml Ocamlc src/transform/encoding.mli Ocamlopt src/transform/encoding.ml Ocamlc src/transform/encoding_select.mli Ocamlopt src/transform/encoding_select.ml Ocamlc src/transform/encoding_guards_full.mli Ocamlopt src/transform/encoding_guards_full.ml Ocamlc src/transform/encoding_tags_full.mli Ocamlopt src/transform/encoding_tags_full.ml Ocamlc src/transform/encoding_guards.mli Ocamlopt src/transform/encoding_guards.ml Ocamlc src/transform/encoding_tags.mli Ocamlopt src/transform/encoding_tags.ml Ocamlc src/transform/encoding_twin.mli Ocamlopt src/transform/encoding_twin.ml Ocamlc src/transform/encoding_sort.mli Ocamlopt src/transform/encoding_sort.ml Ocamlc src/transform/simplify_array.mli Ocamlopt src/transform/simplify_array.ml Ocamlc src/transform/filter_trigger.mli Ocamlopt src/transform/filter_trigger.ml Ocamlc src/transform/introduction.mli Ocamlopt src/transform/introduction.ml Ocamlc src/transform/abstraction.mli Ocamlopt src/transform/abstraction.ml Ocamlc src/transform/close_epsilon.mli Ocamlopt src/transform/close_epsilon.ml Ocamlc src/transform/lift_epsilon.mli Ocamlopt src/transform/lift_epsilon.ml Ocamlc src/transform/eliminate_epsilon.mli Ocamlopt src/transform/eliminate_epsilon.ml Ocamlc src/transform/eval_match.mli Ocamlopt src/transform/eval_match.ml Ocamlc src/transform/instantiate_predicate.mli Ocamlopt src/transform/instantiate_predicate.ml Ocamlc src/transform/smoke_detector.mli Ocamlopt src/transform/smoke_detector.ml Ocamlc src/printer/alt_ergo.mli Ocamlopt src/printer/alt_ergo.ml Ocamlc src/printer/why3printer.mli Ocamlopt src/printer/why3printer.ml Ocamlc src/printer/smtv1.mli Ocamlopt src/printer/smtv1.ml Ocamlc src/printer/smtv2.mli Ocamlopt src/printer/smtv2.ml Ocamlc src/printer/coq.mli Ocamlopt src/printer/coq.ml Ocamlopt src/printer/pvs.ml Ocamlopt src/printer/isabelle.ml Ocamlc src/printer/simplify.mli Ocamlopt src/printer/simplify.ml Ocamlc src/printer/gappa.mli Ocamlopt src/printer/gappa.ml Ocamlc src/printer/cvc3.mli Ocamlopt src/printer/cvc3.ml Ocamlopt src/printer/yices.ml Ocamlopt src/printer/mathematica.ml Ocamlc src/session/xml.mli Ocamlopt src/session/xml.ml Ocamlc src/session/termcode.mli Ocamlopt src/session/termcode.ml Ocamlc src/session/session.mli Ocamlopt src/session/session.ml Ocamlc src/session/session_tools.mli Ocamlopt src/session/session_tools.ml Ocamlc src/session/session_scheduler.mli Ocamlopt src/session/session_scheduler.ml Ocamlc src/whyml/mlw_ty.mli Ocamlopt src/whyml/mlw_ty.ml Ocamlc src/whyml/mlw_expr.mli Ocamlopt src/whyml/mlw_expr.ml Ocamlc src/whyml/mlw_decl.mli Ocamlopt src/whyml/mlw_decl.ml Ocamlc src/whyml/mlw_pretty.mli Ocamlopt src/whyml/mlw_pretty.ml Ocamlc src/whyml/mlw_wp.mli Ocamlopt src/whyml/mlw_wp.ml Ocamlc src/whyml/mlw_module.mli Ocamlopt src/whyml/mlw_module.ml Ocamlc src/whyml/mlw_dexpr.mli Ocamlopt src/whyml/mlw_dexpr.ml Ocamlc src/whyml/mlw_typing.mli Ocamlopt src/whyml/mlw_typing.ml Ocamlc src/whyml/mlw_driver.mli Ocamlopt src/whyml/mlw_driver.ml Ocamlc src/whyml/mlw_ocaml.mli Ocamlopt src/whyml/mlw_ocaml.ml Ocamlc src/whyml/mlw_main.mli Ocamlopt src/whyml/mlw_main.ml Ocamlc src/whyml/mlw_interp.mli Ocamlopt src/whyml/mlw_interp.ml Linking lib/why3/why3.cmx Ocamlopt plugins/parser/genequlin.ml Linking lib/plugins/genequlin.cmxs Ocamlopt plugins/parser/dimacs.ml Linking lib/plugins/dimacs.cmxs Ocamlopt plugins/tptp/tptp_ast.ml Ocamlc plugins/tptp/tptp_parser.mli Ocamlopt plugins/tptp/tptp_parser.ml Ocamlc plugins/tptp/tptp_typing.mli Ocamlopt plugins/tptp/tptp_typing.ml Ocamlc plugins/tptp/tptp_lexer.mli Ocamlopt plugins/tptp/tptp_lexer.ml Ocamlc plugins/tptp/tptp_printer.mli Ocamlopt plugins/tptp/tptp_printer.ml Linking lib/plugins/tptp.cmxs Ocamlopt plugins/transform/hypothesis_selection.ml Linking lib/plugins/hypothesis_selection.cmxs Linking lib/why3/why3.cmxa Ocamlopt src/main.ml Linking bin/why3.opt Ocamlopt src/why3config/why3config.ml Linking bin/why3config.opt ocamlc.opt -c -ccopt "-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -mtune=generic -o src/ide/resetgc.o" src/ide/resetgc.c Ocamlc src/ide/gconfig.mli Ocamlopt src/ide/gconfig.ml Ocamlopt src/ide/gmain.ml Linking bin/why3ide.opt Ocamlopt src/why3replayer/replay.ml Linking bin/why3replayer.opt Ocamlc src/why3session/why3session_lib.mli Ocamlopt src/why3session/why3session_lib.ml Ocamlopt src/why3session/why3session_copy.ml Ocamlopt src/why3session/why3session_info.ml Ocamlopt src/why3session/why3session_latex.ml Ocamlopt src/why3session/why3session_html.ml Ocamlopt src/why3session/why3session_rm.ml Ocamlopt src/why3session/why3session_output.ml Ocamlopt src/why3session/why3session_run.ml Ocamlopt src/why3session/why3session_csv.ml Ocamlopt src/why3session/why3session.ml Linking bin/why3session.opt Ocamlopt src/why3bench/worker.ml Ocamlc src/why3bench/db.mli Ocamlopt src/why3bench/db.ml Ocamlc src/why3bench/bench.mli Ocamlopt src/why3bench/bench.ml Ocamlc src/why3bench/benchrc.mli Ocamlopt src/why3bench/benchrc.ml Ocamlc src/why3bench/benchdb.mli Ocamlopt src/why3bench/benchdb.ml Ocamlopt src/why3bench/why3bench.ml Linking bin/why3bench.opt Ocamlc src/coq-tactic/coqCompat.mli Ocamlopt src/coq-tactic/coqCompat.ml Ocamlopt src/coq-tactic/why3tac.ml Ocamlopt src/coq-tactic/g_why3tac.ml Linking lib/coq-tactic/why3tac.cmxs Coqc lib/coq-tactic/Why3.v Coqc lib/coq/BuiltIn.v Coqc lib/coq/int/Int.v Coqc lib/coq/int/Exponentiation.v Coqc lib/coq/int/Abs.v Coqc lib/coq/int/ComputerDivision.v Coqc lib/coq/int/EuclideanDivision.v Coqc lib/coq/int/Div2.v Coqc lib/coq/int/MinMax.v Coqc lib/coq/int/Power.v Coqc lib/coq/bool/Bool.v Coqc lib/coq/real/Real.v Coqc lib/coq/real/Abs.v Coqc lib/coq/real/ExpLog.v Coqc lib/coq/real/FromInt.v Coqc lib/coq/real/MinMax.v Coqc lib/coq/real/RealInfix.v Coqc lib/coq/real/PowerInt.v Coqc lib/coq/real/Square.v Coqc lib/coq/number/Parity.v Coqc lib/coq/number/Divisibility.v Coqc lib/coq/number/Gcd.v Coqc lib/coq/number/Prime.v Coqc lib/coq/number/Coprime.v Coqc lib/coq/set/Set.v Coqc lib/coq/map/Map.v Coqc lib/coq/map/Occ.v Coqc lib/coq/map/MapPermut.v Coqc lib/coq/map/MapInjection.v Coqc lib/coq/list/List.v Coqc lib/coq/list/Length.v Coqc lib/coq/list/Mem.v Coqc lib/coq/option/Option.v Coqc lib/coq/list/Nth.v Coqc lib/coq/list/NthLength.v Coqc lib/coq/list/HdTl.v Coqc lib/coq/list/NthHdTl.v Coqc lib/coq/list/Append.v Coqc lib/coq/list/NthLengthAppend.v Coqc lib/coq/list/Reverse.v Coqc lib/coq/floating_point/Rounding.v Coqc lib/coq/floating_point/GenFloat.v Coqc lib/coq/floating_point/SingleFormat.v Coqc lib/coq/floating_point/Single.v Coqc lib/coq/floating_point/DoubleFormat.v Coqc lib/coq/floating_point/Double.v Generate drivers/coq-realizations.aux echo "(* generated automatically at compilation time *)" > drivers/pvs-realizations.aux echo "(* generated automatically at compilation time *)" > drivers/isabelle-realizations.aux Ocamlopt lib/ocaml/why3__BigInt.ml Ocamlopt lib/ocaml/why3__IntAux.ml Ocamlopt lib/ocaml/why3__Array.ml Linking lib/why3/why3extract.cmx Linking lib/why3/why3extract.cmxa gcc -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -mtune=generic -o lib/why3-cpulimit src/tools/cpulimit.c Ocamlc src/why3doc/doc_html.mli Ocamlopt src/why3doc/doc_html.ml Ocamlc src/why3doc/doc_def.mli Ocamlopt src/why3doc/doc_def.ml Ocamlopt src/why3doc/doc_lexer.ml Ocamlopt src/why3doc/doc_main.ml Linking bin/why3doc.opt + make doc/manual.pdf cp -p lib/ocaml/why3__BigInt_zarith.ml lib/ocaml/why3__BigInt.ml ocamllex.opt doc/bnf.mll 91 states, 1859 transitions, table size 7982 bytes 1594 additional bytes used for bindings ocamlopt.opt -o doc/bnf doc/bnf.ml doc/bnf doc/qualid.bnf > doc/qualid_bnf.tex doc/bnf doc/label.bnf > doc/label_bnf.tex doc/bnf doc/constant.bnf > doc/constant_bnf.tex doc/bnf doc/operator.bnf > doc/operator_bnf.tex doc/bnf doc/term.bnf > doc/term_bnf.tex doc/bnf doc/type.bnf > doc/type_bnf.tex doc/bnf doc/formula.bnf > doc/formula_bnf.tex doc/bnf doc/theory.bnf > doc/theory_bnf.tex doc/bnf doc/theory2.bnf > doc/theory2_bnf.tex doc/bnf doc/why_file.bnf > doc/why_file_bnf.tex doc/bnf doc/spec.bnf > doc/spec_bnf.tex doc/bnf doc/expr.bnf > doc/expr_bnf.tex doc/bnf doc/expr2.bnf > doc/expr2_bnf.tex doc/bnf doc/module.bnf > doc/module_bnf.tex doc/bnf doc/whyml_file.bnf > doc/whyml_file_bnf.tex doc/bnf doc/term_old_at.bnf > doc/term_old_at_bnf.tex cd doc; rubber --warn all --pdf manual.tex compiling manual.tex... processing index manual.idx... This is makeindex, version 2.15 [TeX Live 2014] (kpathsea + Thai support). Scanning input file manual.idx....done (296 entries accepted, 0 rejected). Sorting entries.....done (2576 comparisons). Generating output file manual.ind....done (285 lines written, 0 warnings). Output written in manual.ind. Transcript written in manual.ilg. running BibTeX on manual... compiling manual.tex... compiling manual.tex... manual.toc:116: Overfull \hbox (1.91618pt too wide) (page 6) manual.toc:119: Overfull \hbox (1.91618pt too wide) (page 6) manual.toc:120: Overfull \hbox (1.91618pt too wide) (page 6) manual.toc:121: Overfull \hbox (1.91618pt too wide) (page 6) starting.tex: Underfull \vbox (badness 1348) has occurred while \output is active [] (page 9) syntaxref.tex:366: Overfull \hbox (16.9156pt too wide) (page 81) ../share/why3session.dtd:45-46: Overfull \hbox (137.37589pt too wide) (page 93) ../share/why3session.dtd: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 93) ../share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 96) ../share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 97) ../share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 98) ../share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 99) ../share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 100) ../share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 101) ../share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 102) manual.tex: Underfull \vbox (badness 6380) has occurred while \output is active [] (page 111) + exit 0 Executing(%install): /bin/sh -e /var/tmp/rpm-tmp.AjKtsI + umask 022 + cd /builddir/build/BUILD + '[' /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64 '!=' / ']' + rm -rf /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64 ++ dirname /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64 + mkdir -p /builddir/build/BUILDROOT + mkdir /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64 + cd why3-0.83 + make install DESTDIR=/builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64 cp -p lib/ocaml/why3__BigInt_zarith.ml lib/ocaml/why3__BigInt.ml rm -f /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3* rm -rf /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3 rm -rf /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/ocaml/why3 mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3 mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/images mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/images/boomy mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/images/fatcow mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/emacs mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/vim mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/lang mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/theories mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/modules/mach mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/drivers cp -p -f theories/*.why /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/theories cp -p -f modules/*.mlw /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/modules cp -p -f modules/mach/*.mlw /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/modules/mach cp -p -f drivers/*.drv drivers/*.gen /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/drivers cp -p -f share/provers-detection-data.conf /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/ cp -p -f share/images/icons.rc /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/images cp -p -f share/images/*.png /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/images cp -p -f share/images/boomy/*.png /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/images/boomy cp -p -f share/images/fatcow/*.png /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/images/fatcow cp -p -f share/why3session.dtd /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3 cp -p -rf share/javascript /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/javascript cp -p -f share/emacs/why3.el /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/emacs/why3.el cp -p -f share/vim/why3.vim /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/vim/why3.vim cp -p -f share/lang/why3.lang /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/lang/why3.lang rm -rf /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/plugins mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/plugins cp -p -f lib/plugins/genequlin.cmxs lib/plugins/dimacs.cmxs lib/plugins/tptp.cmxs lib/plugins/hypothesis_selection.cmxs /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/plugins cp -p -f bin/why3.opt /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3 cp -p -f bin/why3config.opt /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3config cp -p -f bin/why3ide.opt /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3ide cp -p -f bin/why3replayer.opt /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3replayer cp -p -f bin/why3session.opt /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3session cp -p -f bin/why3bench.opt /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3bench mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq-tactic cp -p -f lib/coq-tactic/* /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq-tactic mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq cp -p lib/coq/BuiltIn.vo /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/ mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/int cp -p lib/coq/int/Exponentiation.vo lib/coq/int/Abs.vo lib/coq/int/ComputerDivision.vo lib/coq/int/Div2.vo lib/coq/int/EuclideanDivision.vo lib/coq/int/Int.vo lib/coq/int/MinMax.vo lib/coq/int/Power.vo /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/int/ mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/bool cp -p lib/coq/bool/Bool.vo /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/bool/ mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/real cp -p lib/coq/real/Abs.vo lib/coq/real/ExpLog.vo lib/coq/real/FromInt.vo lib/coq/real/MinMax.vo lib/coq/real/PowerInt.vo lib/coq/real/Real.vo lib/coq/real/Square.vo lib/coq/real/RealInfix.vo /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/real/ mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/number cp -p lib/coq/number/Divisibility.vo lib/coq/number/Gcd.vo lib/coq/number/Parity.vo lib/coq/number/Prime.vo lib/coq/number/Coprime.vo /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/number/ mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/set cp -p lib/coq/set/Set.vo /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/set/ mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/map cp -p lib/coq/map/Map.vo lib/coq/map/Occ.vo lib/coq/map/MapPermut.vo lib/coq/map/MapInjection.vo /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/map/ mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/list cp -p lib/coq/list/List.vo lib/coq/list/Length.vo lib/coq/list/Mem.vo lib/coq/list/Nth.vo lib/coq/list/NthLength.vo lib/coq/list/HdTl.vo lib/coq/list/NthHdTl.vo lib/coq/list/Append.vo lib/coq/list/NthLengthAppend.vo lib/coq/list/Reverse.vo /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/list/ mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/option cp -p lib/coq/option/Option.vo /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/option/ mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/floating_point cp -p lib/coq/floating_point/GenFloat.vo lib/coq/floating_point/Rounding.vo lib/coq/floating_point/SingleFormat.vo lib/coq/floating_point/Single.vo lib/coq/floating_point/DoubleFormat.vo lib/coq/floating_point/Double.vo /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq/floating_point/ cp -p drivers/coq-realizations.aux /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/drivers/ cp -p drivers/pvs-realizations.aux /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/drivers/ cp -p drivers/isabelle-realizations.aux /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/drivers/ mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3 cp -p -f lib/why3-cpulimit /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/why3-cpulimit cp -p -f lib/why3-call-pvs /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/why3-call-pvs cp -p -f bin/why3doc.opt /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3doc if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then cp -p -f share/bash/why3 /etc/bash_completion.d; fi + mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/man/man1 + cd man + for f in '*.1' + sed s/@version@/0.83/ why3-cpulimit.1 + touch -r why3-cpulimit.1 /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/man/man1/why3-cpulimit.1 + for f in '*.1' + sed s/@version@/0.83/ why3.1 + touch -r why3.1 /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/man/man1/why3.1 + for f in '*.1' + sed s/@version@/0.83/ why3bench.1 + touch -r why3bench.1 /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/man/man1/why3bench.1 + for f in '*.1' + sed s/@version@/0.83/ why3config.1 + touch -r why3config.1 /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/man/man1/why3config.1 + for f in '*.1' + sed s/@version@/0.83/ why3doc.1 + touch -r why3doc.1 /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/man/man1/why3doc.1 + for f in '*.1' + sed s/@version@/0.83/ why3ide.1 + touch -r why3ide.1 /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/man/man1/why3ide.1 + for f in '*.1' + sed s/@version@/0.83/ why3ml.1 + touch -r why3ml.1 /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/man/man1/why3ml.1 + for f in '*.1' + sed s/@version@/0.83/ why3realize.1 + touch -r why3realize.1 /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/man/man1/why3realize.1 + for f in '*.1' + sed s/@version@/0.83/ why3replayer.1 + touch -r why3replayer.1 /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/man/man1/why3replayer.1 + cd .. + mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/bash-completion/completions + cp -p share/bash/why3 /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/bash-completion/completions + mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/zsh/site-functions + cp -p share/zsh/_why3 /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/zsh/site-functions + mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/texmf/tex/latex/why3 + cp -p share/latex/why3lang.sty /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/texmf/tex/latex/why3 + mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/gtksourceview-2.0 + mv /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/lang /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/gtksourceview-2.0/language-specs + mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/vim/vimfiles + mv /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/vim /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/vim/vimfiles/syntax + mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/xemacs/site-packages/lisp + cp -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/emacs/why3.el /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/xemacs/site-packages/lisp + pushd /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/xemacs/site-packages/lisp ~/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/xemacs/site-packages/lisp ~/build/BUILD/why3-0.83 + /usr/bin/xemacs -q -no-site-file -batch -eval '(push "." load-path)' -f batch-byte-compile why3.el Compiling /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/xemacs/site-packages/lisp/why3.el... While compiling why3-mode in file /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/xemacs/site-packages/lisp/why3.el: ** assignment to free variable font-lock-defaults Wrote /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/xemacs/site-packages/lisp/why3.elc Done + mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/emacs/site-lisp + mv /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/emacs/why3.el /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/emacs/site-lisp + rmdir /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/why3/emacs + cd /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/emacs/site-lisp + /usr/bin/emacs -batch --no-init-file --no-site-file --eval '(progn (setq load-path (cons "." load-path)))' -f batch-byte-compile why3.el Wrote /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/emacs/site-lisp/why3.elc ~/build/BUILD/why3-0.83 + popd + rm -fr /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/doc + chmod 0755 /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3 /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3bench /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3config /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3doc /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3ide /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3replayer /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3session /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq-tactic/why3tac.cmxs /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/plugins/dimacs.cmxs /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/plugins/genequlin.cmxs /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/plugins/hypothesis_selection.cmxs /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/plugins/tptp.cmxs /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/why3-cpulimit + /usr/lib/rpm/find-debuginfo.sh --strict-build-id -m --run-dwz --dwz-low-mem-die-limit 10000000 --dwz-max-die-limit 110000000 /builddir/build/BUILD/why3-0.83 extracting debug info from /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/coq-tactic/why3tac.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/why3-cpulimit extracting debug info from /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/plugins/hypothesis_selection.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/plugins/genequlin.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/plugins/tptp.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/lib64/why3/plugins/dimacs.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3ide extracting debug info from /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3bench extracting debug info from /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3replayer extracting debug info from /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3 extracting debug info from /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3config extracting debug info from /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3session extracting debug info from /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/bin/why3doc /usr/lib/rpm/sepdebugcrcfix: Updated 10 CRC32s, 3 CRC32s did match. cpio: ocaml-4.01.0/stdlib: Cannot stat: No such file or directory cpio: ocaml-4.01.0/stdlib/std_exit.ml: Cannot stat: No such file or directory cpio: why3-0.83/big_int.ml: Cannot stat: No such file or directory cpio: why3-0.83/buffer.ml: Cannot stat: No such file or directory cpio: why3-0.83/format.ml: Cannot stat: No such file or directory cpio: why3-0.83/hashtbl.ml: Cannot stat: No such file or directory cpio: why3-0.83/lexing.ml: Cannot stat: No such file or directory cpio: why3-0.83/list.ml: Cannot stat: No such file or directory cpio: why3-0.83/pervasives.ml: Cannot stat: No such file or directory cpio: why3-0.83/random.ml: Cannot stat: No such file or directory cpio: why3-0.83/stack.ml: Cannot stat: No such file or directory cpio: why3-0.83/str.ml: Cannot stat: No such file or directory cpio: why3-0.83/string.ml: Cannot stat: No such file or directory 5282 blocks + /usr/lib/rpm/check-buildroot + /usr/lib/rpm/brp-compress + /usr/lib/rpm/brp-strip-static-archive /usr/bin/strip + /usr/lib/rpm/brp-python-bytecompile /usr/bin/python 1 + /usr/lib/rpm/brp-python-hardlink + /usr/lib/rpm/redhat/brp-java-repack-jars Processing files: why3-0.83-7.fc21.x86_64 Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.CZ6KAU + umask 022 + cd /builddir/build/BUILD + cd why3-0.83 + DOCDIR=/builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/doc/why3 + export DOCDIR + /usr/bin/mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/doc/why3 + cp -pr AUTHORS /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/doc/why3 + cp -pr CHANGES /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/doc/why3 + cp -pr LICENSE /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/doc/why3 + cp -pr README /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/doc/why3 + cp -pr doc/manual.pdf /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/doc/why3 + exit 0 Provides: why3 = 0.83-7.fc21 why3(x86-64) = 0.83-7.fc21 Requires(interp): /bin/sh /bin/sh Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Requires(post): /bin/sh Requires(postun): /bin/sh tex(tex) Requires(posttrans): tex(tex) Requires: /bin/sh libatk-1.0.so.0()(64bit) libc.so.6()(64bit) libc.so.6(GLIBC_2.11)(64bit) libc.so.6(GLIBC_2.14)(64bit) libc.so.6(GLIBC_2.15)(64bit) libc.so.6(GLIBC_2.2.5)(64bit) libc.so.6(GLIBC_2.3)(64bit) libc.so.6(GLIBC_2.3.2)(64bit) libc.so.6(GLIBC_2.3.4)(64bit) libc.so.6(GLIBC_2.4)(64bit) libc.so.6(GLIBC_2.7)(64bit) libcairo.so.2()(64bit) libdl.so.2()(64bit) libdl.so.2(GLIBC_2.2.5)(64bit) libfontconfig.so.1()(64bit) libfreetype.so.6()(64bit) libgdk-x11-2.0.so.0()(64bit) libgdk_pixbuf-2.0.so.0()(64bit) libgio-2.0.so.0()(64bit) libglib-2.0.so.0()(64bit) libgobject-2.0.so.0()(64bit) libgtk-x11-2.0.so.0()(64bit) libgtksourceview-2.0.so.0()(64bit) libm.so.6()(64bit) libm.so.6(GLIBC_2.2.5)(64bit) libpango-1.0.so.0()(64bit) libpangocairo-1.0.so.0()(64bit) libpangoft2-1.0.so.0()(64bit) libpthread.so.0()(64bit) libpthread.so.0(GLIBC_2.2.5)(64bit) libpthread.so.0(GLIBC_2.3.2)(64bit) libsqlite3.so.0()(64bit) rtld(GNU_HASH) Processing files: why3-examples-0.83-7.fc21.noarch Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.r2wUua + umask 022 + cd /builddir/build/BUILD + cd why3-0.83 + DOCDIR=/builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/doc/why3-examples + export DOCDIR + /usr/bin/mkdir -p /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/doc/why3-examples + cp -pr examples /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64/usr/share/doc/why3-examples + exit 0 Provides: why3-examples = 0.83-7.fc21 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Processing files: why3-emacs-0.83-7.fc21.noarch Provides: why3-emacs = 0.83-7.fc21 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Processing files: why3-emacs-el-0.83-7.fc21.noarch Provides: why3-emacs-el = 0.83-7.fc21 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Processing files: why3-xemacs-0.83-7.fc21.noarch Provides: why3-xemacs = 0.83-7.fc21 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Processing files: why3-xemacs-el-0.83-7.fc21.noarch Provides: why3-xemacs-el = 0.83-7.fc21 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Processing files: why3-all-0.83-7.fc21.x86_64 Provides: why3-all = 0.83-7.fc21 why3-all(x86-64) = 0.83-7.fc21 Requires(rpmlib): rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 rpmlib(CompressedFileNames) <= 3.0.4-1 Processing files: why3-debuginfo-0.83-7.fc21.x86_64 Provides: why3-debuginfo = 0.83-7.fc21 why3-debuginfo(x86-64) = 0.83-7.fc21 Requires(rpmlib): rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 rpmlib(CompressedFileNames) <= 3.0.4-1 Checking for unpackaged file(s): /usr/lib/rpm/check-files /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64 Wrote: /builddir/build/RPMS/why3-0.83-7.fc21.x86_64.rpm Wrote: /builddir/build/RPMS/why3-examples-0.83-7.fc21.noarch.rpm Wrote: /builddir/build/RPMS/why3-emacs-0.83-7.fc21.noarch.rpm Wrote: /builddir/build/RPMS/why3-emacs-el-0.83-7.fc21.noarch.rpm Wrote: /builddir/build/RPMS/why3-xemacs-0.83-7.fc21.noarch.rpm Wrote: /builddir/build/RPMS/why3-xemacs-el-0.83-7.fc21.noarch.rpm Wrote: /builddir/build/RPMS/why3-all-0.83-7.fc21.x86_64.rpm Wrote: /builddir/build/RPMS/why3-debuginfo-0.83-7.fc21.x86_64.rpm Executing(%clean): /bin/sh -e /var/tmp/rpm-tmp.HWMLGu + umask 022 + cd /builddir/build/BUILD + cd why3-0.83 + /usr/bin/rm -rf /builddir/build/BUILDROOT/why3-0.83-7.fc21.x86_64 + exit 0 Child return code was: 0 LEAVE do -->