https://git.altlinux.org/tasks/371761/logs/events.5.1.log
https://packages.altlinux.org/tasks/371761

subtask  name  aarch64    i586  ppc64le  x86_64
   #300  coq     17:25  failed   failed    9:16

2025-Jan-27 09:18:54 :: test-only task #371761 for sisyphus resumed by 
respublica:
#40 build 3.1.5-alt2 from /people/respublica/packages/ocaml-lablgtk3.git 
fetched at 2025-Jan-26 14:48:18
#100 removed
#200 removed
#300 build 8.20.0-alt1 from /people/respublica/packages/coq.git fetched at 
2025-Jan-27 09:18:47
2025-Jan-27 09:18:54 :: created build repo
2025-Jan-27 09:18:55 :: [x86_64] #40 ocaml-lablgtk3.git 3.1.5-alt2: build start
2025-Jan-27 09:18:55 :: [i586] #40 ocaml-lablgtk3.git 3.1.5-alt2: build start
2025-Jan-27 09:18:55 :: [aarch64] #40 ocaml-lablgtk3.git 3.1.5-alt2: build start
2025-Jan-27 09:18:55 :: [ppc64le] #40 ocaml-lablgtk3.git 3.1.5-alt2: build start
2025-Jan-27 09:19:14 :: [i586] #40 ocaml-lablgtk3.git 3.1.5-alt2: build OK 
(cached)
2025-Jan-27 09:19:14 :: [i586] #300 coq.git 8.20.0-alt1: build start
2025-Jan-27 09:19:16 :: [x86_64] #40 ocaml-lablgtk3.git 3.1.5-alt2: build OK 
(cached)
2025-Jan-27 09:19:16 :: [x86_64] #300 coq.git 8.20.0-alt1: build start
2025-Jan-27 09:19:33 :: [aarch64] #40 ocaml-lablgtk3.git 3.1.5-alt2: build OK 
(cached)
2025-Jan-27 09:19:33 :: [aarch64] #300 coq.git 8.20.0-alt1: build start
2025-Jan-27 09:19:40 :: [ppc64le] #40 ocaml-lablgtk3.git 3.1.5-alt2: build OK 
(cached)
2025-Jan-27 09:19:41 :: [ppc64le] #300 coq.git 8.20.0-alt1: build start
[i586] Running[2264]: (cd _build/default && /usr/bin/ocamlc -w -40 -g -o 
topbin/coqtop_byte_bin.bc -linkall /usr/lib/ocaml/compiler-libs/ocamlcommon.cma 
/usr/lib/ocaml/compiler-libs/ocamlbytecomp.cma 
/usr/lib/ocaml/compiler-libs/ocamltoplevel.cma config/byte_config.cma 
config/config.cma boot/boot.cma /usr/lib/ocaml/str/str.cma 
/usr/lib/ocaml/unix/unix.cma /usr/lib/ocaml/threads/threads.cma clib/clib.cma 
perf/coqperf.cma -I perf lib/lib.cma gramlib/gramlib.cma 
/usr/lib/ocaml/zarith/zarith.cma kernel/byterun/coqrun.cma -I kernel/byterun 
/usr/lib/ocaml/dynlink/dynlink.cma kernel/kernel.cma library/library.cma 
engine/engine.cma pretyping/pretyping.cma interp/interp.cma parsing/parsing.cma 
proofs/proofs.cma printing/printing.cma tactics/tactics.cma 
/usr/lib/ocaml/findlib/findlib.cma /usr/lib/ocaml/findlib/findlib_dynload.cma 
topbin/.coqtop_byte_bin.eobjs/byte/findlib_initl.cmo vernac/vernac.cma 
sysinit/sysinit.cma tools/coqworkmgr/coqworkmgrlib.cma stm/stm.cma 
toplevel/toplevel.cma plugin
 s/ltac/ltac_plugin.cma dev/dev.cma /usr/lib/ocaml/findlib/findlib_top.cma 
topbin/.coqtop_byte_bin.eobjs/byte/dune__exe__Coqtop_byte_bin.cmo)
[i586] Running[2265]: (cd _build/default && /usr/bin/ocamlc -w -40 -g -a -o 
plugins/firstorder/firstorder_plugin.cma 
plugins/firstorder/.firstorder_plugin.objs/byte/firstorder_plugin.cmo 
plugins/firstorder/.firstorder_plugin.objs/byte/firstorder_plugin__Formula.cmo 
plugins/firstorder/.firstorder_plugin.objs/byte/firstorder_plugin__Unify.cmo 
plugins/firstorder/.firstorder_plugin.objs/byte/firstorder_plugin__Sequent.cmo 
plugins/firstorder/.firstorder_plugin.objs/byte/firstorder_plugin__Rules.cmo 
plugins/firstorder/.firstorder_plugin.objs/byte/firstorder_plugin__Instances.cmo
 plugins/firstorder/.firstorder_plugin.objs/byte/firstorder_plugin__Ground.cmo 
plugins/firstorder/.firstorder_plugin.objs/byte/firstorder_plugin__G_ground.cmo)
[i586] Running[2266]: (cd _build/default && /usr/bin/ocamlc -w -40 -g -a -o 
plugins/ring/ring_plugin.cma 
plugins/ring/.ring_plugin.objs/byte/ring_plugin.cmo 
plugins/ring/.ring_plugin.objs/byte/ring_plugin__Ring_ast.cmo 
plugins/ring/.ring_plugin.objs/byte/ring_plugin__Ring.cmo 
plugins/ring/.ring_plugin.objs/byte/ring_plugin__G_ring.cmo)
[i586] Running[2267]: (cd _build/default && /usr/bin/ocamlc -w -40 -g -a -o 
plugins/funind/funind_plugin.cma 
plugins/funind/.funind_plugin.objs/byte/funind_plugin.cmo 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Indfun_common.cmo 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Recdef.cmo 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Invfun.cmo 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Indfun.cmo 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Glob_termops.cmo 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Glob_term_to_relation.cmo
 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Functional_principles_proofs.cmo
 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Functional_principles_types.cmo
 plugins/funind/.funind_plugin.objs/byte/funind_plugin__Gen_principle.cmo 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__G_indfun.cmo)
