Build:
- 0
2026-09-03 22:56.35: New job: build coqide.8.12.1 (55a0d174b2b5) 2026-09-03 22:56.35: Waiting for resource in pool day11-builds 2026-09-03 23:46.10: Got resource from pool day11-builds 2026-09-03 23:46.10: [profile full] build coqide.8.12.1 2026-09-03 23:46.10: build coqide.8.12.1 (55a0d174b2b5) === DEPENDENCIES (22 transitive) === base-bigarray.base 31ac6860ef52 base-threads.base 3d2f2cbc6db2 base-unix.base 3a38ddca6b5e cairo2.0.6.5 ee009ac99668 camlp-streams.5.0.1 50dfb9c1257b conf-adwaita-icon-theme.2 2df4351f623b conf-cairo.1 9e32499642c2 conf-findutils.1 ae9b487ad27c conf-gtk3.18 29bc2ce5fb33 conf-gtksourceview3.0+2 89f7273ce96d conf-pkg-config.5 74f50f3cfe72 coq.8.12.1 7533e29cff2c csexp.1.5.2 67f9dc836ab0 dune.3.22.2 7240d0a5a88c dune-configurator.3.22.2 7fb534e4fa20 lablgtk3.3.1.5 ae330eec2883 lablgtk3-sourceview3.3.1.5 960b96379960 num.1.6 2234dcccc6b4 ocaml.4.11.2 9044b53bfe17 ocaml-base-compiler.4.11.2 d1ed934bdaf0 ocaml-config.1 51b78fd13520 ocamlfind.1.9.8 67e30f343c55 === STDOUT === Processing: [default: loading data] [coqide.8.12.1: extract] [coqide.8.12.1/coqide.install: dl] -> retrieved coqide.8.12.1 (cached) [coqide: ./configure] + /home/opam/.opam/default/.opam-switch/build/coqide.8.12.1/./configure "-configdir" "/home/opam/.opam/default/lib/coq/config" "-prefix" "/home/opam/.opam/default" "-mandir" "/home/opam/.opam/default/man" "-docdir" "/home/opam/.opam/default/doc" "-libdir" "/home/opam/.opam/default/lib/coq" "-datadir" "/home/opam/.opam/default/share/coq" (CWD=/home/opam/.opam/default/.opam-switch/build/coqide.8.12.1) - You have OCaml 4.11.2. Good! - You have OCamlfind 1.9.8. Good! - You have native-code compilation. Good! - You have the Num library installed. Good! - LablGtk3 and LablGtkSourceView3 found (3.1.5), with native threads: - => native CoqIde will be built. - - Architecture : Linux - Sys.os_type : Unix - Coq VM bytecode link flags : -dllib -lcoqrun -dllpath /home/opam/.opam/default/lib/coq/kernel/byterun - Other bytecode link flags : - OCaml version : 4.11.2 - OCaml binaries in : /home/opam/.opam/default/bin/ - OCaml library in : /home/opam/.opam/default/lib/ocaml - OCaml flambda flags : - Native dynamic link support : true - Lablgtk3 library in : /home/opam/.opam/default/lib/lablgtk3-sourceview3 - CoqIde : opt - Documentation : None - Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s & - Coq web site : http://coq.inria.fr/ - Bytecode VM enabled : true - Native Compiler enabled : true - - Paths for true installation: - - the Coq binaries will be copied in /home/opam/.opam/default/bin - - the Coq library will be copied in /home/opam/.opam/default/lib/coq - - the Coqide configuration files will be copied in /home/opam/.opam/default/lib/coq/config - - the Coqide data files will be copied in /home/opam/.opam/default/share/coq - - the Coq man pages will be copied in /home/opam/.opam/default/man - - the Coq documentation will be copied in /home/opam/.opam/default/doc - - the Coqdoc LaTeX files will be copied in /home/opam/.opam/default/share/texmf/tex/latex/misc - - If anything is wrong above, please restart './configure'. - - *Warning* To compile the system for a new architecture - don't forget to do a 'make clean' before './configure'. [coqide: make coqide-files] + /usr/bin/make "COQ_USE_DUNE=" "-j39" "coqide-files" (CWD=/home/opam/.opam/default/.opam-switch/build/coqide.8.12.1) - rm -f - cp -a "kernel/.merlin.in" "kernel/.merlin" - cp -a "plugins/.merlin.in" "plugins/.merlin" - cp -a "ide/.merlin.in" "ide/.merlin" - cp -a ".merlin.in" ".merlin" - cp -a "test-suite/unit-tests/.merlin.in" "test-suite/unit-tests/.merlin" - cp -a "META.coq.in" "META.coq" - mkdir bin - /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build coqide-files - make[1]: Entering directory '/home/opam/.opam/default/.opam-switch/build/coqide.8.12.1' - OCAMLDEP checker/MLFILES checker/MLIFILES - OCAMLLEX tools/ocamllibdep.mll - OCAMLC coqpp/coqpp_ast.mli - make[1]: Circular coqpp/coqpp_parse.cmi <- coqpp/coqpp_parse.cmo dependency dropped. - OCAMLYACC coqpp/coqpp_parse.mly - OCAMLLEX coqpp/coqpp_lex.mll - 14 states, 417 transitions, table size 1752 bytes - mkdir -p gramlib/.pack - OCAMLLEX tools/coqdoc/cpretty.mll - OCAMLLEX tools/coqwc.mll - OCAMLLEX tools/coqdep_lexer.mll - OCAMLLEX ide/utf8_convert.mll - OCAMLLEX ide/protocol/xml_lexer.mll - OCAMLLEX ide/config_lexer.mll - 244 states, 858 transitions, table size 4896 bytes - 15 states, 827 transitions, table size 3398 bytes - rm -f ide/coqide_os_specific.ml && cp ide/coqide_X11.ml.in ide/coqide_os_specific.ml && chmod a-w ide/coqide_os_specific.ml - OCAMLLEX ide/coq_lex.mll - OCAMLC kernel/genOpcodeFiles.ml - rm -f kernel/uint63.ml && cp kernel/uint63_63.ml kernel/uint63.ml && chmod a-w kernel/uint63.ml - printf '# 1 "%s"\n' gramlib/ploc.ml > gramlib/.pack/gramlib__Ploc.ml - printf '# 1 "%s"\n' gramlib/plexing.ml > gramlib/.pack/gramlib__Plexing.ml - printf '# 1 "%s"\n' gramlib/gramext.ml > gramlib/.pack/gramlib__Gramext.ml - printf '# 1 "%s"\n' gramlib/grammar.ml > gramlib/.pack/gramlib__Grammar.ml - echo " \ - module Ploc = Gramlib__Ploc \ - module Plexing = Gramlib__Plexing \ - module Gramext = Gramlib__Gramext \ - module Grammar = Gramlib__Grammar" > gramlib/.pack/gramlib.ml - cat gramlib/plexing.ml >> gramlib/.pack/gramlib__Plexing.ml - cat gramlib/ploc.ml >> gramlib/.pack/gramlib__Ploc.ml - 30 states, 1657 transitions, table size 6808 bytes - 6052 additional bytes used for bindings - cat gramlib/gramext.ml >> gramlib/.pack/gramlib__Gramext.ml - cat gramlib/grammar.ml >> gramlib/.pack/gramlib__Grammar.ml - printf '# 1 "%s"\n' gramlib/ploc.mli > gramlib/.pack/gramlib__Ploc.mli - printf '# 1 "%s"\n' gramlib/plexing.mli > gramlib/.pack/gramlib__Plexing.mli - 80 states, 774 transitions, table size 3576 bytes - printf '# 1 "%s"\n' gramlib/gramext.mli > gramlib/.pack/gramlib__Gramext.mli - printf '# 1 "%s"\n' gramlib/grammar.mli > gramlib/.pack/gramlib__Grammar.mli - 124 states, 1808 transitions, table size 7976 bytes - 217 states, 2223 transitions, table size 10194 bytes - cat gramlib/ploc.mli >> gramlib/.pack/gramlib__Ploc.mli - cat gramlib/plexing.mli >> gramlib/.pack/gramlib__Plexing.mli - cat gramlib/gramext.mli >> gramlib/.pack/gramlib__Gramext.mli - cat gramlib/grammar.mli >> gramlib/.pack/gramlib__Grammar.mli - 240 states, 15992 transitions, table size 65408 bytes - OCAMLC clib/segmenttree.mli - OCAMLC clib/unicode.mli - OCAMLC tools/coqdep_lexer.mli - OCAMLC tools/coqdep_common.mli - OCAMLC tools/ocamllibdep.ml - OCAMLC coqpp/coqpp_parse.mli - WRITE kernel/byterun/coq_instruct.h - WRITE kernel/copcodes.ml - OCAMLOPT clib/segmenttree.ml - WRITE kernel/byterun/coq_jumptbl.h - OCAMLC clib/segmenttree.ml - OCAMLC tools/coqdep_boot.ml - OCAMLC coqpp/coqpp_parse.ml - CCDEP kernel/byterun/coq_fix_code.c - CCDEP kernel/byterun/coq_values.c - CCDEP kernel/byterun/coq_memory.c - CCDEP kernel/byterun/coq_interp.c - OCAMLOPT tools/ocamllibdep.ml - OCAMLC clib/unicodetable.ml - 2714 states, 8784 transitions, table size 51420 bytes - 17613 additional bytes used for bindings - OCAMLC coqpp/coqpp_lex.ml - OCAMLBEST -o bin/ocamllibdep - OCAMLC -a bin/coqpp - COQPP toplevel/g_toplevel.mlg - COQPP parsing/g_prim.mlg - COQPP parsing/g_constr.mlg - COQPP vernac/g_vernac.mlg - COQPP vernac/g_proofs.mlg - COQPP plugins/ltac/g_class.mlg - COQPP plugins/ltac/g_ltac.mlg - COQPP plugins/ltac/extraargs.mlg - COQPP plugins/ltac/coretactics.mlg - COQPP plugins/ltac/g_eqdecide.mlg - COQPP plugins/ltac/g_obligations.mlg - COQPP plugins/ltac/extratactics.mlg - COQPP plugins/ltac/g_auto.mlg - COQPP plugins/ltac/g_rewrite.mlg - COQPP plugins/ltac/profile_ltac_tactics.mlg - COQPP plugins/ltac/g_tactic.mlg - COQPP plugins/cc/g_congruence.mlg - COQPP plugins/funind/g_indfun.mlg - COQPP plugins/btauto/g_btauto.mlg - COQPP plugins/extraction/g_extraction.mlg - COQPP plugins/firstorder/g_ground.mlg - COQPP plugins/micromega/g_zify.mlg - COQPP plugins/micromega/g_micromega.mlg - COQPP plugins/syntax/g_numeral.mlg - COQPP plugins/syntax/g_string.mlg - COQPP plugins/omega/g_omega.mlg - COQPP plugins/ssr/ssrvernac.mlg - COQPP plugins/ssrmatching/g_ssrmatching.mlg - COQPP plugins/ssrsearch/g_search.mlg - COQPP plugins/derive/g_derive.mlg - COQPP plugins/ssr/ssrparser.mlg - COQPP plugins/setoid_ring/g_newring.mlg - COQPP user-contrib/Ltac2/g_ltac2.mlg - COQPP plugins/nsatz/g_nsatz.mlg - COQPP plugins/rtauto/g_rtauto.mlg - OCAMLLIBDEP checker/MLLIBFILES checker/MLPACKFILES - OCAMLDEP MLFILES MLIFILES - OCAMLLIBDEP MLLIBFILES MLPACKFILES - OCAMLDEP plugins/MLFILES plugins/MLIFILES - OCAMLLIBDEP plugins/MLLIBFILES plugins/MLPACKFILES - OCAMLDEP user-contrib/MLFILES user-contrib/MLIFILES - OCAMLLIBDEP user-contrib/MLLIBFILES user-contrib/MLPACKFILES - OCAMLOPT clib/unicodetable.ml - OCAMLC clib/unicode.ml - OCAMLC clib/minisys.ml - OCAMLOPT clib/unicode.ml - OCAMLOPT clib/minisys.ml - OCAMLOPT tools/coqdep_lexer.ml - OCAMLOPT tools/coqdep_common.ml - OCAMLOPT tools/coqdep_boot.ml - OCAMLBEST -o bin/coqdep_boot - COQDEP VFILES - rm coqpp/coqpp_parse.mli - make[1]: Circular coqpp/coqpp_parse.cmi <- coqpp/coqpp_parse.cmo dependency dropped. - "/home/opam/.opam/default/bin/ocamlfind" ocamlc -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67 -safe-string -strict-sequence ide/default_bindings_src.ml -o ide/default_bindings_src.exe - ide/default_bindings_src.exe ide/default.bindings - make[1]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/coqide.8.12.1' [coqide: make coqide-opt] + /usr/bin/make "COQ_USE_DUNE=" "-j39" "coqide-opt" (CWD=/home/opam/.opam/default/.opam-switch/build/coqide.8.12.1) - rm -f - /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build coqide-opt - make[1]: Entering directory '/home/opam/.opam/default/.opam-switch/build/coqide.8.12.1' - make[1]: Circular coqpp/coqpp_parse.cmi <- coqpp/coqpp_parse.cmo dependency dropped. - OCAMLC config/coq_config.mli - OCAMLC clib/cObj.mli - OCAMLC clib/cEphemeron.mli - OCAMLC clib/cSig.mli - OCAMLC clib/hashset.mli - OCAMLC clib/orderedType.mli - OCAMLC clib/range.mli - OCAMLC clib/cArray.mli - OCAMLC clib/option.mli - OCAMLC clib/bigint.mli - OCAMLC clib/cUnix.mli - OCAMLC clib/cThread.mli - OCAMLC clib/predicate.mli - OCAMLC clib/trie.mli - OCAMLC clib/heap.mli - OCAMLC clib/unionfind.mli - OCAMLC clib/store.mli - OCAMLC clib/exninfo.mli - OCAMLC clib/iStream.mli - OCAMLC clib/terminal.mli - OCAMLC clib/monad.mli - OCAMLC clib/diff2.mli - OCAMLC lib/flags.mli - OCAMLC lib/hook.mli - OCAMLC lib/control.mli - OCAMLC lib/xml_datatype.mli - OCAMLC lib/pp.mli - OCAMLC lib/cProfile.mli - OCAMLC lib/remoteCounter.mli - OCAMLC lib/spawn.mli - OCAMLC lib/envars.mli - OCAMLC lib/coqProject_file.mli - OCAMLC ide/protocol/xml_lexer.mli - OCAMLC ide/configwin_types.ml - OCAMLC ide/configwin_messages.ml - OCAMLC ide/configwin.mli - OCAMLC ide/tags.mli - OCAMLC ide/wg_Notebook.mli - OCAMLC ide/utf8_convert.mli - OCAMLC ide/unicode_bindings.mli - OCAMLC ide/coq_lex.mli - OCAMLC ide/sentence.mli - OCAMLC ide/gtk_parsing.mli - OCAMLC ide/wg_Segment.mli - OCAMLC ide/wg_Find.mli - OCAMLC ide/wg_Detachable.mli - OCAMLC ide/coqide_ui.mli - OCAMLC ide/coqide.mli - OCAMLC ide/coqide_os_specific.mli - OCAMLC ide/coq_commands.mli - OCAMLC kernel/uint63.mli - OCAMLC kernel/copcodes.ml - OCAMLC engine/logic_monad.mli - OCAMLC interp/numTok.mli - OCAMLC gramlib/.pack/gramlib.ml - OCAMLC tactics/dnet.mli - OCAMLC tactics/dn.mli - OCAMLC stm/dag.mli - OCAMLC stm/spawned.mli - OCAMLC stm/tQueue.mli - OCAMLC stm/coqworkmgrApi.mli - OCAMLC stm/vio_checking.mli - OCAMLC toplevel/workerLoop.mli - OCAMLC toplevel/usage.mli - OCAMLC toplevel/coqc.mli - OCAMLC kernel/byterun/coq_fix_code.c - OCAMLC kernel/byterun/coq_values.c - OCAMLC kernel/byterun/coq_memory.c - OCAMLC kernel/byterun/coq_interp.c - OCAMLOPT config/coq_config.ml - OCAMLOPT clib/cObj.ml - OCAMLOPT clib/cEphemeron.ml - OCAMLC clib/cMap.mli - OCAMLC clib/hashcons.mli - OCAMLC clib/cList.mli - OCAMLOPT clib/option.ml - OCAMLOPT clib/cThread.ml - OCAMLOPT clib/trie.ml - OCAMLOPT clib/predicate.ml - OCAMLOPT clib/heap.ml - OCAMLOPT clib/unionfind.ml - OCAMLC clib/dyn.mli - OCAMLOPT clib/terminal.ml - OCAMLOPT clib/iStream.ml - OCAMLOPT clib/monad.ml - OCAMLOPT clib/diff2.ml - OCAMLOPT lib/hook.ml - OCAMLC lib/loc.mli - OCAMLC lib/pp_diff.mli - OCAMLC lib/rtree.mli - OCAMLC lib/system.mli - OCAMLC lib/explore.mli - OCAMLC lib/future.mli - OCAMLC lib/genarg.mli - OCAMLOPT ide/protocol/xml_lexer.ml - OCAMLC ide/protocol/xml_parser.mli - OCAMLC ide/protocol/xml_printer.mli - OCAMLC ide/protocol/richpp.mli - OCAMLC ide/minilib.mli - OCAMLOPT ide/configwin_types.ml - OCAMLC ide/configwin_ihm.mli - OCAMLOPT ide/tags.ml - OCAMLOPT ide/utf8_convert.ml - OCAMLOPT ide/coq_commands.ml - OCAMLOPT ide/gtk_parsing.ml - OCAMLOPT kernel/uint63.ml - OCAMLC kernel/float64.mli - OCAMLOPT ide/coqide_os_specific.ml - OCAMLC kernel/cPrimitives.mli - OCAMLC kernel/evar.mli - OCAMLC library/summary.mli - OCAMLC interp/deprecation.mli - OCAMLOPT gramlib/.pack/gramlib.ml - OCAMLOPT kernel/copcodes.ml - OCAMLC gramlib/.pack/gramlib__Ploc.mli - OCAMLC gramlib/.pack/gramlib__Gramext.mli - OCAMLC stm/vcs.mli - OCAMLC stm/workerPool.mli - OCAMLOPT stm/coqworkmgrApi.ml - OCAMLOPT toplevel/usage.ml - OCAMLOPT -a -o config/config.cmxa - OCAMLOPT clib/cMap.ml - OCAMLC clib/int.mli - OCAMLC clib/cSet.mli - OCAMLC clib/cString.mli - OCAMLC clib/hMap.mli - OCAMLC lib/stateid.mli - OCAMLC lib/cWarnings.mli - OCAMLC lib/cErrors.mli - OCAMLC lib/cAst.mli - OCAMLC lib/aux_file.mli - OCAMLC ide/protocol/serialize.mli - OCAMLOPT ide/configwin_messages.ml - OCAMLOPT tactics/dnet.ml - OCAMLOPT ide/protocol/xml_printer.ml - OCAMLOPT gramlib/.pack/gramlib__Gramext.ml - OCAMLC lib/acyclicGraph.mli - OCAMLOPT ide/coq_lex.ml - OCAMLC lib/dAst.mli - OCAMLC lib/feedback.mli - OCAMLC ide/document.mli - OCAMLOPT ide/wg_Detachable.ml - OCAMLC lib/util.mli - OCAMLC lib/objFile.mli - OCAMLOPT kernel/float64.ml - OCAMLC ide/ideutils.mli - OCAMLC stm/asyncTaskQueue.mli - OCAMLOPT ide/protocol/xml_parser.ml - OCAMLC ide/protocol/interface.ml - OCAMLC ide/config_lexer.mli - OCAMLC kernel/names.mli - OCAMLC ide/preferences.mli - OCAMLC kernel/esubst.mli - OCAMLC parsing/tok.mli - OCAMLC gramlib/.pack/gramlib__Plexing.mli - OCAMLOPT clib/int.ml - OCAMLC gramlib/.pack/gramlib__Grammar.mli - OCAMLC parsing/cLexer.mli - OCAMLOPT ide/sentence.ml - OCAMLC ide/protocol/xmlprotocol.mli - OCAMLC ide/coq.mli - OCAMLC ide/wg_ProofView.mli - OCAMLC ide/wg_ScriptView.mli - OCAMLC ide/wg_Completion.mli - OCAMLC ide/wg_MessageView.mli - OCAMLC ide/fileOps.mli - OCAMLC ide/wg_RoutedMessageViews.mli - OCAMLC kernel/transparentState.mli - OCAMLC kernel/univ.mli - OCAMLC kernel/retroknowledge.mli - OCAMLC engine/evar_kinds.mli - OCAMLC library/libnames.mli - OCAMLC pretyping/locus.ml - OCAMLC tactics/declareScheme.mli - OCAMLC proofs/goal_select.mli - OCAMLC vernac/canonical.mli - OCAMLOPT clib/hashset.ml - OCAMLOPT clib/orderedType.ml - OCAMLOPT clib/cList.ml - OCAMLOPT clib/range.ml - OCAMLOPT clib/hMap.ml - OCAMLOPT stm/dag.ml - OCAMLOPT clib/dyn.ml - OCAMLOPT clib/bigint.ml - OCAMLC library/coqlib.mli - OCAMLC interp/decls.mli - OCAMLC vernac/loadpath.mli - OCAMLC kernel/conv_oracle.mli - OCAMLC pretyping/locusops.mli - OCAMLC kernel/uGraph.mli - OCAMLC kernel/sorts.mli - OCAMLC engine/univNames.mli - OCAMLC tactics/declareUctx.mli - OCAMLC ide/coqOps.mli - OCAMLOPT clib/store.ml - OCAMLC kernel/context.mli - OCAMLOPT clib/exninfo.ml - OCAMLOPT clib/hashcons.ml - OCAMLC kernel/constr.mli - OCAMLC ide/wg_Command.mli - OCAMLC ide/session.mli - OCAMLOPT lib/flags.ml - OCAMLOPT lib/control.ml - OCAMLOPT lib/loc.ml - OCAMLC kernel/vars.mli - OCAMLC kernel/term.mli - OCAMLC kernel/mod_subst.mli - OCAMLC kernel/vmvalues.mli - OCAMLC kernel/nativevalues.mli - OCAMLC engine/univSubst.mli - OCAMLC engine/univProblem.mli - OCAMLC engine/univops.mli - OCAMLC engine/nameops.mli - OCAMLC pretyping/pattern.ml - OCAMLOPT clib/cSet.ml - OCAMLC pretyping/keys.mli - OCAMLC kernel/opaqueproof.mli - OCAMLC library/globnames.mli - OCAMLC tactics/term_dnet.mli - OCAMLC kernel/cbytecodes.mli - OCAMLC kernel/vm.mli - OCAMLC engine/univMinim.mli - OCAMLOPT lib/cAst.ml - OCAMLOPT gramlib/.pack/gramlib__Ploc.ml - OCAMLC library/libobject.mli - OCAMLC library/nametab.mli - OCAMLC ide/microPG.mli - OCAMLC vernac/library.mli - OCAMLC kernel/cemitcodes.mli - OCAMLOPT lib/dAst.ml - OCAMLC kernel/declarations.ml - OCAMLOPT clib/cString.ml - OCAMLOPT clib/cArray.ml - OCAMLC kernel/entries.ml - OCAMLC kernel/environ.mli - OCAMLC kernel/cooking.mli - OCAMLC kernel/declareops.mli - OCAMLOPT ide/protocol/serialize.ml - OCAMLOPT clib/cUnix.ml - OCAMLC kernel/primred.mli - OCAMLC kernel/cClosure.mli - OCAMLC kernel/reduction.mli - OCAMLC kernel/clambda.mli - OCAMLC kernel/nativelambda.mli - OCAMLC kernel/cbytegen.mli - OCAMLC kernel/csymtable.mli - OCAMLC kernel/type_errors.mli - OCAMLC kernel/inductive.mli - OCAMLC kernel/modops.mli - OCAMLC kernel/typeops.mli - OCAMLC kernel/indTyping.mli - OCAMLC kernel/inferCumulativity.mli - OCAMLC kernel/indtypes.mli - OCAMLC kernel/term_typing.mli - OCAMLC kernel/subtyping.mli - OCAMLC kernel/mod_typing.mli - OCAMLC kernel/section.mli - OCAMLC library/goptions.mli - OCAMLC engine/univGen.mli - OCAMLC printing/printmod.mli - OCAMLC pretyping/arguments_renaming.mli - OCAMLC pretyping/heads.mli - OCAMLOPT -a -o clib/clib.cmxa - OCAMLOPT lib/util.ml - OCAMLOPT lib/pp.ml - OCAMLOPT lib/coqProject_file.ml - OCAMLC kernel/relevanceops.mli - OCAMLC kernel/vconv.mli - OCAMLC kernel/nativecode.mli - OCAMLC kernel/nativeconv.mli - OCAMLC library/lib.mli - OCAMLC vernac/attributes.mli - OCAMLC kernel/nativelib.mli - OCAMLC kernel/nativelibrary.mli - OCAMLC kernel/safe_typing.mli - OCAMLC library/states.mli - OCAMLC library/global.mli - OCAMLC engine/uState.mli - OCAMLOPT ide/wg_Notebook.ml - OCAMLOPT lib/envars.ml - OCAMLOPT ide/config_lexer.ml - OCAMLOPT kernel/esubst.ml - OCAMLOPT gramlib/.pack/gramlib__Plexing.ml - OCAMLOPT tactics/dn.ml - OCAMLC engine/evd.mli - OCAMLOPT lib/pp_diff.ml - OCAMLOPT lib/cErrors.ml - OCAMLOPT lib/stateid.ml - OCAMLOPT lib/rtree.ml - OCAMLOPT ide/protocol/richpp.ml - OCAMLOPT ide/minilib.ml - OCAMLOPT kernel/evar.ml - OCAMLOPT interp/numTok.ml - OCAMLOPT lib/cProfile.ml - OCAMLOPT lib/acyclicGraph.ml - OCAMLOPT lib/future.ml - OCAMLOPT lib/spawn.ml - OCAMLOPT lib/genarg.ml - OCAMLOPT lib/remoteCounter.ml - OCAMLOPT kernel/names.ml - OCAMLOPT kernel/cPrimitives.ml - OCAMLOPT stm/vcs.ml - OCAMLOPT stm/workerPool.ml - OCAMLOPT stm/tQueue.ml - OCAMLOPT ide/configwin_ihm.ml - OCAMLOPT lib/feedback.ml - OCAMLOPT ide/document.ml - OCAMLC engine/eConstr.mli - OCAMLC engine/proofview_monad.mli - OCAMLC pretyping/indrec.mli - OCAMLOPT lib/cWarnings.ml - OCAMLOPT lib/explore.ml - OCAMLOPT lib/aux_file.ml - OCAMLOPT ide/protocol/interface.ml - OCAMLOPT engine/logic_monad.ml - OCAMLC pretyping/pretype_errors.mli - OCAMLC pretyping/reductionops.mli - OCAMLC pretyping/retyping.mli - OCAMLC pretyping/inductiveops.mli - OCAMLC pretyping/vnorm.mli - OCAMLC pretyping/cbv.mli - OCAMLC pretyping/nativenorm.mli - OCAMLC pretyping/evardefine.mli - OCAMLC pretyping/typing.mli - OCAMLC pretyping/typeclasses_errors.mli - OCAMLC pretyping/typeclasses.mli - OCAMLC pretyping/coercionops.mli - OCAMLC pretyping/program.mli - OCAMLOPT gramlib/.pack/gramlib__Grammar.ml - OCAMLC tactics/btermdn.mli - OCAMLC proofs/goal.mli - OCAMLC tactics/hipattern.mli - OCAMLC vernac/recLemmas.mli - OCAMLC engine/namegen.mli - OCAMLOPT stm/spawned.ml - OCAMLC engine/termops.mli - OCAMLC engine/proofview.mli - OCAMLC pretyping/find_subterm.mli - OCAMLC pretyping/evarsolve.mli - OCAMLOPT lib/system.ml - OCAMLOPT library/summary.ml - OCAMLOPT interp/deprecation.ml - OCAMLOPT ide/protocol/xmlprotocol.ml - OCAMLC pretyping/recordops.mli - OCAMLC engine/evarutil.mli - OCAMLC pretyping/glob_term.ml - OCAMLC proofs/tactypes.ml - OCAMLOPT parsing/tok.ml - OCAMLC proofs/miscprint.mli - OCAMLC pretyping/evarconv.mli - OCAMLC engine/ftactic.mli - OCAMLC proofs/refine.mli - OCAMLC proofs/logic.mli - OCAMLC proofs/refiner.mli - OCAMLC proofs/tacmach.mli - OCAMLC tactics/ind_tables.mli - OCAMLC tactics/abstract.mli - OCAMLC tactics/tacticals.mli - OCAMLC tactics/contradiction.mli - OCAMLC tactics/inv.mli - OCAMLC tactics/eqdecide.mli - OCAMLC vernac/retrieveObl.mli - OCAMLC pretyping/geninterp.mli - OCAMLC interp/constrexpr.ml - OCAMLC proofs/proof.mli - OCAMLC vernac/declareUniv.mli - OCAMLOPT parsing/cLexer.ml - OCAMLC interp/notation_term.ml - OCAMLC interp/smartlocate.mli - OCAMLC interp/constrexpr_ops.mli - OCAMLC interp/impargs.mli - OCAMLC interp/modintern.mli - OCAMLC parsing/pcoq.mli - OCAMLC printing/genprint.mli - OCAMLC printing/pputils.mli - OCAMLC vernac/declaremods.mli - OCAMLC printing/ppconstr.mli - OCAMLC vernac/himsg.mli - OCAMLC vernac/prettyp.mli - OCAMLC vernac/comPrimitive.mli - OCAMLC pretyping/ltac_pretype.ml - OCAMLC printing/proof_diffs.mli - OCAMLC proofs/proof_bullet.mli - OCAMLC parsing/extend.ml - OCAMLC pretyping/coercion.mli - OCAMLC interp/genintern.mli - OCAMLC interp/notation.mli - OCAMLC interp/notation_ops.mli - OCAMLC interp/reserve.mli - OCAMLC interp/syntax_def.mli - OCAMLC tactics/eqschemes.mli - OCAMLC tactics/elimschemes.mli - OCAMLC vernac/auto_ind_decl.mli - OCAMLOPT lib/objFile.ml - OCAMLC parsing/g_prim.ml - OCAMLC parsing/ppextend.mli - OCAMLC parsing/g_constr.ml - OCAMLC pretyping/glob_ops.mli - OCAMLC pretyping/constr_matching.mli - OCAMLC pretyping/patternops.mli - OCAMLC pretyping/tacred.mli - OCAMLC pretyping/globEnv.mli - OCAMLC pretyping/detyping.mli - OCAMLC proofs/evar_refiner.mli - OCAMLC interp/stdarg.mli - OCAMLC printing/printer.mli - OCAMLC tactics/genredexpr.ml - OCAMLC interp/constrextern.mli - OCAMLC interp/dumpglob.mli - OCAMLC parsing/notation_gram.ml - OCAMLC vernac/egramcoq.mli - OCAMLC parsing/notgram_ops.mli - OCAMLC pretyping/cases.mli - OCAMLC pretyping/pretyping.mli - OCAMLC tactics/redops.mli - OCAMLC tactics/redexpr.mli - OCAMLC tactics/ppred.mli - OCAMLC vernac/assumptions.mli - OCAMLC toplevel/coqcargs.mli - OCAMLC pretyping/unification.mli - OCAMLOPT -a -o lib/lib.cmxa - OCAMLC interp/implicit_quantifiers.mli - OCAMLC interp/constrintern.mli - OCAMLC vernac/declareInd.mli - OCAMLOPT ide/configwin.ml - OCAMLC proofs/clenv.mli - OCAMLOPT kernel/transparentState.ml - OCAMLOPT kernel/univ.ml - OCAMLOPT kernel/retroknowledge.ml - OCAMLOPT library/libnames.ml - OCAMLOPT engine/evar_kinds.ml - OCAMLOPT -a -o ide/ide_common.cmxa - OCAMLOPT pretyping/locus.ml - OCAMLOPT -a -o ide/protocol/ideprotocol.cmxa - OCAMLC proofs/clenvtac.mli - OCAMLC tactics/hints.mli - OCAMLC tactics/tactics.mli - OCAMLOPT ide/preferences.ml - OCAMLOPT kernel/conv_oracle.ml - OCAMLC tactics/auto.mli - OCAMLC tactics/eauto.mli - OCAMLC tactics/class_tactics.mli - OCAMLC vernac/vernacexpr.ml - OCAMLOPT pretyping/locusops.ml - OCAMLC tactics/elim.mli - OCAMLC tactics/equality.mli - OCAMLC vernac/pvernac.mli - OCAMLC vernac/egramml.mli - OCAMLC vernac/ppvernac.mli - OCAMLC vernac/metasyntax.mli - OCAMLC vernac/proof_using.mli - OCAMLC vernac/declare.mli - OCAMLC vernac/vernacprop.mli - OCAMLC vernac/search.mli - OCAMLC vernac/comHints.mli - OCAMLC vernac/indschemes.mli - OCAMLC vernac/comSearch.mli - OCAMLC vernac/comInductive.mli - OCAMLC vernac/record.mli - OCAMLC vernac/mltop.mli - OCAMLC vernac/comArguments.mli - OCAMLC vernac/topfmt.mli - OCAMLC vernac/g_vernac.ml - OCAMLC toplevel/g_toplevel.ml - OCAMLC tactics/autorewrite.mli - OCAMLC vernac/locality.mli - OCAMLC vernac/declareObl.mli - OCAMLC vernac/comCoercion.mli - OCAMLC vernac/comDefinition.mli - OCAMLC vernac/comProgramFixpoint.mli - OCAMLC vernac/comAssumption.mli - OCAMLC vernac/proof_global.ml - OCAMLC vernac/pfedit.ml - OCAMLC vernac/declareDef.ml - OCAMLC vernac/lemmas.mli - OCAMLC vernac/vernacextend.mli - OCAMLC vernac/obligations.mli - OCAMLC vernac/comFixpoint.mli - OCAMLC vernac/classes.mli - OCAMLC vernac/vernacstate.mli - OCAMLC vernac/vernacinterp.mli - OCAMLOPT -a -o gramlib/.pack/gramlib.cmxa - OCAMLC stm/vernac_classifier.mli - OCAMLC stm/stm.mli - OCAMLC vernac/vernacentries.mli - OCAMLC stm/proofBlockDelimiter.mli - OCAMLC toplevel/vernac.mli - OCAMLC toplevel/coqargs.mli - OCAMLC toplevel/coqinit.mli - OCAMLC toplevel/coqloop.mli - OCAMLC toplevel/coqtop.mli - OCAMLC toplevel/ccompile.mli - OCAMLOPT kernel/uGraph.ml - OCAMLOPT kernel/sorts.ml - OCAMLOPT kernel/context.ml - OCAMLOPT ide/wg_Segment.ml - OCAMLOPT ide/ideutils.ml - OCAMLOPT ide/coqide_ui.ml - OCAMLOPT engine/nameops.ml - OCAMLOPT kernel/constr.ml - OCAMLC vernac/g_proofs.ml - OCAMLOPT ide/unicode_bindings.ml - OCAMLOPT ide/coq.ml - OCAMLOPT ide/wg_MessageView.ml - OCAMLOPT ide/wg_Find.ml - OCAMLOPT ide/fileOps.ml - OCAMLOPT ide/wg_ProofView.ml - OCAMLOPT ide/wg_Completion.ml - OCAMLOPT ide/wg_Command.ml - OCAMLOPT ide/wg_RoutedMessageViews.ml - cd kernel/byterun/ && \ - "/home/opam/.opam/default/bin/ocamlfind" ocamlmklib -oc coqrun coq_fix_code.o coq_memory.o coq_values.o coq_interp.o - OCAMLOPT kernel/vmvalues.ml - OCAMLOPT kernel/vars.ml - OCAMLOPT engine/univSubst.ml - OCAMLOPT kernel/nativevalues.ml - OCAMLOPT pretyping/pattern.ml - OCAMLOPT ide/wg_ScriptView.ml - OCAMLOPT engine/univProblem.ml - OCAMLOPT kernel/cbytecodes.ml - OCAMLOPT kernel/term.ml - OCAMLOPT kernel/mod_subst.ml - OCAMLOPT ide/coqOps.ml - OCAMLOPT kernel/cemitcodes.ml - OCAMLOPT kernel/opaqueproof.ml - OCAMLOPT library/globnames.ml - OCAMLOPT library/libobject.ml - OCAMLOPT library/nametab.ml - OCAMLOPT kernel/declarations.ml - OCAMLOPT kernel/entries.ml - OCAMLOPT kernel/cooking.ml - OCAMLOPT kernel/declareops.ml - OCAMLOPT engine/univNames.ml - OCAMLOPT ide/session.ml - OCAMLOPT kernel/environ.ml - OCAMLOPT kernel/primred.ml - OCAMLOPT kernel/section.ml - OCAMLOPT ide/microPG.ml - OCAMLOPT kernel/cClosure.ml - OCAMLOPT ide/coqide.ml - OCAMLOPT kernel/relevanceops.ml - OCAMLOPT kernel/reduction.ml - OCAMLOPT kernel/clambda.ml - OCAMLOPT kernel/nativelambda.ml - OCAMLOPT kernel/type_errors.ml - OCAMLOPT kernel/inferCumulativity.ml - OCAMLOPT pretyping/heads.ml - OCAMLOPT kernel/inductive.ml - OCAMLOPT -a -o ide/ide.cmxa - OCAMLOPT kernel/cbytegen.ml - OCAMLOPT kernel/nativecode.ml - OCAMLOPT -o bin/coqide - OCAMLOPT kernel/csymtable.ml - OCAMLOPT kernel/modops.ml - OCAMLOPT kernel/vm.ml - OCAMLOPT kernel/vconv.ml - OCAMLOPT kernel/subtyping.ml - OCAMLOPT kernel/nativelibrary.ml - OCAMLOPT kernel/nativelib.ml - OCAMLOPT kernel/nativeconv.ml - OCAMLOPT kernel/typeops.ml - OCAMLOPT kernel/indTyping.ml - OCAMLOPT kernel/term_typing.ml - OCAMLOPT kernel/mod_typing.ml - OCAMLOPT kernel/indtypes.ml - OCAMLOPT kernel/safe_typing.ml - OCAMLOPT -a -o kernel/kernel.cmxa - OCAMLOPT library/global.ml - OCAMLOPT engine/univGen.ml - OCAMLOPT library/lib.ml - OCAMLOPT tactics/declareUctx.ml - OCAMLOPT stm/asyncTaskQueue.ml - OCAMLOPT library/states.ml - OCAMLOPT library/goptions.ml - OCAMLOPT library/coqlib.ml - OCAMLOPT pretyping/keys.ml - OCAMLOPT interp/decls.ml - OCAMLOPT tactics/declareScheme.ml - OCAMLOPT engine/univMinim.ml - OCAMLOPT -a -o library/library.cmxa - OCAMLOPT proofs/goal_select.ml - OCAMLOPT vernac/attributes.ml - OCAMLOPT engine/uState.ml - OCAMLOPT engine/univops.ml - OCAMLOPT engine/evd.ml - OCAMLOPT engine/eConstr.ml - OCAMLOPT engine/proofview_monad.ml - OCAMLOPT engine/namegen.ml - OCAMLOPT pretyping/pretype_errors.ml - OCAMLOPT pretyping/typeclasses_errors.ml - OCAMLOPT engine/termops.ml - OCAMLOPT pretyping/glob_term.ml - OCAMLOPT proofs/tactypes.ml - OCAMLOPT interp/constrexpr.ml - OCAMLOPT proofs/miscprint.ml - OCAMLOPT interp/notation_term.ml - OCAMLOPT parsing/extend.ml - OCAMLOPT engine/evarutil.ml - OCAMLOPT pretyping/find_subterm.ml - OCAMLOPT tactics/term_dnet.ml - OCAMLOPT engine/proofview.ml - OCAMLOPT pretyping/reductionops.ml - OCAMLOPT pretyping/program.ml - OCAMLOPT engine/ftactic.ml - OCAMLOPT proofs/goal.ml - OCAMLOPT tactics/ind_tables.ml - OCAMLOPT vernac/retrieveObl.ml - OCAMLOPT -a -o engine/engine.cmxa - OCAMLOPT pretyping/geninterp.ml - OCAMLOPT pretyping/inductiveops.ml - OCAMLOPT pretyping/cbv.ml - OCAMLOPT pretyping/evardefine.ml - OCAMLOPT pretyping/recordops.ml - OCAMLOPT vernac/recLemmas.ml - OCAMLOPT interp/stdarg.ml - OCAMLOPT printing/genprint.ml - OCAMLOPT pretyping/ltac_pretype.ml - OCAMLOPT printing/pputils.ml - OCAMLOPT parsing/pcoq.ml - OCAMLOPT vernac/canonical.ml - OCAMLOPT pretyping/nativenorm.ml - OCAMLOPT pretyping/arguments_renaming.ml - OCAMLOPT pretyping/glob_ops.ml - OCAMLOPT parsing/g_prim.ml - OCAMLOPT pretyping/retyping.ml - OCAMLOPT interp/impargs.ml - OCAMLOPT pretyping/vnorm.ml - OCAMLOPT pretyping/evarsolve.ml - OCAMLOPT pretyping/typeclasses.ml - OCAMLOPT pretyping/indrec.ml - OCAMLOPT pretyping/globEnv.ml - OCAMLOPT pretyping/patternops.ml - OCAMLOPT interp/dumpglob.ml - OCAMLOPT tactics/eqschemes.ml - OCAMLOPT tactics/elimschemes.ml - OCAMLOPT pretyping/evarconv.ml - OCAMLOPT tactics/btermdn.ml - OCAMLOPT pretyping/constr_matching.ml - OCAMLOPT pretyping/detyping.ml - OCAMLOPT tactics/hipattern.ml - OCAMLOPT pretyping/typing.ml - OCAMLOPT pretyping/tacred.ml - OCAMLOPT proofs/refine.ml - OCAMLOPT interp/genintern.ml - OCAMLOPT interp/notation_ops.ml - OCAMLOPT tactics/genredexpr.ml - OCAMLOPT tactics/redops.ml - OCAMLOPT tactics/ppred.ml - OCAMLOPT pretyping/coercionops.ml - OCAMLOPT tactics/redexpr.ml - OCAMLOPT pretyping/coercion.ml - OCAMLOPT pretyping/cases.ml - OCAMLOPT interp/notation.ml - OCAMLOPT interp/reserve.ml - OCAMLOPT interp/syntax_def.ml - OCAMLOPT parsing/notation_gram.ml - OCAMLOPT parsing/notgram_ops.ml - OCAMLOPT parsing/ppextend.ml - OCAMLOPT vernac/egramcoq.ml - OCAMLOPT interp/smartlocate.ml - OCAMLOPT pretyping/pretyping.ml - OCAMLOPT pretyping/unification.ml - OCAMLOPT interp/constrexpr_ops.ml - OCAMLOPT proofs/evar_refiner.ml - OCAMLOPT vernac/declareUniv.ml - OCAMLOPT proofs/proof.ml - OCAMLOPT parsing/g_constr.ml - OCAMLOPT interp/implicit_quantifiers.ml - OCAMLOPT interp/constrintern.ml - OCAMLOPT proofs/logic.ml - OCAMLOPT proofs/proof_bullet.ml - OCAMLOPT -a -o pretyping/pretyping.cmxa - OCAMLOPT -a -o parsing/parsing.cmxa - OCAMLOPT proofs/refiner.ml - OCAMLOPT proofs/tacmach.ml - OCAMLOPT proofs/clenv.ml - OCAMLOPT interp/modintern.ml - OCAMLOPT interp/constrextern.ml - OCAMLOPT proofs/clenvtac.ml - OCAMLOPT -a -o proofs/proofs.cmxa - OCAMLOPT -a -o interp/interp.cmxa - OCAMLOPT printing/ppconstr.ml - OCAMLOPT printing/proof_diffs.ml - OCAMLOPT printing/printer.ml - OCAMLOPT printing/printmod.ml - OCAMLOPT tactics/tacticals.ml - OCAMLOPT tactics/hints.ml - OCAMLOPT vernac/himsg.ml - OCAMLOPT -a -o printing/printing.cmxa - OCAMLOPT vernac/declaremods.ml - OCAMLOPT tactics/tactics.ml - OCAMLOPT vernac/vernacexpr.ml - OCAMLOPT vernac/library.ml - OCAMLOPT vernac/pvernac.ml - OCAMLOPT vernac/vernacprop.ml - OCAMLOPT vernac/mltop.ml - OCAMLOPT vernac/comArguments.ml - OCAMLOPT vernac/g_vernac.ml - OCAMLOPT vernac/egramml.ml - OCAMLOPT toplevel/g_toplevel.ml - OCAMLOPT vernac/assumptions.ml - OCAMLOPT vernac/loadpath.ml - OCAMLOPT vernac/ppvernac.ml - OCAMLOPT vernac/metasyntax.ml - OCAMLOPT vernac/topfmt.ml - OCAMLOPT toplevel/coqcargs.ml - OCAMLOPT tactics/elim.ml - OCAMLOPT tactics/abstract.ml - OCAMLOPT tactics/equality.ml - OCAMLOPT tactics/contradiction.ml - OCAMLOPT tactics/auto.ml - OCAMLOPT vernac/proof_using.ml - OCAMLOPT vernac/declare.ml - OCAMLOPT tactics/eauto.ml - OCAMLOPT vernac/g_proofs.ml - OCAMLOPT vernac/locality.ml - OCAMLOPT vernac/comHints.ml - OCAMLOPT vernac/comCoercion.ml - OCAMLOPT vernac/comPrimitive.ml - OCAMLOPT vernac/proof_global.ml - OCAMLOPT vernac/pfedit.ml - OCAMLOPT vernac/declareDef.ml - OCAMLOPT vernac/declareObl.ml - OCAMLOPT vernac/lemmas.ml - OCAMLOPT tactics/class_tactics.ml - OCAMLOPT tactics/inv.ml - OCAMLOPT tactics/eqdecide.ml - OCAMLOPT tactics/autorewrite.ml - OCAMLOPT vernac/auto_ind_decl.ml - OCAMLOPT vernac/obligations.ml - OCAMLOPT vernac/vernacextend.ml - OCAMLOPT vernac/comFixpoint.ml - OCAMLOPT vernac/vernacstate.ml - OCAMLOPT -a -o tactics/tactics.cmxa - OCAMLOPT vernac/comDefinition.ml - OCAMLOPT vernac/classes.ml - OCAMLOPT vernac/comProgramFixpoint.ml - OCAMLOPT vernac/indschemes.ml - OCAMLOPT vernac/declareInd.ml - OCAMLOPT vernac/prettyp.ml - OCAMLOPT vernac/comInductive.ml - OCAMLOPT vernac/search.ml - OCAMLOPT vernac/comAssumption.ml - OCAMLOPT vernac/comSearch.ml - OCAMLOPT vernac/record.ml - OCAMLOPT vernac/vernacentries.ml - OCAMLOPT vernac/vernacinterp.ml - OCAMLOPT -a -o vernac/vernac.cmxa - OCAMLOPT stm/vernac_classifier.ml - OCAMLOPT stm/stm.ml - OCAMLOPT stm/proofBlockDelimiter.ml - OCAMLOPT stm/vio_checking.ml - OCAMLOPT toplevel/vernac.ml - OCAMLOPT toplevel/coqinit.ml - OCAMLOPT toplevel/coqargs.ml - OCAMLOPT -a -o stm/stm.cmxa - OCAMLOPT toplevel/coqloop.ml - OCAMLOPT toplevel/ccompile.ml - OCAMLOPT toplevel/coqtop.ml - OCAMLOPT toplevel/workerLoop.ml - OCAMLOPT toplevel/coqc.ml - OCAMLOPT -a -o toplevel/toplevel.cmxa - COQMKTOP -o bin/coqidetop.opt - findlib: [WARNING] Interface ratio.cmi occurs in several directories: /home/opam/.opam/default/lib/num, /home/opam/.opam/default/lib/ocaml - findlib: [WARNING] Interface big_int.cmi occurs in several directories: /home/opam/.opam/default/lib/num, /home/opam/.opam/default/lib/ocaml - findlib: [WARNING] Interface num.cmi occurs in several directories: /home/opam/.opam/default/lib/num, /home/opam/.opam/default/lib/ocaml - findlib: [WARNING] Interface nat.cmi occurs in several directories: /home/opam/.opam/default/lib/num, /home/opam/.opam/default/lib/ocaml - findlib: [WARNING] Interface arith_status.cmi occurs in several directories: /home/opam/.opam/default/lib/num, /home/opam/.opam/default/lib/ocaml - rm -f bin/coqidetop && cp bin/coqidetop.opt bin/coqidetop - make[1]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/coqide.8.12.1' -> compiled coqide.8.12.1 [coqide: make install-ide-bin] + /usr/bin/make "COQ_USE_DUNE=" "install-ide-bin" "install-ide-files" "install-ide-info" "install-ide-devfiles" (CWD=/home/opam/.opam/default/.opam-switch/build/coqide.8.12.1) - rm -f - /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build install-ide-bin install-ide-files install-ide-info install-ide-devfiles - make[1]: Entering directory '/home/opam/.opam/default/.opam-switch/build/coqide.8.12.1' - make[1]: Circular coqpp/coqpp_parse.cmi <- coqpp/coqpp_parse.cmo dependency dropped. - install -d "/home/opam/.opam/default/bin" - install bin/coqide "/home/opam/.opam/default/bin" - install -d "/home/opam/.opam/default/share/coq" - install -m 644 ide/coq.png ide/*.lang ide/coq_style.xml ide/default.bindings "/home/opam/.opam/default/share/coq" - install -d "/home/opam/.opam/default/lib/coq/config" - install -d "/home/opam/.opam/default/doc" - install -m 644 ide/FAQ "/home/opam/.opam/default/doc"/FAQ-CoqIde - install -d "/home/opam/.opam/default/lib/coq" - ./install.sh "/home/opam/.opam/default/lib/coq" \ - ide/minilib.cmi ide/configwin_messages.cmi ide/configwin_ihm.cmi ide/configwin.cmi ide/tags.cmi ide/wg_Notebook.cmi ide/config_lexer.cmi ide/utf8_convert.cmi ide/preferences.cmi ide/ideutils.cmi ide/unicode_bindings.cmi ide/coq.cmi ide/coq_lex.cmi ide/sentence.cmi ide/gtk_parsing.cmi ide/wg_Segment.cmi ide/wg_ProofView.cmi ide/wg_MessageView.cmi ide/wg_RoutedMessageViews.cmi ide/wg_Detachable.cmi ide/wg_Find.cmi ide/wg_Completion.cmi ide/wg_ScriptView.cmi ide/coq_commands.cmi ide/fileOps.cmi ide/document.cmi ide/coqOps.cmi ide/wg_Command.cmi ide/session.cmi ide/coqide_ui.cmi ide/microPG.cmi ide/coqide.cmi - ./install.sh "/home/opam/.opam/default/lib/coq" ide/ide.cmxa ide/ide.a - make[1]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/coqide.8.12.1' - make: 'install-ide-files' is up to date. - make: 'install-ide-info' is up to date. - make: 'install-ide-devfiles' is up to date. -> installed coqide.8.12.1 [WARNING] Opam packages conf-adwaita-icon-theme.2, conf-cairo.1, conf-gtk3.18 and conf-gtksourceview3.0+2 depend on the following system packages that are no longer installed: adwaita-icon-theme libcairo2-dev libexpat1-dev libgtk-3-dev libgtksourceview-3.0-dev - conf-adwaita-icon-theme.2: depends on adwaita-icon-theme - conf-cairo.1: depends on libcairo2-dev - conf-gtk3.18: depends on libexpat1-dev, libgtk-3-dev - conf-gtksourceview3.0+2: depends on libgtksourceview-3.0-dev === STDERR === 2026-09-03 23:47.35: OK: build coqide.8.12.1 (runc: 71.7s, disk: 44KB) 2026-09-03 23:47.35: Job succeeded