Mock Version: 1.2.8 Mock Version: 1.2.8 ENTER do(['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target armv7hl --nodeps /builddir/build/SPECS/why3.spec'], chrootPath='/var/lib/mock/f22-build-3352503-484417/root'shell=FalseprintOutput=Falseenv={'LANG': 'en_US.UTF-8', 'TERM': 'vt100', 'SHELL': '/bin/bash', 'PROMPT_COMMAND': 'printf "\x1b]0;\x07"', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'HOME': '/builddir', 'HOSTNAME': 'mock'}gid=425user='mockbuild'timeout=86400logger=uid=1000) Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target armv7hl --nodeps /builddir/build/SPECS/why3.spec'] with env {'LANG': 'en_US.UTF-8', 'TERM': 'vt100', 'SHELL': '/bin/bash', 'PROMPT_COMMAND': 'printf "\x1b]0;\x07"', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'HOME': '/builddir', 'HOSTNAME': 'mock'} and shell False warning: Could not canonicalize hostname: arm04-builder21.arm.fedoraproject.org Building target platforms: armv7hl Building for target armv7hl Wrote: /builddir/build/SRPMS/why3-0.86-1.fc22.src.rpm Child return code was: 0 LEAVE do --> ENTER do(['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --target armv7hl --nodeps /builddir/build/SPECS/why3.spec '], chrootPath='/var/lib/mock/f22-build-3352503-484417/root'shell=FalseprintOutput=Falseenv={'LANG': 'en_US.UTF-8', 'TERM': 'vt100', 'SHELL': '/bin/bash', 'PROMPT_COMMAND': 'printf "\x1b]0;\x07"', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'HOME': '/builddir', 'HOSTNAME': 'mock'}gid=425user='mockbuild'timeout=86400logger=uid=1000) Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --target armv7hl --nodeps /builddir/build/SPECS/why3.spec '] with env {'LANG': 'en_US.UTF-8', 'TERM': 'vt100', 'SHELL': '/bin/bash', 'PROMPT_COMMAND': 'printf "\x1b]0;\x07"', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'HOME': '/builddir', 'HOSTNAME': 'mock'} and shell False Building target platforms: armv7hl Building for target armv7hl Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.BvQJgi + umask 022 + cd /builddir/build/BUILD + cd /builddir/build/BUILD + rm -rf why3-0.86 + /usr/bin/gzip -dc /builddir/build/SOURCES/why3-0.86.tar.gz + /usr/bin/tar -xf - + STATUS=0 + '[' 0 -ne 0 ']' + cd why3-0.86 + /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w . + cd /builddir/build/BUILD + cd why3-0.86 + /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 . + 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 -march=armv7-a -mfpu=vfpv3-d16 -mfloat-abi=hard|' -e 's/cp /cp -p /' -e 's|Aer[[:digit:]-]*|& -ccopt "-Wl,-z,relro "|' -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.77LdO6 + umask 022 + cd /builddir/build/BUILD + cd why3-0.86 + 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 -march=armv7-a -mfpu=vfpv3-d16 -mfloat-abi=hard' + 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 -march=armv7-a -mfpu=vfpv3-d16 -mfloat-abi=hard' + 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 -march=armv7-a -mfpu=vfpv3-d16 -mfloat-abi=hard -I/usr/lib/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 -march=armv7-a -mfpu=vfpv3-d16 -mfloat-abi=hard -I/usr/lib/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=armv7hl-redhat-linux-gnu --host=armv7hl-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/lib --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 armv7hl-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.02.0 ocaml library path is /usr/lib/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 menhir... menhir checking for ocamlfind... yes checking for rubber... rubber checking for hevea... hevea checking for hacha... hacha checking for emacs... emacs ocamlfind found zarith in /usr/lib/ocaml/zarith ocamlfind found camlzip in /usr/lib/ocaml/zip ocamlfind found menhirLib in /usr/lib/ocaml/menhirLib ocamlfind found lablgtk2 in /usr/lib/ocaml/lablgtk2 ocamlfind found lablgtksourceview2 in /usr/lib/ocaml/lablgtk2 checking for coqc... coqc checking Coq version... 8.4pl6 checking for coqdep... coqdep checking for /usr/lib/coq/kernel/term.cmi... yes 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/lib/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 .merlin config.status: creating src/jessie/Makefile config.status: executing chmod commands configure: WARNING: unrecognized options: --disable-dependency-tracking Summary ----------------------------------------- Verbose make : no OCaml compiler : yes Version : 4.02.0 Library path : /usr/lib/ocaml Native compilation : yes Profiling : no Components IDE command : yes GMP arithmetic : yes Compressed sessions : yes MenhirLib support : yes Hypothesis selection : yes Frama-C support : no (disabled by default) Documentation : yes PDF : yes HTML : yes Support for interactive proof assistants Coq : yes Version : 8.4pl6 Library path : /usr/lib/coq "why3" tactic : yes Realization support : yes FP arithmetic : yes PVS : no (pvs not found) Isabelle : no (isabelle not found) Installable : yes Binary path : /usr/bin Lib path : /usr/lib/why3 Data path : ${prefix}/share/why3 Ocaml Library : /usr/lib/ocaml/why3 Relocatable : no + make Makefile:245: src/util/config.dep: No such file or directory Makefile:245: src/util/bigInt.dep: No such file or directory Makefile:245: src/util/util.dep: No such file or directory Makefile:245: src/util/opt.dep: No such file or directory Makefile:245: src/util/lists.dep: No such file or directory Makefile:245: src/util/strings.dep: No such file or directory Makefile:245: src/util/extmap.dep: No such file or directory Makefile:245: src/util/extset.dep: No such file or directory Makefile:245: src/util/exthtbl.dep: No such file or directory Makefile:245: src/util/weakhtbl.dep: No such file or directory Makefile:245: src/util/hashcons.dep: No such file or directory Makefile:245: src/util/stdlib.dep: No such file or directory Makefile:245: src/util/exn_printer.dep: No such file or directory Makefile:245: src/util/pp.dep: No such file or directory Makefile:245: src/util/debug.dep: No such file or directory Makefile:245: src/util/loc.dep: No such file or directory Makefile:245: src/util/lexlib.dep: No such file or directory Makefile:245: src/util/print_tree.dep: No such file or directory Makefile:245: src/util/cmdline.dep: No such file or directory Makefile:245: src/util/warning.dep: No such file or directory Makefile:245: src/util/sysutil.dep: No such file or directory Makefile:245: src/util/rc.dep: No such file or directory Makefile:245: src/util/plugin.dep: No such file or directory Makefile:245: src/util/bigInt.dep: No such file or directory Makefile:245: src/util/number.dep: No such file or directory Makefile:245: src/util/pqueue.dep: No such file or directory Makefile:245: src/core/ident.dep: No such file or directory Makefile:245: src/core/ty.dep: No such file or directory Makefile:245: src/core/term.dep: No such file or directory Makefile:245: src/core/pattern.dep: No such file or directory Makefile:245: src/core/decl.dep: No such file or directory Makefile:245: src/core/theory.dep: No such file or directory Makefile:245: src/core/task.dep: No such file or directory Makefile:245: src/core/pretty.dep: No such file or directory Makefile:245: src/core/dterm.dep: No such file or directory Makefile:245: src/core/env.dep: No such file or directory Makefile:245: src/core/trans.dep: No such file or directory Makefile:245: src/core/printer.dep: No such file or directory Makefile:245: src/core/model_parser.dep: No such file or directory Makefile:245: src/driver/call_provers.dep: No such file or directory Makefile:245: src/driver/driver_ast.dep: No such file or directory Makefile:245: src/driver/driver_parser.dep: No such file or directory Makefile:245: src/driver/driver_lexer.dep: No such file or directory Makefile:245: src/driver/driver.dep: No such file or directory Makefile:245: src/driver/whyconf.dep: No such file or directory Makefile:245: src/driver/autodetection.dep: No such file or directory Makefile:245: src/driver/parse_cvc4_z3_model.dep: No such file or directory Makefile:245: src/mlw/ity.dep: No such file or directory Makefile:245: src/mlw/expr.dep: No such file or directory Makefile:245: src/mlw/dexpr.dep: No such file or directory Makefile:245: src/parser/ptree.dep: No such file or directory Makefile:245: src/parser/glob.dep: No such file or directory Makefile:245: src/parser/parser.dep: No such file or directory Makefile:245: src/parser/typing.dep: No such file or directory Makefile:245: src/parser/lexer.dep: No such file or directory Makefile:245: src/transform/simplify_formula.dep: No such file or directory Makefile:245: src/transform/inlining.dep: No such file or directory Makefile:245: src/transform/split_goal.dep: No such file or directory Makefile:245: src/transform/induction.dep: No such file or directory Makefile:245: src/transform/detect_polymorphism.dep: No such file or directory Makefile:245: src/transform/eliminate_definition.dep: No such file or directory Makefile:245: src/transform/eliminate_algebraic.dep: No such file or directory Makefile:245: src/transform/eliminate_inductive.dep: No such file or directory Makefile:245: src/transform/eliminate_let.dep: No such file or directory Makefile:245: src/transform/eliminate_if.dep: No such file or directory Makefile:245: src/transform/libencoding.dep: No such file or directory Makefile:245: src/transform/discriminate.dep: No such file or directory Makefile:245: src/transform/encoding.dep: No such file or directory Makefile:245: src/transform/encoding_select.dep: No such file or directory Makefile:245: src/transform/encoding_guards_full.dep: No such file or directory Makefile:245: src/transform/encoding_tags_full.dep: No such file or directory Makefile:245: src/transform/encoding_guards.dep: No such file or directory Makefile:245: src/transform/encoding_tags.dep: No such file or directory Makefile:245: src/transform/encoding_twin.dep: No such file or directory Makefile:245: src/transform/encoding_sort.dep: No such file or directory Makefile:245: src/transform/simplify_array.dep: No such file or directory Makefile:245: src/transform/filter_trigger.dep: No such file or directory Makefile:245: src/transform/introduction.dep: No such file or directory Makefile:245: src/transform/abstraction.dep: No such file or directory Makefile:245: src/transform/close_epsilon.dep: No such file or directory Makefile:245: src/transform/lift_epsilon.dep: No such file or directory Makefile:245: src/transform/eliminate_epsilon.dep: No such file or directory Makefile:245: src/transform/intro_projections_counterexmp.dep: No such file or directory Makefile:245: src/transform/eval_match.dep: No such file or directory Makefile:245: src/transform/instantiate_predicate.dep: No such file or directory Makefile:245: src/transform/smoke_detector.dep: No such file or directory Makefile:245: src/transform/reduction_engine.dep: No such file or directory Makefile:245: src/transform/compute.dep: No such file or directory Makefile:245: src/transform/induction_pr.dep: No such file or directory Makefile:245: src/transform/prop_curry.dep: No such file or directory Makefile:245: src/printer/alt_ergo.dep: No such file or directory Makefile:245: src/printer/why3printer.dep: No such file or directory Makefile:245: src/printer/smtv1.dep: No such file or directory Makefile:245: src/printer/smtv2.dep: No such file or directory Makefile:245: src/printer/coq.dep: No such file or directory Makefile:245: src/printer/pvs.dep: No such file or directory Makefile:245: src/printer/isabelle.dep: No such file or directory Makefile:245: src/printer/simplify.dep: No such file or directory Makefile:245: src/printer/gappa.dep: No such file or directory Makefile:245: src/printer/cvc3.dep: No such file or directory Makefile:245: src/printer/yices.dep: No such file or directory Makefile:245: src/printer/mathematica.dep: No such file or directory Makefile:245: src/whyml/mlw_ty.dep: No such file or directory Makefile:245: src/whyml/mlw_expr.dep: No such file or directory Makefile:245: src/whyml/mlw_decl.dep: No such file or directory Makefile:245: src/whyml/mlw_pretty.dep: No such file or directory Makefile:245: src/whyml/mlw_wp.dep: No such file or directory Makefile:245: src/whyml/mlw_module.dep: No such file or directory Makefile:245: src/whyml/mlw_dexpr.dep: No such file or directory Makefile:245: src/whyml/mlw_typing.dep: No such file or directory Makefile:245: src/whyml/mlw_driver.dep: No such file or directory Makefile:245: src/whyml/mlw_exec.dep: No such file or directory Makefile:245: src/whyml/mlw_ocaml.dep: No such file or directory Makefile:245: src/whyml/mlw_main.dep: No such file or directory Makefile:245: src/whyml/mlw_interp.dep: No such file or directory Makefile:245: src/session/compress.dep: No such file or directory Makefile:245: src/session/xml.dep: No such file or directory Makefile:245: src/session/termcode.dep: No such file or directory Makefile:245: src/session/session.dep: No such file or directory Makefile:245: src/session/session_tools.dep: No such file or directory Makefile:245: src/session/strategy.dep: No such file or directory Makefile:245: src/session/strategy_parser.dep: No such file or directory Makefile:245: src/session/session_scheduler.dep: No such file or directory Makefile:428: plugins/parser/genequlin.dep: No such file or directory Makefile:428: plugins/parser/dimacs.dep: No such file or directory Makefile:428: plugins/transform/hypothesis_selection.dep: No such file or directory Makefile:428: plugins/tptp/tptp_ast.dep: No such file or directory Makefile:428: plugins/tptp/tptp_parser.dep: No such file or directory Makefile:428: plugins/tptp/tptp_typing.dep: No such file or directory Makefile:428: plugins/tptp/tptp_lexer.dep: No such file or directory Makefile:428: plugins/tptp/tptp_printer.dep: No such file or directory Makefile:549: src/tools/main.dep: No such file or directory Makefile:549: src/tools/why3config.dep: No such file or directory Makefile:549: src/tools/why3execute.dep: No such file or directory Makefile:549: src/tools/why3extract.dep: No such file or directory Makefile:549: src/tools/why3prove.dep: No such file or directory Makefile:549: src/tools/why3realize.dep: No such file or directory Makefile:549: src/tools/why3replay.dep: No such file or directory Makefile:549: src/tools/why3wc.dep: No such file or directory Makefile:689: src/ide/gconfig.dep: No such file or directory Makefile:689: src/ide/gmain.dep: No such file or directory Ocamllex src/why3doc/doc_lexer.mll Makefile:740: src/why3session/why3session_lib.dep: No such file or directory Makefile:740: src/why3session/why3session_copy.dep: No such file or directory Makefile:740: src/why3session/why3session_info.dep: No such file or directory Makefile:740: src/why3session/why3session_latex.dep: No such file or directory Makefile:740: src/why3session/why3session_html.dep: No such file or directory Makefile:740: src/why3session/why3session_rm.dep: No such file or directory Makefile:740: src/why3session/why3session_output.dep: No such file or directory Makefile:740: src/why3session/why3session_run.dep: No such file or directory Makefile:740: src/why3session/why3session_csv.dep: No such file or directory Makefile:740: src/why3session/why3session_main.dep: No such file or directory Makefile:816: src/coq-tactic/why3tac.dep: No such file or directory Makefile:991: lib/coq/BuiltIn.vd: No such file or directory Makefile:991: lib/coq/HighOrd.vd: No such file or directory Makefile:991: lib/coq/int/Exponentiation.vd: No such file or directory Makefile:991: lib/coq/int/Abs.vd: No such file or directory Makefile:991: lib/coq/int/ComputerDivision.vd: No such file or directory Makefile:991: lib/coq/int/Div2.vd: No such file or directory Makefile:991: lib/coq/int/EuclideanDivision.vd: No such file or directory Makefile:991: lib/coq/int/Int.vd: No such file or directory Makefile:991: lib/coq/int/MinMax.vd: No such file or directory Makefile:991: lib/coq/int/Power.vd: No such file or directory Makefile:991: lib/coq/bool/Bool.vd: No such file or directory Makefile:991: lib/coq/real/Abs.vd: No such file or directory Makefile:991: lib/coq/real/ExpLog.vd: No such file or directory Makefile:991: lib/coq/real/FromInt.vd: No such file or directory Makefile:991: lib/coq/real/MinMax.vd: No such file or directory Makefile:991: lib/coq/real/PowerInt.vd: No such file or directory Makefile:991: lib/coq/real/PowerReal.vd: No such file or directory Makefile:991: lib/coq/real/Real.vd: No such file or directory Makefile:991: lib/coq/real/RealInfix.vd: No such file or directory Makefile:991: lib/coq/real/Square.vd: No such file or directory Makefile:991: lib/coq/real/Trigonometry.vd: No such file or directory Makefile:991: lib/coq/number/Divisibility.vd: No such file or directory Makefile:991: lib/coq/number/Gcd.vd: No such file or directory Makefile:991: lib/coq/number/Parity.vd: No such file or directory Makefile:991: lib/coq/number/Prime.vd: No such file or directory Makefile:991: lib/coq/number/Coprime.vd: No such file or directory Makefile:991: lib/coq/set/Set.vd: No such file or directory Makefile:991: lib/coq/map/Map.vd: No such file or directory Makefile:991: lib/coq/map/Occ.vd: No such file or directory Makefile:991: lib/coq/map/MapPermut.vd: No such file or directory Makefile:991: lib/coq/map/MapInjection.vd: No such file or directory Makefile:991: lib/coq/list/List.vd: No such file or directory Makefile:991: lib/coq/list/Length.vd: No such file or directory Makefile:991: lib/coq/list/Mem.vd: No such file or directory Makefile:991: lib/coq/list/Nth.vd: No such file or directory Makefile:991: lib/coq/list/NthLength.vd: No such file or directory Makefile:991: lib/coq/list/HdTl.vd: No such file or directory Makefile:991: lib/coq/list/NthHdTl.vd: No such file or directory Makefile:991: lib/coq/list/Append.vd: No such file or directory Makefile:991: lib/coq/list/NthLengthAppend.vd: No such file or directory Makefile:991: lib/coq/list/Reverse.vd: No such file or directory Makefile:991: lib/coq/list/HdTlNoOpt.vd: No such file or directory Makefile:991: lib/coq/list/NthNoOpt.vd: No such file or directory Makefile:991: lib/coq/list/RevAppend.vd: No such file or directory Makefile:991: lib/coq/list/Combine.vd: No such file or directory Makefile:991: lib/coq/list/Distinct.vd: No such file or directory Makefile:991: lib/coq/list/NumOcc.vd: No such file or directory Makefile:991: lib/coq/list/Permut.vd: No such file or directory Makefile:991: lib/coq/option/Option.vd: No such file or directory Makefile:991: lib/coq/seq/Seq.vd: No such file or directory Makefile:991: lib/coq/floating_point/GenFloat.vd: No such file or directory Makefile:991: lib/coq/floating_point/Rounding.vd: No such file or directory Makefile:991: lib/coq/floating_point/SingleFormat.vd: No such file or directory Makefile:991: lib/coq/floating_point/Single.vd: No such file or directory Makefile:991: lib/coq/floating_point/DoubleFormat.vd: No such file or directory Makefile:991: lib/coq/floating_point/Double.vd: No such file or directory Makefile:1276: lib/ocaml/why3__BigInt_compat.dep: No such file or directory Makefile:1276: lib/ocaml/why3__BigInt.dep: No such file or directory Makefile:1276: lib/ocaml/why3__IntAux.dep: No such file or directory Makefile:1276: lib/ocaml/why3__Array.dep: No such file or directory Makefile:1364: src/why3doc/doc_html.dep: No such file or directory Makefile:1364: src/why3doc/doc_def.dep: No such file or directory Makefile:1364: src/why3doc/doc_lexer.dep: No such file or directory Makefile:1364: src/why3doc/doc_main.dep: No such file or directory 112 states, 1119 transitions, table size 5148 bytes 1707 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_compat.ml Ocamldep lib/ocaml/why3__Array.ml Ocamldep lib/ocaml/why3__IntAux.ml Ocamldep lib/ocaml/why3__BigInt.ml Ocamldep lib/ocaml/why3__BigInt_compat.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/seq/Seq.v Coqdep lib/coq/option/Option.v Coqdep lib/coq/list/Permut.v Coqdep lib/coq/list/NumOcc.v Coqdep lib/coq/list/Distinct.v Coqdep lib/coq/list/Combine.v Coqdep lib/coq/list/RevAppend.v Coqdep lib/coq/list/NthNoOpt.v Coqdep lib/coq/list/HdTlNoOpt.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/Trigonometry.v Coqdep lib/coq/real/Square.v Coqdep lib/coq/real/RealInfix.v Coqdep lib/coq/real/Real.v Coqdep lib/coq/real/PowerReal.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/HighOrd.v Coqdep lib/coq/BuiltIn.v Camlp src/coq-tactic/why3tac.ml4 Ocamldep src/coq-tactic/why3tac.ml Ocamldep src/why3session/why3session_main.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/ide/gmain.ml Ocamldep src/ide/gconfig.ml Ocamllex src/tools/why3wc.mll 298 states, 15365 transitions, table size 63248 bytes Ocamldep src/tools/why3wc.ml Ocamldep src/tools/why3replay.ml Ocamldep src/tools/why3realize.ml Ocamldep src/tools/why3prove.ml Ocamldep src/tools/why3extract.ml Ocamldep src/tools/why3execute.ml Ocamldep src/tools/why3config.ml Ocamldep src/tools/main.ml Ocamllex plugins/tptp/tptp_lexer.mll 101 states, 1563 transitions, table size 6858 bytes 3126 additional bytes used for bindings Menhir plugins/tptp/tptp_parser.mly Warning: you are using the standard library and/or the %inline keyword. We recommend switching on --infer in order to avoid obscure type error messages. 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/util/lexlib.mll 16 states, 260 transitions, table size 1136 bytes Ocamllex src/parser/lexer.mll 128 states, 3177 transitions, table size 13476 bytes 7458 additional bytes used for bindings Menhir src/parser/parser.mly Warning: you are using the standard library and/or the %inline keyword. We recommend switching on --infer in order to avoid obscure type error messages. Menhir src/driver/driver_parser.mly Ocamllex src/driver/driver_lexer.mll 29 states, 1101 transitions, table size 4578 bytes cp -p src/session/compress_z.ml src/session/compress.ml Ocamllex src/session/xml.mll 114 states, 1396 transitions, table size 6268 bytes 3538 additional bytes used for bindings Ocamllex src/session/strategy_parser.mll 39 states, 619 transitions, table size 2710 bytes 1755 additional bytes used for bindings Ocamldep src/session/session_scheduler.ml Ocamldep src/session/strategy_parser.ml Ocamldep src/session/strategy.ml Ocamldep src/session/session_tools.ml Ocamldep src/session/session.ml Ocamldep src/session/termcode.ml Ocamldep src/session/xml.ml Ocamldep src/session/compress.ml Ocamldep src/whyml/mlw_interp.ml Ocamldep src/whyml/mlw_main.ml Ocamldep src/whyml/mlw_ocaml.ml Ocamldep src/whyml/mlw_exec.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/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/prop_curry.ml Ocamldep src/transform/induction_pr.ml Ocamldep src/transform/compute.ml Ocamldep src/transform/reduction_engine.ml Ocamldep src/transform/smoke_detector.ml Ocamldep src/transform/instantiate_predicate.ml Ocamldep src/transform/eval_match.ml Ocamldep src/transform/intro_projections_counterexmp.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/detect_polymorphism.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/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/mlw/dexpr.ml Ocamldep src/mlw/expr.ml Ocamldep src/mlw/ity.ml Ocamldep src/driver/parse_cvc4_z3_model.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/core/model_parser.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/lexlib.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_compat.ml cp -p src/session/compress_z.ml src/session/compress.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 File "src/util/strings.ml", line 36, characters 12-25: Warning 3: deprecated: String.create File "src/util/strings.ml", line 38, characters 4-15: Warning 3: deprecated: String.fill 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/lexlib.mli Ocamlopt src/util/lexlib.ml File "src/util/lexlib.mll", line 101, characters 14-27: Warning 3: deprecated: String.create File "src/util/lexlib.mll", line 103, characters 46-56: Warning 3: deprecated: String.set Ocamlc src/util/print_tree.mli Ocamlopt src/util/print_tree.ml Ocamlc src/util/cmdline.mli Ocamlopt src/util/cmdline.ml File "src/util/cmdline.ml", line 46, characters 16-29: Warning 3: deprecated: String.create File "src/util/cmdline.ml", line 48, characters 10-20: Warning 3: deprecated: String.set 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 File "src/util/rc.mll", line 67, characters 13-26: Warning 3: deprecated: String.create File "src/util/rc.mll", line 73, characters 10-27: Warning 3: deprecated: String.unsafe_set File "src/util/rc.mll", line 76, characters 6-23: Warning 3: deprecated: String.unsafe_set Ocamlc src/util/plugin.mli Ocamlopt src/util/plugin.ml Ocamlc src/util/number.mli Ocamlopt src/util/number.ml File "src/util/number.ml", line 161, characters 14-25: Warning 3: deprecated: String.copy File "src/util/number.ml", line 161, characters 31-44: Warning 3: deprecated: String.set 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 Ocamlc src/core/model_parser.mli Ocamlopt src/core/model_parser.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 Ocamlopt src/driver/parse_cvc4_z3_model.ml Ocamlc src/mlw/ity.mli Ocamlopt src/mlw/ity.ml Ocamlc src/mlw/expr.mli Ocamlopt src/mlw/expr.ml File "src/mlw/expr.ml", line 440, characters 34-46: Warning 48: implicit elimination of optional argument ?loc Ocamlc src/mlw/dexpr.mli Ocamlopt src/mlw/dexpr.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/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/detect_polymorphism.mli Ocamlopt src/transform/detect_polymorphism.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/intro_projections_counterexmp.mli Ocamlopt src/transform/intro_projections_counterexmp.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/transform/reduction_engine.mli Ocamlopt src/transform/reduction_engine.ml Ocamlc src/transform/compute.mli Ocamlopt src/transform/compute.ml Ocamlc src/transform/induction_pr.mli Ocamlopt src/transform/induction_pr.ml Ocamlopt src/transform/prop_curry.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 File "src/printer/coq.ml", line 481, characters 14-27: Warning 3: deprecated: String.create 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/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_exec.mli Ocamlopt src/whyml/mlw_exec.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 Ocamlc src/session/compress.mli Ocamlopt src/session/compress.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 File "src/session/session.ml", line 1517, characters 10-23: Warning 3: deprecated: String.create File "src/session/session.ml", line 1546, characters 16-27: Warning 3: deprecated: String.copy Ocamlc src/session/session_tools.mli Ocamlopt src/session/session_tools.ml Ocamlc src/session/strategy.mli Ocamlopt src/session/strategy.ml Ocamlc src/session/strategy_parser.mli Ocamlopt src/session/strategy_parser.ml Ocamlc src/session/session_scheduler.mli Ocamlopt src/session/session_scheduler.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/tools/main.ml Linking bin/why3.opt Ocamlopt src/tools/why3config.ml Linking bin/why3config.opt Ocamlopt src/tools/why3execute.ml Linking bin/why3execute.opt Ocamlopt src/tools/why3extract.ml Linking bin/why3extract.opt Ocamlopt src/tools/why3prove.ml Linking bin/why3prove.opt Ocamlopt src/tools/why3realize.ml Linking bin/why3realize.opt Ocamlopt src/tools/why3replay.ml Linking bin/why3replay.opt Ocamlopt src/tools/why3wc.ml Linking bin/why3wc.opt Ocamlc src/ide/resetgc.c Ocamlc src/ide/gconfig.mli Ocamlopt src/ide/gconfig.ml Ocamlopt src/ide/gmain.ml Linking bin/why3ide.opt Ocamlc src/why3session/why3session_lib.mli Ocamlopt src/why3session/why3session_lib.ml File "src/why3session/why3session_lib.ml", line 252, characters 10-23: Warning 3: deprecated: String.create 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_main.ml Linking bin/why3session.opt Coqc lib/coq/BuiltIn.v Ocamlopt src/coq-tactic/why3tac.ml Linking lib/coq-tactic/why3tac.cmxs Coqc lib/coq-tactic/Why3.v Coqc lib/coq/HighOrd.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/real/PowerReal.v Coqc lib/coq/real/Trigonometry.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/list/HdTlNoOpt.v Coqc lib/coq/list/NthNoOpt.v Coqc lib/coq/list/RevAppend.v Coqc lib/coq/list/Combine.v Coqc lib/coq/list/Distinct.v Coqc lib/coq/list/NumOcc.v Coqc lib/coq/list/Permut.v Coqc lib/coq/seq/Seq.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_compat.ml 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 -march=armv7-a -mfpu=vfpv3-d16 -mfloat-abi=hard -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_compat.ml cp -p src/session/compress_z.ml src/session/compress.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 (340 entries accepted, 0 rejected). Sorting entries......done (3100 comparisons). Generating output file manual.ind....done (322 lines written, 0 warnings). Output written in manual.ind. Transcript written in manual.ilg. running BibTeX on manual... compiling 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 (340 entries accepted, 0 rejected). Sorting entries......done (3100 comparisons). Generating output file manual.ind....done (322 lines written, 0 warnings). Output written in manual.ind. Transcript written in manual.ilg. compiling manual.tex... manual.toc:124: Overfull \hbox (1.91618pt too wide) (page 6) manual.toc:127: Overfull \hbox (1.91618pt too wide) (page 6) manual.toc:128: Overfull \hbox (1.91618pt too wide) (page 6) manual.toc:129: Overfull \hbox (1.91618pt too wide) (page 7) starting.tex: Underfull \vbox (badness 1348) has occurred while \output is active [] (page 11) manpages.tex:669: Overfull \hbox (3.7864pt too wide) (page 68) syntaxref.tex:366: Overfull \hbox (16.9156pt too wide) (page 83) ../share/why3session.dtd:48-49: Overfull \hbox (137.37589pt too wide) (page 95) ../share/why3session.dtd: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 95) ../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) ../share/provers-detection-data.conf:354-356: Overfull \hbox (89.024pt too wide) (page 103) ../share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 103) ../share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 104) ../share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 105) manual.tex: Underfull \vbox (badness 6380) has occurred while \output is active [] (page 115) manual.ind:260-261: Underfull \hbox (badness 10000) (page 123) manual.ind:261-262: Overfull \hbox (31.74225pt too wide) (page 123) + exit 0 Executing(%install): /bin/sh -e /var/tmp/rpm-tmp.fnAQi7 + umask 022 + cd /builddir/build/BUILD + '[' /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm '!=' / ']' + rm -rf /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm ++ dirname /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm + mkdir -p /builddir/build/BUILDROOT + mkdir /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm + cd why3-0.86 + make install DESTDIR=/builddir/build/BUILDROOT/why3-0.86-1.fc22.arm cp -p lib/ocaml/why3__BigInt_zarith.ml lib/ocaml/why3__BigInt_compat.ml cp -p src/session/compress_z.ml src/session/compress.ml rm -rf /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3 rm -rf /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3 rm -rf /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/ocaml/why3 rm -f /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/emacs/site-lisp/why3.el rm -f /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/emacs/site-lisp/why3.elc rm -f /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3config /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3execute /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3extract /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3prove /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3realize /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3replay /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3wc /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/bin/why3 rm -f /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/bin/why3bench /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/bin/why3replayer rm -f /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/bin/why3ide rm -f /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/bin/why3session rm -f /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/bin/why3doc if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then rm -f /etc/bash_completion.d/why3; fi emacs --batch --no-init-file -f batch-byte-compile share/emacs/why3.el Loading /usr/share/emacs/site-lisp/site-start.d/desktop-entry-mode-init.el (source)... Wrote /builddir/build/BUILD/why3-0.86/share/emacs/why3.elc mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/bin mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3 mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3 mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/images mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/images/boomy mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/images/fatcow mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/vim mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/lang mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/theories mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/modules/mach mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/drivers mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/emacs/site-lisp/ cp -p -f theories/*.why /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/theories cp -p -f modules/*.mlw /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/modules cp -p -f modules/mach/*.mlw /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/modules/mach cp -p -f drivers/*.drv drivers/*.gen /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/drivers cp -p -f LICENSE /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/ cp -p -f share/provers-detection-data.conf /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/ cp -p -f share/images/icons.rc /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/images cp -p -f share/images/*.png /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/images cp -p -f share/images/boomy/* /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/images/boomy cp -p -f share/images/fatcow/* /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/images/fatcow cp -p -f share/why3session.dtd /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3 cp -p -f share/Makefile.config /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3 cp -p -rf share/javascript /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/javascript cp -p -f share/vim/why3.vim /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/vim/why3.vim cp -p -f share/lang/why3.lang /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/lang/why3.lang cp -p -f share/emacs/why3.el /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/emacs/site-lisp/why3.el cp -p -f share/emacs/why3.elc /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/emacs/site-lisp/why3.elc mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/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.86-1.fc22.arm/usr/lib/why3/plugins cp -p -f bin/why3.opt /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/bin/why3 cp -p -f bin/why3config.opt /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3config cp -p -f bin/why3execute.opt /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3execute cp -p -f bin/why3extract.opt /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3extract cp -p -f bin/why3prove.opt /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3prove cp -p -f bin/why3realize.opt /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3realize cp -p -f bin/why3replay.opt /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3replay cp -p -f bin/why3wc.opt /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3wc cp -p -f bin/why3ide.opt /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3ide cp -p -f bin/why3session.opt /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3session mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq-tactic cp -p -f lib/coq-tactic/* /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq-tactic mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq cp -p lib/coq/BuiltIn.vo lib/coq/HighOrd.vo /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq/ mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/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.86-1.fc22.arm/usr/lib/why3/coq/int/ mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq/bool cp -p lib/coq/bool/Bool.vo /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq/bool/ mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/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/PowerReal.vo lib/coq/real/Real.vo lib/coq/real/RealInfix.vo lib/coq/real/Square.vo lib/coq/real/Trigonometry.vo /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq/real/ mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/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.86-1.fc22.arm/usr/lib/why3/coq/number/ mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq/set cp -p lib/coq/set/Set.vo /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq/set/ mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/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.86-1.fc22.arm/usr/lib/why3/coq/map/ mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/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 lib/coq/list/HdTlNoOpt.vo lib/coq/list/NthNoOpt.vo lib/coq/list/RevAppend.vo lib/coq/list/Combine.vo lib/coq/list/Distinct.vo lib/coq/list/NumOcc.vo lib/coq/list/Permut.vo /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq/list/ mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq/option cp -p lib/coq/option/Option.vo /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq/option/ mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq/seq cp -p lib/coq/seq/Seq.vo /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq/seq/ mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/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.86-1.fc22.arm/usr/lib/why3/coq/floating_point/ cp -p drivers/coq-realizations.aux /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/drivers/ cp -p drivers/pvs-realizations.aux /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/drivers/ cp -p drivers/isabelle-realizations.aux /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/drivers/ cp -p -f lib/why3-cpulimit /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/why3-cpulimit cp -p -f lib/why3-call-pvs /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/why3-call-pvs cp -p -f bin/why3doc.opt /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/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.86-1.fc22.arm/usr/share/man/man1 + cd man + for f in '*.1' + sed s/@version@/0.86/ why3-cpulimit.1 + touch -r why3-cpulimit.1 /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/man/man1/why3-cpulimit.1 + for f in '*.1' + sed s/@version@/0.86/ why3.1 + touch -r why3.1 /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/man/man1/why3.1 + for f in '*.1' + sed s/@version@/0.86/ why3bench.1 + touch -r why3bench.1 /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/man/man1/why3bench.1 + for f in '*.1' + sed s/@version@/0.86/ why3config.1 + touch -r why3config.1 /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/man/man1/why3config.1 + for f in '*.1' + sed s/@version@/0.86/ why3doc.1 + touch -r why3doc.1 /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/man/man1/why3doc.1 + for f in '*.1' + sed s/@version@/0.86/ why3ide.1 + touch -r why3ide.1 /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/man/man1/why3ide.1 + for f in '*.1' + sed s/@version@/0.86/ why3ml.1 + touch -r why3ml.1 /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/man/man1/why3ml.1 + for f in '*.1' + sed s/@version@/0.86/ why3realize.1 + touch -r why3realize.1 /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/man/man1/why3realize.1 + for f in '*.1' + sed s/@version@/0.86/ why3replayer.1 + touch -r why3replayer.1 /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/man/man1/why3replayer.1 + cd .. + mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/bash-completion/completions + cp -p share/bash/why3 /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/bash-completion/completions + mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/zsh/site-functions + cp -p share/zsh/_why3 /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/zsh/site-functions + mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/texmf/tex/latex/why3 + cp -p share/latex/why3lang.sty /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/texmf/tex/latex/why3 + mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/gtksourceview-2.0 + mv /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/lang /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/gtksourceview-2.0/language-specs + mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/vim/vimfiles + mv /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/why3/vim /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/vim/vimfiles/syntax + mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/xemacs/site-packages/lisp + cp -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/emacs/site-lisp/why3.el /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/xemacs/site-packages/lisp + pushd /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/xemacs/site-packages/lisp ~/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/xemacs/site-packages/lisp ~/build/BUILD/why3-0.86 + /usr/bin/xemacs -q -no-site-file -batch -eval '(push "." load-path)' -f batch-byte-compile why3.el Compiling /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/xemacs/site-packages/lisp/why3.el... While compiling why3-mode in file /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/xemacs/site-packages/lisp/why3.el: ** assignment to free variable font-lock-defaults Wrote /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/xemacs/site-packages/lisp/why3.elc Done+ cd /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/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.86-1.fc22.arm/usr/share/emacs/site-lisp/why3.elc + popd ~/build/BUILD/why3-0.86 + rm -fr /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/doc + chmod 0755 /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/bin/why3 /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3config /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3doc /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3execute /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3extract /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3ide /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3prove /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3realize /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3replay /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3session /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3wc /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq-tactic/why3tac.cmxs /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/plugins/dimacs.cmxs /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/plugins/genequlin.cmxs /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/plugins/hypothesis_selection.cmxs /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/plugins/tptp.cmxs /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/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 50000000 /builddir/build/BUILD/why3-0.86 extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/coq-tactic/why3tac.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/why3-cpulimit extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/plugins/dimacs.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/plugins/hypothesis_selection.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/plugins/genequlin.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/plugins/tptp.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3execute extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3realize extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3ide extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3wc extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3session extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3prove extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3replay extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3config extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3extract extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/lib/why3/commands/why3doc extracting debug info from /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/bin/why3 /usr/lib/rpm/sepdebugcrcfix: Updated 14 CRC32s, 3 CRC32s did match. cpio: menhir-20141215/src/_stage2: Cannot stat: No such file or directory cpio: menhir-20141215/src/_stage2/convert.ml: Cannot stat: No such file or directory cpio: menhir-20141215/src/_stage2/engine.ml: Cannot stat: No such file or directory cpio: menhir-20141215/src/_stage2/infiniteArray.ml: Cannot stat: No such file or directory cpio: menhir-20141215/src/_stage2/packedIntArray.ml: Cannot stat: No such file or directory cpio: menhir-20141215/src/_stage2/rowDisplacement.ml: Cannot stat: No such file or directory cpio: menhir-20141215/src/_stage2/tableInterpreter.ml: Cannot stat: No such file or directory cpio: ocaml-4.02.0/stdlib: Cannot stat: No such file or directory cpio: ocaml-4.02.0/stdlib/std_exit.ml: Cannot stat: No such file or directory cpio: why3-0.86/big_int.ml: Cannot stat: No such file or directory cpio: why3-0.86/buffer.ml: Cannot stat: No such file or directory cpio: why3-0.86/bytes.ml: Cannot stat: No such file or directory cpio: why3-0.86/format.ml: Cannot stat: No such file or directory cpio: why3-0.86/gdkPixbuf.ml: Cannot stat: No such file or directory cpio: why3-0.86/gtkMain.ml: Cannot stat: No such file or directory cpio: why3-0.86/hashtbl.ml: Cannot stat: No such file or directory cpio: why3-0.86/lexing.ml: Cannot stat: No such file or directory cpio: why3-0.86/list.ml: Cannot stat: No such file or directory cpio: why3-0.86/pervasives.ml: Cannot stat: No such file or directory cpio: why3-0.86/random.ml: Cannot stat: No such file or directory cpio: why3-0.86/stack.ml: Cannot stat: No such file or directory cpio: why3-0.86/str.ml: Cannot stat: No such file or directory cpio: why3-0.86/string.ml: Cannot stat: No such file or directory 7737 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.86-1.fc22.armv7hl Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.Ni03Uh + umask 022 + cd /builddir/build/BUILD + cd why3-0.86 + DOCDIR=/builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/doc/why3 + export DOCDIR + /usr/bin/mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/doc/why3 + cp -pr AUTHORS /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/doc/why3 + cp -pr CHANGES /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/doc/why3 + cp -pr README /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/doc/why3 + cp -pr doc/manual.pdf /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/doc/why3 + exit 0 Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.MkUJxi + umask 022 + cd /builddir/build/BUILD + cd why3-0.86 + LICENSEDIR=/builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/licenses/why3 + export LICENSEDIR + /usr/bin/mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/licenses/why3 + cp -pr LICENSE /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/licenses/why3 + exit 0 Provides: bundled(jquery) why3 = 0.86-1.fc22 why3(armv7hl-32) = 0.86-1.fc22 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 ld-linux-armhf.so.3 ld-linux-armhf.so.3(GLIBC_2.4) libatk-1.0.so.0 libc.so.6 libc.so.6(GLIBC_2.15) libc.so.6(GLIBC_2.4) libc.so.6(GLIBC_2.7) libcairo.so.2 libdl.so.2 libdl.so.2(GLIBC_2.4) libfontconfig.so.1 libfreetype.so.6 libgcc_s.so.1 libgcc_s.so.1(GCC_3.5) libgdk-x11-2.0.so.0 libgdk_pixbuf-2.0.so.0 libgio-2.0.so.0 libglib-2.0.so.0 libgobject-2.0.so.0 libgtk-x11-2.0.so.0 libgtksourceview-2.0.so.0 libm.so.6 libm.so.6(GLIBC_2.4) libpango-1.0.so.0 libpangocairo-1.0.so.0 libpangoft2-1.0.so.0 libz.so.1 rtld(GNU_HASH) Processing files: why3-examples-0.86-1.fc22.noarch Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.w4jLFm + umask 022 + cd /builddir/build/BUILD + cd why3-0.86 + DOCDIR=/builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/doc/why3-examples + export DOCDIR + /usr/bin/mkdir -p /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/doc/why3-examples + cp -pr examples /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm/usr/share/doc/why3-examples + exit 0 Provides: why3-examples = 0.86-1.fc22 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Processing files: why3-emacs-0.86-1.fc22.noarch Provides: why3-emacs = 0.86-1.fc22 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.86-1.fc22.noarch Provides: why3-emacs-el = 0.86-1.fc22 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Processing files: why3-xemacs-0.86-1.fc22.noarch Provides: why3-xemacs = 0.86-1.fc22 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.86-1.fc22.noarch Provides: why3-xemacs-el = 0.86-1.fc22 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Processing files: why3-all-0.86-1.fc22.armv7hl Processing files: why3-debuginfo-0.86-1.fc22.armv7hl Checking for unpackaged file(s): /usr/lib/rpm/check-files /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm Wrote: /builddir/build/RPMS/why3-0.86-1.fc22.armv7hl.rpm Wrote: /builddir/build/RPMS/why3-examples-0.86-1.fc22.noarch.rpm Wrote: /builddir/build/RPMS/why3-emacs-0.86-1.fc22.noarch.rpm Wrote: /builddir/build/RPMS/why3-emacs-el-0.86-1.fc22.noarch.rpm Wrote: /builddir/build/RPMS/why3-xemacs-0.86-1.fc22.noarch.rpm Wrote: /builddir/build/RPMS/why3-xemacs-el-0.86-1.fc22.noarch.rpm Wrote: /builddir/build/RPMS/why3-all-0.86-1.fc22.armv7hl.rpm Wrote: /builddir/build/RPMS/why3-debuginfo-0.86-1.fc22.armv7hl.rpm Executing(%clean): /bin/sh -e /var/tmp/rpm-tmp.YgZVKn + umask 022 + cd /builddir/build/BUILD + cd why3-0.86 + /usr/bin/rm -rf /builddir/build/BUILDROOT/why3-0.86-1.fc22.arm + exit 0 Child return code was: 0 LEAVE do -->