[i586] Running[2268]: (cd _build/default && /usr/bin/ocamlc -w -40 -g -a -o 
plugins/ssrmatching/ssrmatching_plugin.cma 
plugins/ssrmatching/.ssrmatching_plugin.objs/byte/ssrmatching_plugin.cmo 
plugins/ssrmatching/.ssrmatching_plugin.objs/byte/ssrmatching_plugin__Ssrmatching.cmo
 
plugins/ssrmatching/.ssrmatching_plugin.objs/byte/ssrmatching_plugin__G_ssrmatching.cmo)
[i586] Running[2269]: (cd _build/default && /usr/bin/ocamlc -w -40 -open 
Micromega_core_plugin -g -a -o plugins/micromega/micromega_plugin.cma 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin.cmo 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Vect.cmo 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Polynomial.cmo 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Simplex.cmo 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Persistent_cache.cmo
 plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Linsolve.cmo 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Itv.cmo 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Certificate.cmo 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Coq_micromega.cmo
 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__G_micromega.cmo)
[i586] Running[2270]: (cd _build/default && /usr/bin/ocamlc -w -40 -open 
Gramlib -g -a -o plugins/ssr/ssreflect_plugin.cma 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrprinters.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrcommon.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrview.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrvernac.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrtacticals.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrbwd.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrelim.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrequality.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssripats.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrfwd.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrparser.cmo 
plugins/ssr/.ssreflect_plu
 gin.objs/byte/ssreflect_plugin__Ssrtacs.cmo)
