coq-tools icon indicating copy to clipboard operation
coq-tools copied to clipboard

Command line options -boot and -coqlib are incompatible.

Open JasonGross opened this issue 10 months ago • 0 comments

https://github.com/rocq-prover/rocq/pull/20506#issuecomment-2801221029

Running command (in: /github/workspace/builds/coq/coq-failing/_build_ci/equations/_build/default): "/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig" "-q" "-w" "-deprecated-native-compiler-option" "-native-output-dir" "-native-compiler" "on" "-nI" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/kernel" "-nI" "theories" "-nI" "theories/Prop" "-boot" "-coqlib" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//" "-R" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/theories" "Coq" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/equations/_build/default/theories/Prop" "Equations.Prop" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Stdlib" "Stdlib" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/equations/_build/default/theories" "Equations" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Stdlib" "Stdlib" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/boot" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/clib" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/config" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/engine" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/gramlib" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/interp" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/kernel" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/lib" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/library" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/parsing" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/perf" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/cc" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/cc_core" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/extraction" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/ltac" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/pretyping" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/printing" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/proofs" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/tactics" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/vernac" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/vm" "-I" "/root/.opamcache/4.14.2+flambda/lib/findlib" "-I" "/root/.opamcache/4.14.2+flambda/lib/ocaml" "-I" "/root/.opamcache/4.14.2+flambda/lib/ocaml/threads" "-I" "/root/.opamcache/4.14.2+flambda/lib/zarith" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/equations/_build/default/src" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/btauto" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/derive" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/firstorder" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/firstorder_core" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/funind" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/ltac2" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/ltac2_ltac1" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/micromega" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/micromega_core" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/nsatz" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/nsatz_core" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/number_string_notation" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/ring" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/rtauto" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/ssreflect" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/ssrmatching" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/tauto" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/tutorial/p0" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/tutorial/p1" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/tutorial/p2" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/tutorial/p3" "-I" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/rocq-runtime/plugins/zify" "-top" "Equations.Prop.NoCycle" "." "-Q" "/tmp/tmpy446w_ob" "" "/tmp/tmpy446w_ob/Equations/Prop/NoCycle.v" "-q"

The timeout for ('/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig',) has been set to: 3

This file produces the following output when Coq'ed: Command line options -boot and -coqlib are incompatible.

The current state of the file does not have a recognizable error. Traceback (most recent call last): File "/github/workspace/coq-tools/coq_tools/find_bug.py", line 3163, in main env["error_reg_string"] = get_error_reg_string(output_file_name, **env) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/github/workspace/coq-tools/coq_tools/find_bug.py", line 772, in get_error_reg_string error_reg_string = get_error_reg_string_of_output(output, output_file_name, **kwargs) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/github/workspace/coq-tools/coq_tools/find_bug.py", line 706, in get_error_reg_string_of_output error_reg_string = raw_input( ^^^^^^^^^^ EOFError: EOF when reading a line

JasonGross avatar Apr 14 '25 15:04 JasonGross