Mock Version: 1.2.13 Mock Version: 1.2.13 ENTER do(['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target x86_64 --nodeps /builddir/build/SPECS/why3.spec'], uid=1000gid=425user='mockbuild'logger=printOutput=Falseshell=FalsechrootPath='/var/lib/mock/f24-build-4485543-550506/root'env={'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'printf "\x1b]0;\x07"', 'TERM': 'vt100', 'LANG': 'en_US.UTF-8', 'SHELL': '/bin/bash'}timeout=172800) Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target x86_64 --nodeps /builddir/build/SPECS/why3.spec'] with env {'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'printf "\x1b]0;\x07"', 'TERM': 'vt100', 'LANG': 'en_US.UTF-8', 'SHELL': '/bin/bash'} and shell False Building target platforms: x86_64 Building for target x86_64 Wrote: /builddir/build/SRPMS/why3-0.86.2-2.fc24.src.rpm Child return code was: 0 LEAVE do --> ENTER do(['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --target x86_64 --nodeps /builddir/build/SPECS/why3.spec '], uid=1000gid=425user='mockbuild'logger=printOutput=Falseprivate_network=Trueshell=FalsechrootPath='/var/lib/mock/f24-build-4485543-550506/root'env={'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'printf "\x1b]0;\x07"', 'TERM': 'vt100', 'LANG': 'en_US.UTF-8', 'SHELL': '/bin/bash'}timeout=172800) Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --target x86_64 --nodeps /builddir/build/SPECS/why3.spec '] with env {'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'printf "\x1b]0;\x07"', 'TERM': 'vt100', 'LANG': 'en_US.UTF-8', 'SHELL': '/bin/bash'} and shell False Building target platforms: x86_64 Building for target x86_64 Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.VPssFC + umask 022 + cd /builddir/build/BUILD + cd /builddir/build/BUILD + rm -rf why3-0.86.2 + /usr/bin/gzip -dc /builddir/build/SOURCES/why3-0.86.2.tar.gz + /usr/bin/tar -xof - + STATUS=0 + '[' 0 -ne 0 ']' + cd why3-0.86.2 + /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w . + cd /builddir/build/BUILD + cd why3-0.86.2 + /usr/bin/xz -dc /builddir/build/SOURCES/why3-man.tar.xz + /usr/bin/tar -xof - + 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 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -m64 -mtune=generic|' -e 's/cp /cp -p /' -e 's|Aer[[:digit:]-]*|& -ccopt "-Wl,-z,relro -specs=/usr/lib/rpm/redhat/redhat-hardened-ld"|' -i Makefile.in + find -O3 examples -type f -perm /0111 + xargs chmod a-x + sed -i.orig '/iconset boomy/,/^$/d' share/images/icons.rc + fixtimestamp share/images/icons.rc + touch -r share/images/icons.rc.orig share/images/icons.rc + rm -f share/images/icons.rc.orig + sed -e s/boomy/fatcow/ -e 's/folder16\.png/folder.png/' -e 's/file16\.png/script.png/' -e 's/wizard16\.png/magic_wand_2.png/' -e 's/configure16\.png/multitool.png/' -i.orig src/why3session/why3session_html.ml + fixtimestamp src/why3session/why3session_html.ml + touch -r src/why3session/why3session_html.ml.orig src/why3session/why3session_html.ml + rm -f src/why3session/why3session_html.ml.orig + exit 0 Executing(%build): /bin/sh -e /var/tmp/rpm-tmp.RL3GVj + umask 022 + cd /builddir/build/BUILD + cd why3-0.86.2 + 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 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -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 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -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 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -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 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -m64 -mtune=generic -I/usr/lib64/gfortran/modules' + export FCFLAGS + LDFLAGS='-Wl,-z,relro -specs=/usr/lib/rpm/redhat/redhat-hardened-ld' + export LDFLAGS + '[' 1 = 1 ']' +++ dirname ./configure ++ find . -name config.guess -o -name config.sub + '[' 1 = 1 ']' + '[' x '!=' x-specs=/usr/lib/rpm/redhat/redhat-hardened-ld ']' ++ find . -name ltmain.sh + ./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.02.3 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 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/lib64/ocaml/zarith ocamlfind found camlzip in /usr/lib64/ocaml/zip ocamlfind found menhirLib in /usr/lib64/ocaml/menhirLib ocamlfind found lablgtk2 in /usr/lib64/ocaml/lablgtk2 ocamlfind found lablgtksourceview2 in /usr/lib64/ocaml/lablgtk2 checking for coqc... coqc checking Coq version... 8.4pl6 checking for coqdep... coqdep checking for /usr/lib64/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/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 .merlin config.status: creating src/jessie/Makefile config.status: executing chmod commands Summary ----------------------------------------- Verbose make : no OCaml compiler : yes configure: WARNING: unrecognized options: --disable-dependency-tracking Version : 4.02.3 Library path : /usr/lib64/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/lib64/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/lib64/why3 Data path : ${prefix}/share/why3 Ocaml Library : /usr/lib64/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 Ocamllex src/why3doc/doc_lexer.mll 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 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 Use Bytes.create instead. File "src/util/strings.ml", line 38, characters 4-15: Warning 3: deprecated: String.fill Use Bytes.fill instead. 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 File "src/util/weakhtbl.ml", line 172, characters 4-68: Warning 50: unattached documentation comment (ignored) 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 File "src/util/debug.ml", line 67, characters 2-69: Warning 50: unattached documentation comment (ignored) File "src/util/debug.ml", line 183, characters 2-69: Warning 50: unattached documentation comment (ignored) 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 Use Bytes.create instead. File "src/util/lexlib.mll", line 103, characters 46-56: Warning 3: deprecated: String.set Use Bytes.set instead. 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 Use Bytes.create instead. File "src/util/cmdline.ml", line 48, characters 10-20: Warning 3: deprecated: String.set Use Bytes.set instead. 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 File "src/util/rc.mli", line 35, characters 0-91: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 39, characters 0-67: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 41, characters 0-68: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 43, characters 0-60: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 45, characters 0-49: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 49, characters 0-43: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 57, characters 7-28: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 58, characters 13-38: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 59, characters 38-65: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 62, characters 14-32: Warning 50: ambiguous documentation comment Ocamlopt src/util/rc.ml File "src/util/rc.mll", line 67, characters 13-26: Warning 3: deprecated: String.create Use Bytes.create instead. 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 Use Bytes.set instead. 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 File "src/driver/call_provers.mli", line 46, characters 2-43: Warning 50: unattached documentation comment (ignored) 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 File "src/driver/whyconf.mli", line 234, characters 0-93: Warning 50: ambiguous documentation comment File "src/driver/whyconf.mli", line 241, characters 0-93: Warning 50: ambiguous documentation comment Ocamlopt src/driver/whyconf.ml File "src/driver/whyconf.ml", line 37, characters 30-60: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 316, characters 2-33: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 321, characters 2-39: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 324, characters 2-24: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 656, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 665, characters 2-28: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 670, characters 2-23: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 684, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 701, characters 2-23: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 711, characters 2-20: Warning 50: unattached documentation comment (ignored) Ocamlc src/driver/autodetection.mli Ocamlopt src/driver/autodetection.ml File "src/driver/autodetection.ml", line 151, characters 4-97: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 288, characters 4-142: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 294, characters 2-38: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 333, characters 2-109: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 367, characters 6-25: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 368, characters 32-63: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 377, characters 11-46: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 380, characters 4-35: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 428, characters 6-214: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 503, characters 4-40: Warning 50: unattached documentation comment (ignored) Ocamlopt src/driver/parse_cvc4_z3_model.ml Ocamlc src/mlw/ity.mli File "src/mlw/ity.mli", line 185, characters 23-57: Warning 50: ambiguous documentation comment File "src/mlw/ity.mli", line 311, characters 18-47: Warning 50: ambiguous documentation comment 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 File "src/transform/encoding_guards_full.ml", line 62, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/transform/encoding_guards_full.ml", line 71, characters 2-15: Warning 50: unattached documentation comment (ignored) File "src/transform/encoding_guards_full.ml", line 145, characters 2-28: Warning 50: unattached documentation comment (ignored) 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 File "src/printer/smtv2.ml", line 35, characters 4-25: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 36, characters 5-31: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 43, characters 6-30: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 49, characters 6-23: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 51, characters 6-48: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 65, characters 6-48: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 73, characters 6-20: Warning 50: unattached documentation comment (ignored) Ocamlc src/printer/coq.mli Ocamlopt src/printer/coq.ml File "src/printer/coq.ml", line 422, characters 4-30: Warning 50: unattached documentation comment (ignored) File "src/printer/coq.ml", line 434, characters 4-34: Warning 50: unattached documentation comment (ignored) File "src/printer/coq.ml", line 811, characters 2-154: Warning 50: unattached documentation comment (ignored) File "src/printer/coq.ml", line 481, characters 14-27: Warning 3: deprecated: String.create Use Bytes.create instead. Ocamlopt src/printer/pvs.ml Ocamlopt src/printer/isabelle.ml File "src/printer/isabelle.ml", line 329, characters 2-159: Warning 50: unattached documentation comment (ignored) 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 File "src/printer/cvc3.ml", line 30, characters 4-25: Warning 50: unattached documentation comment (ignored) File "src/printer/cvc3.ml", line 31, characters 5-20: Warning 50: unattached documentation comment (ignored) File "src/printer/cvc3.ml", line 34, characters 7-26: Warning 50: unattached documentation comment (ignored) File "src/printer/cvc3.ml", line 39, characters 7-26: Warning 50: unattached documentation comment (ignored) Ocamlopt src/printer/yices.ml File "src/printer/yices.ml", line 30, characters 4-25: Warning 50: unattached documentation comment (ignored) File "src/printer/yices.ml", line 31, characters 5-20: Warning 50: unattached documentation comment (ignored) File "src/printer/yices.ml", line 34, characters 7-26: Warning 50: unattached documentation comment (ignored) File "src/printer/yices.ml", line 39, characters 7-26: Warning 50: unattached documentation comment (ignored) Ocamlopt src/printer/mathematica.ml Ocamlc src/whyml/mlw_ty.mli File "src/whyml/mlw_ty.mli", line 147, characters 23-57: Warning 50: ambiguous documentation comment File "src/whyml/mlw_ty.mli", line 243, characters 25-54: Warning 50: ambiguous documentation comment File "src/whyml/mlw_ty.mli", line 244, characters 25-69: Warning 50: ambiguous documentation comment 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 File "src/session/session.mli", line 529, characters 2-72: Warning 50: ambiguous documentation comment Ocamlopt src/session/session.ml File "src/session/session.ml", line 92, characters 2-35: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 407, characters 6-191: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 667, characters 4-35: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1140, characters 4-31: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1309, characters 8-62: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1351, characters 12-34: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1429, characters 2-56: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1469, characters 6-48: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1497, characters 6-51: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1621, characters 2-73: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1683, characters 8-76: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1852, characters 4-30: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1925, characters 2-49: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1930, characters 22-66: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1934, characters 8-35: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1945, characters 12-74: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 2080, characters 2-55: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 2081, characters 2-91: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 2084, characters 2-49: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 2139, characters 2-48: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 2223, characters 2-164: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 2243, characters 6-62: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 2244, characters 6-56: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 2597, characters 2-28: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 2604, characters 51-72: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1517, characters 10-23: Warning 3: deprecated: String.create Use Bytes.create instead. 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 File "src/session/session_tools.ml", line 36, characters 4-76: Warning 50: unattached documentation comment (ignored) File "src/session/session_tools.ml", line 42, characters 8-61: Warning 50: unattached documentation comment (ignored) 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 File "src/session/session_scheduler.mli", line 265, characters 21-80: Warning 50: unattached documentation comment (ignored) Ocamlopt src/session/session_scheduler.ml File "src/session/session_scheduler.ml", line 91, characters 6-45: Warning 50: unattached documentation comment (ignored) File "src/session/session_scheduler.ml", line 141, characters 2-35: Warning 50: unattached documentation comment (ignored) File "src/session/session_scheduler.ml", line 156, characters 2-50: Warning 50: unattached documentation comment (ignored) File "src/session/session_scheduler.ml", line 170, characters 2-31: Warning 50: unattached documentation comment (ignored) File "src/session/session_scheduler.ml", line 926, characters 4-64: Warning 50: unattached documentation comment (ignored) Linking lib/why3/why3.cmx Ocamlopt plugins/parser/genequlin.ml File "plugins/parser/genequlin.ml", line 63, characters 2-53: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 76, characters 2-50: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 86, characters 2-36: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 94, characters 2-28: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 103, characters 2-26: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 107, characters 2-47: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 112, characters 8-106: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 123, characters 2-26: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 125, characters 2-39: Warning 50: unattached documentation comment (ignored) 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 File "plugins/transform/hypothesis_selection.ml", line 413, characters 4-32: Warning 50: unattached documentation comment (ignored) File "plugins/transform/hypothesis_selection.ml", line 419, characters 4-46: Warning 50: unattached documentation comment (ignored) File "plugins/transform/hypothesis_selection.ml", line 422, characters 6-91: Warning 50: unattached documentation comment (ignored) File "plugins/transform/hypothesis_selection.ml", line 445, characters 4-59: Warning 50: unattached documentation comment (ignored) Linking lib/plugins/hypothesis_selection.cmxs Linking lib/why3/why3.cmxa Ocamlopt src/tools/main.ml File "src/tools/main.ml", line 99, characters 2-17: Warning 50: unattached documentation comment (ignored) Linking bin/why3.opt Ocamlopt src/tools/why3config.ml File "src/tools/why3config.ml", line 117, characters 2-31: Warning 50: unattached documentation comment (ignored) File "src/tools/why3config.ml", line 122, characters 2-19: Warning 50: unattached documentation comment (ignored) File "src/tools/why3config.ml", line 135, characters 2-13: Warning 50: unattached documentation comment (ignored) 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 File "src/ide/gconfig.ml", line 24, characters 4-77: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 281, characters 0-18: Warning 50: ambiguous documentation comment File "src/ide/gconfig.ml", line 1015, characters 2-33: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 1017, characters 2-27: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 1021, characters 2-24: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 1025, characters 2-23: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 1039, characters 2-23: Warning 50: unattached documentation comment (ignored) Ocamlopt src/ide/gmain.ml File "src/ide/gmain.ml", line 819, characters 2-60: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 837, characters 34-64: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 841, characters 10-95: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1089, characters 6-67: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1125, characters 10-73: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1131, characters 4-106: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1134, characters 4-53: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 2049, characters 4-92: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 2052, characters 4-29: Warning 50: unattached documentation comment (ignored) Linking bin/why3ide.opt Ocamlc src/why3session/why3session_lib.mli Ocamlopt src/why3session/why3session_lib.ml File "src/why3session/why3session_lib.ml", line 64, characters 2-22: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 198, characters 2-16: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 202, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 208, characters 18-45: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 210, characters 2-17: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 212, characters 2-17: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 214, characters 2-22: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 217, characters 2-17: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 220, characters 2-15: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 259, characters 14-29: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 252, characters 10-23: Warning 3: deprecated: String.create Use Bytes.create instead. Ocamlopt src/why3session/why3session_copy.ml File "src/why3session/why3session_copy.ml", line 99, characters 14-57: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 133, characters 6-56: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 156, characters 20-74: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 157, characters 20-65: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 176, characters 2-61: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 182, characters 2-24: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3session/why3session_info.ml File "src/why3session/why3session_info.ml", line 407, characters 6-136: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3session/why3session_latex.ml File "src/why3session/why3session_latex.ml", line 302, characters 2-19: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_latex.ml", line 305, characters 2-44: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_latex.ml", line 311, characters 2-43: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_latex.ml", line 314, characters 2-28: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3session/why3session_html.ml File "src/why3session/why3session_html.ml", line 385, characters 6-28: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_html.ml", line 532, characters 6-24: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_html.ml", line 542, characters 6-28: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3session/why3session_rm.ml Ocamlopt src/why3session/why3session_output.ml File "src/why3session/why3session_output.ml", line 69, characters 12-74: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_output.ml", line 74, characters 12-73: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_output.ml", line 76, characters 12-35: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_output.ml", line 92, characters 2-61: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3session/why3session_run.ml File "src/why3session/why3session_run.ml", line 184, characters 24-52: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_run.ml", line 311, characters 31-43: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3session/why3session_csv.ml File "src/why3session/why3session_csv.ml", line 114, characters 23-56: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 198, characters 4-26: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 203, characters 32-47: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 205, characters 6-65: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 211, characters 6-47: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 254, characters 52-65: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 274, characters 2-22: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 277, characters 2-32: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 293, characters 2-32: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 310, characters 2-57: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 331, characters 2-33: Warning 50: unattached documentation comment (ignored) 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 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -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_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 [biblio] cannot find bibliography style abbrv compiling manual.tex... kpathsea running mktexfmt... running: bibtex manual.aux... compiling manual.tex... running: bibtex manual.aux... compiling manual.tex... running: bibtex manual.aux... 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) /builddir/build/BUILD/why3-0.86.2/share/why3session.dtd:48-49: Overfull \hbox (246.60182pt too wide) (page 95) /builddir/build/BUILD/why3-0.86.2/share/why3session.dtd: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 95) /builddir/build/BUILD/why3-0.86.2/share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 98) /builddir/build/BUILD/why3-0.86.2/share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 99) /builddir/build/BUILD/why3-0.86.2/share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 100) /builddir/build/BUILD/why3-0.86.2/share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 101) /builddir/build/BUILD/why3-0.86.2/share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 102) /builddir/build/BUILD/why3-0.86.2/share/provers-detection-data.conf:354-356: Overfull \hbox (89.024pt too wide) (page 103) /builddir/build/BUILD/why3-0.86.2/share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 103) /builddir/build/BUILD/why3-0.86.2/share/provers-detection-data.conf: Underfull \vbox (badness 10000) has occurred while \output is active [] (page 104) /builddir/build/BUILD/why3-0.86.2/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.NGxPYU + umask 022 + cd /builddir/build/BUILD + '[' /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64 '!=' / ']' + rm -rf /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64 ++ dirname /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64 + mkdir -p /builddir/build/BUILDROOT + mkdir /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64 + cd why3-0.86.2 + make install DESTDIR=/builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64 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.2-2.fc24.x86_64/usr/lib64/why3 rm -rf /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3 rm -rf /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/ocaml/why3 rm -f /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/emacs/site-lisp/why3.el rm -f /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/emacs/site-lisp/why3.elc rm -f /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3config /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3execute /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3extract /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3prove /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3realize /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3replay /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3wc /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/bin/why3 rm -f /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/bin/why3bench /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/bin/why3replayer rm -f /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/bin/why3ide rm -f /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/bin/why3session rm -f /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/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.2/share/emacs/why3.elc mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/bin mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3 mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3 mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/images mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/images/boomy mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/images/fatcow mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/vim mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/lang mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/theories mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/modules/mach mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/drivers mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/emacs/site-lisp/ cp -p -f theories/*.why /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/theories cp -p -f modules/*.mlw /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/modules cp -p -f modules/mach/*.mlw /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/modules/mach cp -p -f drivers/*.drv drivers/*.gen /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/drivers cp -p -f LICENSE /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/ cp -p -f share/provers-detection-data.conf /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/ cp -p -f share/images/icons.rc /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/images cp -p -f share/images/*.png /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/images cp -p -f share/images/boomy/* /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/images/boomy cp -p -f share/images/fatcow/* /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/images/fatcow cp -p -f share/why3session.dtd /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3 cp -p -f share/Makefile.config /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3 cp -p -rf share/javascript /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/javascript cp -p -f share/vim/why3.vim /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/vim/why3.vim cp -p -f share/lang/why3.lang /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/lang/why3.lang cp -p -f share/emacs/why3.el /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/emacs/site-lisp/why3.el cp -p -f share/emacs/why3.elc /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/emacs/site-lisp/why3.elc mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.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.86.2-2.fc24.x86_64/usr/lib64/why3/plugins cp -p -f bin/why3.opt /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/bin/why3 cp -p -f bin/why3config.opt /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3config cp -p -f bin/why3execute.opt /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3execute cp -p -f bin/why3extract.opt /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3extract cp -p -f bin/why3prove.opt /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3prove cp -p -f bin/why3realize.opt /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3realize cp -p -f bin/why3replay.opt /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3replay cp -p -f bin/why3wc.opt /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3wc cp -p -f bin/why3ide.opt /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3ide cp -p -f bin/why3session.opt /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3session mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/coq-tactic cp -p -f lib/coq-tactic/* /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/coq-tactic mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/coq cp -p lib/coq/BuiltIn.vo lib/coq/HighOrd.vo /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/coq/ mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.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.86.2-2.fc24.x86_64/usr/lib64/why3/coq/int/ mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/coq/bool cp -p lib/coq/bool/Bool.vo /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/coq/bool/ mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.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/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.2-2.fc24.x86_64/usr/lib64/why3/coq/real/ mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.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.86.2-2.fc24.x86_64/usr/lib64/why3/coq/number/ mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/coq/set cp -p lib/coq/set/Set.vo /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/coq/set/ mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.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.86.2-2.fc24.x86_64/usr/lib64/why3/coq/map/ mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.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 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.2-2.fc24.x86_64/usr/lib64/why3/coq/list/ mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/coq/option cp -p lib/coq/option/Option.vo /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/coq/option/ mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/coq/seq cp -p lib/coq/seq/Seq.vo /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/coq/seq/ mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.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.86.2-2.fc24.x86_64/usr/lib64/why3/coq/floating_point/ cp -p drivers/coq-realizations.aux /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/drivers/ cp -p drivers/pvs-realizations.aux /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/drivers/ cp -p drivers/isabelle-realizations.aux /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/drivers/ cp -p -f lib/why3-cpulimit /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/why3-cpulimit cp -p -f lib/why3-call-pvs /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/why3-call-pvs cp -p -f bin/why3doc.opt /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/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.2-2.fc24.x86_64/usr/share/man/man1 + cd man + for f in '*.1' + sed s/@version@/0.86.2/ why3-cpulimit.1 + touch -r why3-cpulimit.1 /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/man/man1/why3-cpulimit.1 + for f in '*.1' + sed s/@version@/0.86.2/ why3.1 + touch -r why3.1 /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/man/man1/why3.1 + for f in '*.1' + sed s/@version@/0.86.2/ why3bench.1 + touch -r why3bench.1 /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/man/man1/why3bench.1 + for f in '*.1' + sed s/@version@/0.86.2/ why3config.1 + touch -r why3config.1 /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/man/man1/why3config.1 + for f in '*.1' + sed s/@version@/0.86.2/ why3doc.1 + touch -r why3doc.1 /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/man/man1/why3doc.1 + for f in '*.1' + sed s/@version@/0.86.2/ why3ide.1 + touch -r why3ide.1 /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/man/man1/why3ide.1 + for f in '*.1' + sed s/@version@/0.86.2/ why3ml.1 + touch -r why3ml.1 /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/man/man1/why3ml.1 + for f in '*.1' + sed s/@version@/0.86.2/ why3realize.1 + touch -r why3realize.1 /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/man/man1/why3realize.1 + for f in '*.1' + sed s/@version@/0.86.2/ why3replayer.1 + touch -r why3replayer.1 /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/man/man1/why3replayer.1 + cd .. + mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/bash-completion/completions + cp -p share/bash/why3 /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/bash-completion/completions + mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/zsh/site-functions + cp -p share/zsh/_why3 /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/zsh/site-functions + mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/texmf/tex/latex/why3 + cp -p share/latex/why3lang.sty /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/texmf/tex/latex/why3 + mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/gtksourceview-2.0 + mv /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/lang /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/gtksourceview-2.0/language-specs + mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/vim/vimfiles + mv /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/vim /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/vim/vimfiles/syntax + mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/xemacs/site-packages/lisp + cp -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/emacs/site-lisp/why3.el /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/xemacs/site-packages/lisp ~/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/xemacs/site-packages/lisp ~/build/BUILD/why3-0.86.2 + pushd /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/xemacs/site-packages/lisp + /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.2-2.fc24.x86_64/usr/share/xemacs/site-packages/lisp/why3.el... While compiling why3-mode in file /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/xemacs/site-packages/lisp/why3.el: ** assignment to free variable font-lock-defaults Wrote /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/xemacs/site-packages/lisp/why3.elc Done + cd /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.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.86.2-2.fc24.x86_64/usr/share/emacs/site-lisp/why3.elc ~/build/BUILD/why3-0.86.2 + popd + rm -fr /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/doc + rm -fr /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/why3/images/boomy + chmod 0755 /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/bin/why3 /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3config /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3doc /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3execute /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3extract /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3ide /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3prove /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3realize /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3replay /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3session /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3wc /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/coq-tactic/why3tac.cmxs /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/plugins/dimacs.cmxs /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/plugins/genequlin.cmxs /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/plugins/hypothesis_selection.cmxs /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/plugins/tptp.cmxs /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.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.86.2 extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/plugins/tptp.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/plugins/hypothesis_selection.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/plugins/dimacs.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/plugins/genequlin.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/coq-tactic/why3tac.cmxs extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/why3-cpulimit extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3session extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3doc extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3execute extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3prove extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3extract extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3ide extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3wc extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3replay extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3config extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/lib64/why3/commands/why3realize extracting debug info from /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/bin/why3 /usr/lib/rpm/sepdebugcrcfix: Updated 14 CRC32s, 3 CRC32s did match. cpio: menhir-20151112/src/_stage2: Cannot stat: No such file or directory cpio: menhir-20151112/src/_stage2/Convert.ml: Cannot stat: No such file or directory cpio: menhir-20151112/src/_stage2/Engine.ml: Cannot stat: No such file or directory cpio: menhir-20151112/src/_stage2/General.ml: Cannot stat: No such file or directory cpio: menhir-20151112/src/_stage2/InfiniteArray.ml: Cannot stat: No such file or directory cpio: menhir-20151112/src/_stage2/InspectionTableInterpreter.ml: Cannot stat: No such file or directory cpio: menhir-20151112/src/_stage2/LinearizedArray.ml: Cannot stat: No such file or directory cpio: menhir-20151112/src/_stage2/PackedIntArray.ml: Cannot stat: No such file or directory cpio: menhir-20151112/src/_stage2/Printers.ml: Cannot stat: No such file or directory cpio: menhir-20151112/src/_stage2/RowDisplacement.ml: Cannot stat: No such file or directory cpio: menhir-20151112/src/_stage2/TableInterpreter.ml: Cannot stat: No such file or directory cpio: ocaml-4.02.3/stdlib: Cannot stat: No such file or directory cpio: ocaml-4.02.3/stdlib/std_exit.ml: Cannot stat: No such file or directory cpio: why3-0.86.2/big_int.ml: Cannot stat: No such file or directory cpio: why3-0.86.2/buffer.ml: Cannot stat: No such file or directory cpio: why3-0.86.2/bytes.ml: Cannot stat: No such file or directory cpio: why3-0.86.2/format.ml: Cannot stat: No such file or directory cpio: why3-0.86.2/gdkPixbuf.ml: Cannot stat: No such file or directory cpio: why3-0.86.2/gtkMain.ml: Cannot stat: No such file or directory cpio: why3-0.86.2/hashtbl.ml: Cannot stat: No such file or directory cpio: why3-0.86.2/lexing.ml: Cannot stat: No such file or directory cpio: why3-0.86.2/list.ml: Cannot stat: No such file or directory cpio: why3-0.86.2/pervasives.ml: Cannot stat: No such file or directory cpio: why3-0.86.2/random.ml: Cannot stat: No such file or directory cpio: why3-0.86.2/stack.ml: Cannot stat: No such file or directory cpio: why3-0.86.2/str.ml: Cannot stat: No such file or directory cpio: why3-0.86.2/string.ml: Cannot stat: No such file or directory 7952 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.2-2.fc24.x86_64 Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.yE56Me + umask 022 + cd /builddir/build/BUILD + cd why3-0.86.2 + DOCDIR=/builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/doc/why3 + export DOCDIR + /usr/bin/mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/doc/why3 + cp -pr AUTHORS /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/doc/why3 + cp -pr CHANGES /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/doc/why3 + cp -pr README /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/doc/why3 + cp -pr doc/manual.pdf /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/doc/why3 + exit 0 Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.5BfrDy + umask 022 + cd /builddir/build/BUILD + cd why3-0.86.2 + LICENSEDIR=/builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/licenses/why3 + export LICENSEDIR + /usr/bin/mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/licenses/why3 + cp -pr LICENSE /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/licenses/why3 + exit 0 Provides: bundled(jquery) why3 = 0.86.2-2.fc24 why3(x86-64) = 0.86.2-2.fc24 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.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.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) libz.so.1()(64bit) rtld(GNU_HASH) Processing files: why3-examples-0.86.2-2.fc24.noarch Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.8PSLAW + umask 022 + cd /builddir/build/BUILD + cd why3-0.86.2 + DOCDIR=/builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/doc/why3-examples + export DOCDIR + /usr/bin/mkdir -p /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/doc/why3-examples + cp -pr examples /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64/usr/share/doc/why3-examples + exit 0 Provides: why3-examples = 0.86.2-2.fc24 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.2-2.fc24.noarch Provides: why3-emacs = 0.86.2-2.fc24 why3-emacs-el = 0.86.2-2.fc24 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Obsoletes: why3-emacs-el < 0.86.2-2 Processing files: why3-xemacs-0.86.2-2.fc24.noarch Provides: why3-xemacs = 0.86.2-2.fc24 why3-xemacs-el = 0.86.2-2.fc24 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Obsoletes: why3-xemacs-el < 0.86.2-2 Processing files: why3-all-0.86.2-2.fc24.x86_64 Processing files: why3-debuginfo-0.86.2-2.fc24.x86_64 Provides: why3-debuginfo = 0.86.2-2.fc24 why3-debuginfo(x86-64) = 0.86.2-2.fc24 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Checking for unpackaged file(s): /usr/lib/rpm/check-files /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64 Wrote: /builddir/build/RPMS/why3-0.86.2-2.fc24.x86_64.rpm Wrote: /builddir/build/RPMS/why3-examples-0.86.2-2.fc24.noarch.rpm Wrote: /builddir/build/RPMS/why3-emacs-0.86.2-2.fc24.noarch.rpm Wrote: /builddir/build/RPMS/why3-xemacs-0.86.2-2.fc24.noarch.rpm Wrote: /builddir/build/RPMS/why3-all-0.86.2-2.fc24.x86_64.rpm Wrote: /builddir/build/RPMS/why3-debuginfo-0.86.2-2.fc24.x86_64.rpm Executing(%clean): /bin/sh -e /var/tmp/rpm-tmp.LwS8jg + umask 022 + cd /builddir/build/BUILD + cd why3-0.86.2 + /usr/bin/rm -rf /builddir/build/BUILDROOT/why3-0.86.2-2.fc24.x86_64 + exit 0 Child return code was: 0 LEAVE do -->