[i586] Promoting "_build/default/coq-core.install" to "coq-core.install"
[i586] Running[2271]: (cd _build/default && ../install/default/bin/coqc -noinit 
-boot -R theories Coq -I plugins/firstorder -I plugins/funind -I plugins/ltac2 
-I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I plugins/rtauto -I 
plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I plugins/btauto -I 
plugins/micromega -I plugins/cc -I plugins/derive -I plugins/extraction -I 
plugins/ltac -w +default -q -w -deprecated-native-compiler-option 
-native-compiler off -time-file theories/Init/Notations.timing 
theories/Init/Notations.v)
[i586] Promoting "_build/default/coqide-server.install" to 
"coqide-server.install"
2025-Jan-27 09:20:32 :: [i586] coq.git 8.20.0-alt1: remote: build failed
2025-Jan-27 09:20:32 :: [i586] #300 coq.git 8.20.0-alt1: build FAILED
2025-Jan-27 09:20:32 :: [i586] requesting cancellation of task processing
[ppc64le] Running[2264]: (cd _build/default && /usr/bin/ocamlc -w -40 -g -a -o 
plugins/ltac/ltac_plugin.cma 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Tacarg.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Tacsubst.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Tacenv.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Pptactic.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Leminv.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Taccoerce.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Tacintern.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Tactic_debug.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Tactic_matching.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Tacinterp.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Tactic_option.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Pltac.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Tacentries.cmo 
plugins/ltac/.ltac_p
 lugin.objs/byte/ltac_plugin__Profile_ltac_tactics.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Internals.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__G_ltac.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Extraargs.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__G_tactic.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__ComRewrite.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__G_rewrite.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__G_obligations.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__G_eqdecide.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__G_class.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__G_auto.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Extratactics.cmo 
plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__Coretactics.cmo)
[ppc64le] Running[2265]: (cd _build/default && /usr/bin/ocamlc -w -40 -g -a -o 
plugins/ring/ring_plugin.cma 
plugins/ring/.ring_plugin.objs/byte/ring_plugin.cmo 
plugins/ring/.ring_plugin.objs/byte/ring_plugin__Ring_ast.cmo 
plugins/ring/.ring_plugin.objs/byte/ring_plugin__Ring.cmo 
plugins/ring/.ring_plugin.objs/byte/ring_plugin__G_ring.cmo)
[ppc64le] Running[2266]: (cd _build/default && /usr/bin/ocamlc -w -40 -g -o 
topbin/coqtop_byte_bin.bc -linkall 
/usr/lib64/ocaml/compiler-libs/ocamlcommon.cma 
/usr/lib64/ocaml/compiler-libs/ocamlbytecomp.cma 
/usr/lib64/ocaml/compiler-libs/ocamltoplevel.cma config/byte_config.cma 
config/config.cma boot/boot.cma /usr/lib64/ocaml/str/str.cma 
/usr/lib64/ocaml/unix/unix.cma /usr/lib64/ocaml/threads/threads.cma 
clib/clib.cma perf/coqperf.cma -I perf lib/lib.cma gramlib/gramlib.cma 
/usr/lib64/ocaml/zarith/zarith.cma kernel/byterun/coqrun.cma -I kernel/byterun 
/usr/lib64/ocaml/dynlink/dynlink.cma kernel/kernel.cma library/library.cma 
engine/engine.cma pretyping/pretyping.cma interp/interp.cma parsing/parsing.cma 
proofs/proofs.cma printing/printing.cma tactics/tactics.cma 
/usr/lib64/ocaml/findlib/findlib.cma 
/usr/lib64/ocaml/findlib/findlib_dynload.cma 
topbin/.coqtop_byte_bin.eobjs/byte/findlib_initl.cmo vernac/vernac.cma 
sysinit/sysinit.cma tools/coqworkmgr/coqworkmgrlib.cma stm/stm.cma tople
 vel/toplevel.cma plugins/ltac/ltac_plugin.cma dev/dev.cma 
/usr/lib64/ocaml/findlib/findlib_top.cma 
topbin/.coqtop_byte_bin.eobjs/byte/dune__exe__Coqtop_byte_bin.cmo)
[ppc64le] Running[2267]: (cd _build/default && /usr/bin/ocamlc -w -40 -g -a -o 
plugins/funind/funind_plugin.cma 
plugins/funind/.funind_plugin.objs/byte/funind_plugin.cmo 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Indfun_common.cmo 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Recdef.cmo 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Invfun.cmo 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Indfun.cmo 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Glob_termops.cmo 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Glob_term_to_relation.cmo
 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Functional_principles_proofs.cmo
 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__Functional_principles_types.cmo
 plugins/funind/.funind_plugin.objs/byte/funind_plugin__Gen_principle.cmo 
plugins/funind/.funind_plugin.objs/byte/funind_plugin__G_indfun.cmo)
[ppc64le] Running[2268]: (cd _build/default && /usr/bin/ocamlc -w -40 -g -a -o 
plugins/ssrmatching/ssrmatching_plugin.cma 
plugins/ssrmatching/.ssrmatching_plugin.objs/byte/ssrmatching_plugin.cmo 
plugins/ssrmatching/.ssrmatching_plugin.objs/byte/ssrmatching_plugin__Ssrmatching.cmo
 
plugins/ssrmatching/.ssrmatching_plugin.objs/byte/ssrmatching_plugin__G_ssrmatching.cmo)
[ppc64le] Running[2269]: (cd _build/default && /usr/bin/ocamlc -w -40 -open 
Micromega_core_plugin -g -a -o plugins/micromega/micromega_plugin.cma 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin.cmo 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Vect.cmo 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Polynomial.cmo 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Simplex.cmo 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Persistent_cache.cmo
 plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Linsolve.cmo 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Itv.cmo 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Certificate.cmo 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Coq_micromega.cmo
 
plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__G_micromega.cmo)
[ppc64le] Running[2270]: (cd _build/default && /usr/bin/ocamlc -w -40 -open 
Gramlib -g -a -o plugins/ssr/ssreflect_plugin.cma 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrprinters.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrcommon.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrview.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrvernac.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrtacticals.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrbwd.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrelim.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrequality.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssripats.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrfwd.cmo 
plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrparser.cmo 
plugins/ssr/.ssreflect_
 plugin.objs/byte/ssreflect_plugin__Ssrtacs.cmo)
[ppc64le] Running[2271]: (cd _build/default && ../install/default/bin/coqc 
-noinit -boot -R theories Coq -I plugins/firstorder -I plugins/funind -I 
plugins/ltac2 -I plugins/ltac2_ltac1 -I plugins/nsatz -I plugins/ring -I 
plugins/rtauto -I plugins/ssr -I plugins/ssrmatching -I plugins/syntax -I 
plugins/btauto -I plugins/micromega -I plugins/cc -I plugins/derive -I 
plugins/extraction -I plugins/ltac -w +default -q -w 
-deprecated-native-compiler-option -native-compiler off -time-file 
theories/Init/Notations.timing theories/Init/Notations.v)
[ppc64le] Promoting "_build/default/coq-core.install" to "coq-core.install"
[ppc64le] Promoting "_build/default/coqide-server.install" to 
"coqide-server.install"
2025-Jan-27 09:22:43 :: [ppc64le] coq.git 8.20.0-alt1: remote: build failed
2025-Jan-27 09:22:43 :: [ppc64le] #300 coq.git 8.20.0-alt1: build FAILED
2025-Jan-27 09:28:32 :: [x86_64] #300 coq.git 8.20.0-alt1: build OK
2025-Jan-27 09:36:58 :: [aarch64] #300 coq.git 8.20.0-alt1: build OK
2025-Jan-27 09:20:32 :: [i586] build FAILED
2025-Jan-27 09:22:43 :: [ppc64le] build FAILED
2025-Jan-27 09:36:58 :: task #371761 for sisyphus FAILED
_______________________________________________
Sisyphus-incominger mailing list
Sisyphus-incominger@lists.altlinux.org
https://lists.altlinux.org/mailman/listinfo/sisyphus-incominger

Reply via email to