search

coq-community / run-coq-bug-minimizer

Repository for triggering runs of the Coq bug minimizer using GitHub Actions [maintainer=@JasonGross]
MIT License
2 stars 0 forks source link

Minimizer fails when coqc loads from the pwd implicitly #36

Open JasonGross opened 3 hours ago

JasonGross commented 3 hours ago

I guess the runner fails when coqc is loading files from pwd implicitly. That might be fixed by https://github.com/coq-community/run-coq-bug-minimizer/pull/35

Originally posted by @JasonGross in https://github.com/coq/coq/issues/19587#issuecomment-2364788059

@coqbot: minimize

#!/usr/bin/env bash
git clone "https://github.com/roglo/puiseuxth.git" -b coq-8.20.0
cd puiseuxth/coq
make
coqbot-app[bot] commented 3 hours ago

Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.

coqbot-app[bot] commented 3 hours ago

Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.

JasonGross commented 3 hours ago

Let's also try @coqbot: minimize

#!/usr/bin/env bash
mkdir foo
cd foo
echo 'Axiom A : Set.' > foo.v
echo 'Require Import foo.  Fail Check A.' > bar.v
coqc -q foo.v
coqc -q bar.v
coqbot-app[bot] commented 3 hours ago

Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.

coqbot-app[bot] commented 3 hours ago

Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.

coqbot-app[bot] commented 3 hours ago

@JasonGross, Error: Could not minimize file /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/puiseuxth/coq/F1Eq.v (full log on GitHub Actions, cc @JasonGross)

build log ``` + (/github/workspace/run-script.sh @ line 47) $ ocamlc -config version: 4.13.1 standard_library_default: /home/coq/.opam/4.13.1+flambda/lib/ocaml standard_library: /home/coq/.opam/4.13.1+flambda/lib/ocaml ccomp_type: cc c_compiler: gcc ocamlc_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlc_cppflags: -D_FILE_OFFSET_BITS=64 ocamlopt_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlopt_cppflags: -D_FILE_OFFSET_BITS=64 bytecomp_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 native_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 bytecomp_c_libraries: -lm -lpthread native_c_libraries: -lm native_pack_linker: ld -r -o ranlib: ranlib architecture: amd64 model: default int_size: 63 word_size: 64 system: linux asm: as asm_cfi_supported: true with_frame_pointers: false ext_exe: ext_obj: .o ext_asm: .s ext_lib: .a ext_dll: .so os_type: Unix default_executable_name: a.out systhread_supported: true host: x86_64-pc-linux-gnu target: x86_64-pc-linux-gnu flambda: true safe_string: true default_safe_string: true flat_float_array: true function_sections: true afl_instrument: false windows_unicode: false supports_shared_libraries: true exec_magic_number: Caml1999X030 cmi_magic_number: Caml1999I030 cmo_magic_number: Caml1999O030 cma_magic_number: Caml1999A030 cmx_magic_number: Caml1999y030 cmxa_magic_number: Caml1999z030 ast_impl_magic_number: Caml1999M030 ast_intf_magic_number: Caml1999N030 cmxs_magic_number: Caml1999D030 cmt_magic_number: Caml1999T030 linear_magic_number: Caml1999L030 + (/github/workspace/run-script.sh @ line 48) $ coqc --config MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --config MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.ler4muUIvl MINIMIZER_DEBUG: files: COQLIB=/home/coq/.opam/4.13.1+flambda/lib/coq/ COQCORELIB=/home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core/ DOCDIR=/home/coq/.opam/4.13.1+flambda/share/doc/ OCAMLFIND=/home/coq/.opam/4.13.1+flambda/bin/ocamlfind CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 WARN=-warn-error +a-3 HASNATDYNLINK=true COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax COQ_NATIVE_COMPILER_DEFAULT=no + (/github/workspace/run-script.sh @ line 49) $ coqc --version MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.4J3YvbMwzy MINIMIZER_DEBUG: files: The Coq Proof Assistant, version 8.20.0 compiled with OCaml 4.13.1 + (/github/workspace/run-script.sh @ line 50) $ true + (/github/workspace/run-script.sh @ line 50) $ coqtop MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqtop MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqtop.orig MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.ZsmKoaeTJy MINIMIZER_DEBUG: files: Welcome to Coq 8.20.0 Coq < + (/github/workspace/run-script.sh @ line 52) $ source /github/workspace/coqbot.sh ++ (/github/workspace/run-script.sh @ line 2) $ git clone https://github.com/roglo/puiseuxth.git -b coq-8.20.0 Cloning into 'puiseuxth'... ++ (/github/workspace/run-script.sh @ line 3) $ cd puiseuxth/coq ++ (/github/workspace/run-script.sh @ line 4) $ make coqc Misc.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Misc.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.dAewgJIGts MINIMIZER_DEBUG: files: Misc.v coqc Slope_base.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Slope_base.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.225Qr5eApY MINIMIZER_DEBUG: files: Slope_base.v coqc SlopeMisc.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig SlopeMisc.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.zt9jE1lBbz MINIMIZER_DEBUG: files: SlopeMisc.v coqc QbarM.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig QbarM.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.Z60PKiCQip MINIMIZER_DEBUG: files: QbarM.v coqc NbarM.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig NbarM.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.NJFBd8G210 MINIMIZER_DEBUG: files: NbarM.v coqc Field2.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Field2.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.8PhW6oc51t MINIMIZER_DEBUG: files: Field2.v coqc Fsummation.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Fsummation.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.KXTlbbMabq MINIMIZER_DEBUG: files: Fsummation.v coqc Fpolynomial.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Fpolynomial.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.D7VEuZApOF MINIMIZER_DEBUG: files: Fpolynomial.v coqc ConvexHull.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig ConvexHull.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.FMCMjj7SPK MINIMIZER_DEBUG: files: ConvexHull.v coqc Newton.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Newton.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.GAXee3O5DE MINIMIZER_DEBUG: files: Newton.v coqc ConvexHullMisc.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig ConvexHullMisc.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.GaPl6wH7Mm MINIMIZER_DEBUG: files: ConvexHullMisc.v coqc InSegment.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig InSegment.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.NvrsjdKvEo MINIMIZER_DEBUG: files: InSegment.v coqc NotInSegMisc.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig NotInSegMisc.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.WIiIPELLND MINIMIZER_DEBUG: files: NotInSegMisc.v coqc NotInSegment.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig NotInSegment.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.wwViVsYIAg MINIMIZER_DEBUG: files: NotInSegment.v coqc Power_series.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Power_series.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.qblGiI1PQ3 MINIMIZER_DEBUG: files: Power_series.v coqc Puiseux_series.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Puiseux_series.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.4vPZGh0Nlo MINIMIZER_DEBUG: files: Puiseux_series.v coqc Ps_add.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Ps_add.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.4SImIc7RFB MINIMIZER_DEBUG: files: Ps_add.v coqc Ps_add_compat.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Ps_add_compat.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.VXB1sbfAg7 MINIMIZER_DEBUG: files: Ps_add_compat.v coqc Ps_mul.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Ps_mul.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.287P7yOlqu MINIMIZER_DEBUG: files: Ps_mul.v coqc Ps_div.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Ps_div.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.Udd6MkGodV MINIMIZER_DEBUG: files: Ps_div.v coqc Puiseux_base.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Puiseux_base.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.UJV1FBohAp MINIMIZER_DEBUG: files: Puiseux_base.v coqc PolyConvexHull.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig PolyConvexHull.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.Rgk6OC3HUR MINIMIZER_DEBUG: files: PolyConvexHull.v coqc PSpolynomial.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig PSpolynomial.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.eg4sg6rcx1 MINIMIZER_DEBUG: files: PSpolynomial.v coqc CharactPolyn.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig CharactPolyn.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.SrKcXyKPVk MINIMIZER_DEBUG: files: CharactPolyn.v coqc AlgCloCharPol.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig AlgCloCharPol.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.0eMn6ya7mC MINIMIZER_DEBUG: files: AlgCloCharPol.v coqc SplitList.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig SplitList.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.RRvhj5Dg7j MINIMIZER_DEBUG: files: SplitList.v coqc F1Eq.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig F1Eq.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.LQkq75TN4n MINIMIZER_DEBUG: files: F1Eq.v 1 : Q File "./F1Eq.v", line 374, characters 2-10: Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. make: *** [Makefile:20: F1Eq.vo] Error 129 ```
minimizer log ``` Coq version: 8.20.0 compiled with OCaml 4.13.1 First, I will attempt to absolutize relevant [Require]s in /github/workspace/puiseuxth/coq/F1Eq.v, and store the result in /github/workspace/cwd/bug_01.v... getting /github/workspace/puiseuxth/coq/F1Eq.v getting /github/workspace/puiseuxth/coq/F1Eq.glob Now, I will attempt to coq the file, and find the error... Coqing the file (/github/workspace/cwd/bug_01.v)... Running command: "/home/coq/.opam/4.13.1+flambda/bin/coqc.orig" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "F1Eq" "-R" "/tmp/tmprlmlpowj" "" "/tmp/tmprlmlpowj/F1Eq.v" "-q" The timeout for /home/coq/.opam/4.13.1+flambda/bin/coqc.orig has been set to: 3 This file produces the following output when Coq'ed: File "/tmp/tmprlmlpowj/F1Eq.v", line 16, characters 15-29: Error: Cannot find a physical path bound to logical path ConvexHullMisc. I think the error is 'Error: Cannot find a physical path bound to logical path ConvexHullMisc. '. The corresponding regular expression is 'File "[^"]+", line ([0-9]+), characters [0-9-]+:\n(Error:\s+Cannot\s+find\s+a\s+physical\s+path\s+bound\s+to\s+logical\s+path\s+ConvexHullMisc\.)'. Now, I will attempt to find the error message in the log... Moving /github/workspace/cwd/bug_01.v to /github/workspace/cwd/tmp.v... The computed error message was not present in the given error log. ```

If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross). If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.

coqbot-app[bot] commented 3 hours ago

@JasonGross, Error: Could not minimize file /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/puiseuxth/coq/F1Eq.v (full log on GitHub Actions, cc @JasonGross)

build log ``` + (/github/workspace/run-script.sh @ line 47) $ ocamlc -config version: 4.13.1 standard_library_default: /home/coq/.opam/4.13.1+flambda/lib/ocaml standard_library: /home/coq/.opam/4.13.1+flambda/lib/ocaml ccomp_type: cc c_compiler: gcc ocamlc_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlc_cppflags: -D_FILE_OFFSET_BITS=64 ocamlopt_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlopt_cppflags: -D_FILE_OFFSET_BITS=64 bytecomp_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 native_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 bytecomp_c_libraries: -lm -lpthread native_c_libraries: -lm native_pack_linker: ld -r -o ranlib: ranlib architecture: amd64 model: default int_size: 63 word_size: 64 system: linux asm: as asm_cfi_supported: true with_frame_pointers: false ext_exe: ext_obj: .o ext_asm: .s ext_lib: .a ext_dll: .so os_type: Unix default_executable_name: a.out systhread_supported: true host: x86_64-pc-linux-gnu target: x86_64-pc-linux-gnu flambda: true safe_string: true default_safe_string: true flat_float_array: true function_sections: true afl_instrument: false windows_unicode: false supports_shared_libraries: true exec_magic_number: Caml1999X030 cmi_magic_number: Caml1999I030 cmo_magic_number: Caml1999O030 cma_magic_number: Caml1999A030 cmx_magic_number: Caml1999y030 cmxa_magic_number: Caml1999z030 ast_impl_magic_number: Caml1999M030 ast_intf_magic_number: Caml1999N030 cmxs_magic_number: Caml1999D030 cmt_magic_number: Caml1999T030 linear_magic_number: Caml1999L030 + (/github/workspace/run-script.sh @ line 48) $ coqc --config MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --config MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.ImFwKMKnnW MINIMIZER_DEBUG: files: COQLIB=/home/coq/.opam/4.13.1+flambda/lib/coq/ COQCORELIB=/home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core/ DOCDIR=/home/coq/.opam/4.13.1+flambda/share/doc/ OCAMLFIND=/home/coq/.opam/4.13.1+flambda/bin/ocamlfind CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 WARN=-warn-error +a-3 HASNATDYNLINK=true COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax COQ_NATIVE_COMPILER_DEFAULT=no + (/github/workspace/run-script.sh @ line 49) $ coqc --version MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.TIQJbZ57AP MINIMIZER_DEBUG: files: The Coq Proof Assistant, version 8.20.0 compiled with OCaml 4.13.1 + (/github/workspace/run-script.sh @ line 50) $ true + (/github/workspace/run-script.sh @ line 50) $ coqtop MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqtop MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqtop.orig MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.OHjjlbyGCO MINIMIZER_DEBUG: files: Welcome to Coq 8.20.0 Coq < + (/github/workspace/run-script.sh @ line 52) $ source /github/workspace/coqbot.sh ++ (/github/workspace/run-script.sh @ line 2) $ git clone https://github.com/roglo/puiseuxth.git -b coq-8.20.0 Cloning into 'puiseuxth'... ++ (/github/workspace/run-script.sh @ line 3) $ cd puiseuxth/coq ++ (/github/workspace/run-script.sh @ line 4) $ make coqc Misc.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Misc.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.M8g0AhoWkr MINIMIZER_DEBUG: files: Misc.v coqc Slope_base.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Slope_base.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.70KcY7cKfr MINIMIZER_DEBUG: files: Slope_base.v coqc SlopeMisc.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig SlopeMisc.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.eALF5CByVE MINIMIZER_DEBUG: files: SlopeMisc.v coqc QbarM.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig QbarM.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.AKwbyM2ftj MINIMIZER_DEBUG: files: QbarM.v coqc NbarM.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig NbarM.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.prd0umjzTu MINIMIZER_DEBUG: files: NbarM.v coqc Field2.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Field2.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.MJY2Hs8psO MINIMIZER_DEBUG: files: Field2.v coqc Fsummation.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Fsummation.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.WOht7VRsqN MINIMIZER_DEBUG: files: Fsummation.v coqc Fpolynomial.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Fpolynomial.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.MDFOukcVz1 MINIMIZER_DEBUG: files: Fpolynomial.v coqc ConvexHull.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig ConvexHull.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.EmqcNr1uqN MINIMIZER_DEBUG: files: ConvexHull.v coqc Newton.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Newton.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.cnlUG3WSD7 MINIMIZER_DEBUG: files: Newton.v coqc ConvexHullMisc.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig ConvexHullMisc.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.dqcrWPI6zT MINIMIZER_DEBUG: files: ConvexHullMisc.v coqc InSegment.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig InSegment.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.KFk7FqSchk MINIMIZER_DEBUG: files: InSegment.v coqc NotInSegMisc.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig NotInSegMisc.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.qcpxcS7bUC MINIMIZER_DEBUG: files: NotInSegMisc.v coqc NotInSegment.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig NotInSegment.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.KLAJKGHXsF MINIMIZER_DEBUG: files: NotInSegment.v coqc Power_series.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Power_series.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.D7UTWNpv2C MINIMIZER_DEBUG: files: Power_series.v coqc Puiseux_series.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Puiseux_series.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.K6EwqWwykR MINIMIZER_DEBUG: files: Puiseux_series.v coqc Ps_add.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Ps_add.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.dLSCSod6cD MINIMIZER_DEBUG: files: Ps_add.v coqc Ps_add_compat.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Ps_add_compat.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.WJSoKBEy2f MINIMIZER_DEBUG: files: Ps_add_compat.v coqc Ps_mul.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Ps_mul.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.fceLDDZ7rm MINIMIZER_DEBUG: files: Ps_mul.v coqc Ps_div.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Ps_div.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.dcSYMQ4WZQ MINIMIZER_DEBUG: files: Ps_div.v coqc Puiseux_base.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig Puiseux_base.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.9oo17McBXD MINIMIZER_DEBUG: files: Puiseux_base.v coqc PolyConvexHull.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig PolyConvexHull.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.VO4R322GTB MINIMIZER_DEBUG: files: PolyConvexHull.v coqc PSpolynomial.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig PSpolynomial.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.Xa5MdINIz6 MINIMIZER_DEBUG: files: PSpolynomial.v coqc CharactPolyn.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig CharactPolyn.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.u2XX0osDr1 MINIMIZER_DEBUG: files: CharactPolyn.v coqc AlgCloCharPol.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig AlgCloCharPol.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.FgBBTfZDfG MINIMIZER_DEBUG: files: AlgCloCharPol.v coqc SplitList.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig SplitList.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.9RokPEyam5 MINIMIZER_DEBUG: files: SplitList.v coqc F1Eq.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/puiseuxth/coq MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig F1Eq.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.tJbg32ezx7 MINIMIZER_DEBUG: files: F1Eq.v 1 : Q File "./F1Eq.v", line 374, characters 2-10: Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. make: *** [Makefile:20: F1Eq.vo] Error 129 ```
minimizer log ``` Coq version: 8.20.0 compiled with OCaml 4.13.1 First, I will attempt to absolutize relevant [Require]s in /github/workspace/puiseuxth/coq/F1Eq.v, and store the result in /github/workspace/cwd/bug_01.v... getting /github/workspace/puiseuxth/coq/F1Eq.v getting /github/workspace/puiseuxth/coq/F1Eq.glob Now, I will attempt to coq the file, and find the error... Coqing the file (/github/workspace/cwd/bug_01.v)... Running command: "/home/coq/.opam/4.13.1+flambda/bin/coqc.orig" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "F1Eq" "-R" "/tmp/tmpqn5p4vpu" "" "/tmp/tmpqn5p4vpu/F1Eq.v" "-q" The timeout for /home/coq/.opam/4.13.1+flambda/bin/coqc.orig has been set to: 3 This file produces the following output when Coq'ed: File "/tmp/tmpqn5p4vpu/F1Eq.v", line 16, characters 15-29: Error: Cannot find a physical path bound to logical path ConvexHullMisc. I think the error is 'Error: Cannot find a physical path bound to logical path ConvexHullMisc. '. The corresponding regular expression is 'File "[^"]+", line ([0-9]+), characters [0-9-]+:\n(Error:\s+Cannot\s+find\s+a\s+physical\s+path\s+bound\s+to\s+logical\s+path\s+ConvexHullMisc\.)'. Now, I will attempt to find the error message in the log... Moving /github/workspace/cwd/bug_01.v to /github/workspace/cwd/tmp.v... The computed error message was not present in the given error log. ```

If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross). If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.

coqbot-app[bot] commented 3 hours ago

@JasonGross, Error: Could not minimize file /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/foo/bar.v (full log on GitHub Actions, cc @JasonGross)

build log ``` + (/github/workspace/run-script.sh @ line 47) $ ocamlc -config version: 4.13.1 standard_library_default: /home/coq/.opam/4.13.1+flambda/lib/ocaml standard_library: /home/coq/.opam/4.13.1+flambda/lib/ocaml ccomp_type: cc c_compiler: gcc ocamlc_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlc_cppflags: -D_FILE_OFFSET_BITS=64 ocamlopt_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlopt_cppflags: -D_FILE_OFFSET_BITS=64 bytecomp_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 native_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 bytecomp_c_libraries: -lm -lpthread native_c_libraries: -lm native_pack_linker: ld -r -o ranlib: ranlib architecture: amd64 model: default int_size: 63 word_size: 64 system: linux asm: as asm_cfi_supported: true with_frame_pointers: false ext_exe: ext_obj: .o ext_asm: .s ext_lib: .a ext_dll: .so os_type: Unix default_executable_name: a.out systhread_supported: true host: x86_64-pc-linux-gnu target: x86_64-pc-linux-gnu flambda: true safe_string: true default_safe_string: true flat_float_array: true function_sections: true afl_instrument: false windows_unicode: false supports_shared_libraries: true exec_magic_number: Caml1999X030 cmi_magic_number: Caml1999I030 cmo_magic_number: Caml1999O030 cma_magic_number: Caml1999A030 cmx_magic_number: Caml1999y030 cmxa_magic_number: Caml1999z030 ast_impl_magic_number: Caml1999M030 ast_intf_magic_number: Caml1999N030 cmxs_magic_number: Caml1999D030 cmt_magic_number: Caml1999T030 linear_magic_number: Caml1999L030 + (/github/workspace/run-script.sh @ line 48) $ coqc --config MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --config MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.cRzV5PEUNV MINIMIZER_DEBUG: files: COQLIB=/home/coq/.opam/4.13.1+flambda/lib/coq/ COQCORELIB=/home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core/ DOCDIR=/home/coq/.opam/4.13.1+flambda/share/doc/ OCAMLFIND=/home/coq/.opam/4.13.1+flambda/bin/ocamlfind CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 WARN=-warn-error +a-3 HASNATDYNLINK=true COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax COQ_NATIVE_COMPILER_DEFAULT=no + (/github/workspace/run-script.sh @ line 49) $ coqc --version MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.D59lUuRgNp MINIMIZER_DEBUG: files: The Coq Proof Assistant, version 8.20.0 compiled with OCaml 4.13.1 + (/github/workspace/run-script.sh @ line 50) $ true + (/github/workspace/run-script.sh @ line 50) $ coqtop MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqtop MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqtop.orig MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.DnyYESI7oJ MINIMIZER_DEBUG: files: Welcome to Coq 8.20.0 Coq < + (/github/workspace/run-script.sh @ line 52) $ source /github/workspace/coqbot.sh ++ (/github/workspace/run-script.sh @ line 2) $ mkdir foo ++ (/github/workspace/run-script.sh @ line 3) $ cd foo ++ (/github/workspace/run-script.sh @ line 4) $ echo 'Axiom A : Set.' ++ (/github/workspace/run-script.sh @ line 5) $ echo 'Require Import foo. Fail Check A.' ++ (/github/workspace/run-script.sh @ line 6) $ coqc -q foo.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/foo MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q foo.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.uy6L4gbwRM MINIMIZER_DEBUG: files: foo.v ++ (/github/workspace/run-script.sh @ line 7) $ coqc -q bar.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/foo MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q bar.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.JL5YbI3qG7 MINIMIZER_DEBUG: files: bar.v A : Set File "./bar.v", line 1, characters 21-34: Error: The command has not failed! ```
minimizer log ``` Coq version: 8.20.0 compiled with OCaml 4.13.1 First, I will attempt to absolutize relevant [Require]s in /github/workspace/foo/bar.v, and store the result in /github/workspace/cwd/bug_01.v... getting /github/workspace/foo/bar.v NOTE: The file /github/workspace/foo/bar.v is very new (1726879816, 0 seconds old), delaying until it's a bit older getting /github/workspace/foo/bar.glob Now, I will attempt to coq the file, and find the error... Coqing the file (/github/workspace/cwd/bug_01.v)... Running command: "/home/coq/.opam/4.13.1+flambda/bin/coqc.orig" "-q" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "bar" "-R" "/tmp/tmp8_s0t3wq" "" "/tmp/tmp8_s0t3wq/bar.v" "-q" The timeout for /home/coq/.opam/4.13.1+flambda/bin/coqc.orig has been set to: 3 This file produces the following output when Coq'ed: File "/tmp/tmp8_s0t3wq/bar.v", line 10, characters 15-18: Error: Cannot find a physical path bound to logical path foo. I think the error is 'Error: Cannot find a physical path bound to logical path foo. '. The corresponding regular expression is 'File "[^"]+", line ([0-9]+), characters [0-9-]+:\n(Error:\s+Cannot\s+find\s+a\s+physical\s+path\s+bound\s+to\s+logical\s+path\s+foo\.)'. Now, I will attempt to find the error message in the log... Moving /github/workspace/cwd/bug_01.v to /github/workspace/cwd/tmp.v... The computed error message was not present in the given error log. ```

If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross). If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.

coqbot-app[bot] commented 3 hours ago

@JasonGross, Error: Could not minimize file /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/foo/bar.v (full log on GitHub Actions, cc @JasonGross)

build log ``` + (/github/workspace/run-script.sh @ line 47) $ ocamlc -config version: 4.13.1 standard_library_default: /home/coq/.opam/4.13.1+flambda/lib/ocaml standard_library: /home/coq/.opam/4.13.1+flambda/lib/ocaml ccomp_type: cc c_compiler: gcc ocamlc_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlc_cppflags: -D_FILE_OFFSET_BITS=64 ocamlopt_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlopt_cppflags: -D_FILE_OFFSET_BITS=64 bytecomp_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 native_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 bytecomp_c_libraries: -lm -lpthread native_c_libraries: -lm native_pack_linker: ld -r -o ranlib: ranlib architecture: amd64 model: default int_size: 63 word_size: 64 system: linux asm: as asm_cfi_supported: true with_frame_pointers: false ext_exe: ext_obj: .o ext_asm: .s ext_lib: .a ext_dll: .so os_type: Unix default_executable_name: a.out systhread_supported: true host: x86_64-pc-linux-gnu target: x86_64-pc-linux-gnu flambda: true safe_string: true default_safe_string: true flat_float_array: true function_sections: true afl_instrument: false windows_unicode: false supports_shared_libraries: true exec_magic_number: Caml1999X030 cmi_magic_number: Caml1999I030 cmo_magic_number: Caml1999O030 cma_magic_number: Caml1999A030 cmx_magic_number: Caml1999y030 cmxa_magic_number: Caml1999z030 ast_impl_magic_number: Caml1999M030 ast_intf_magic_number: Caml1999N030 cmxs_magic_number: Caml1999D030 cmt_magic_number: Caml1999T030 linear_magic_number: Caml1999L030 + (/github/workspace/run-script.sh @ line 48) $ coqc --config MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --config MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.bLx0TFuDbW MINIMIZER_DEBUG: files: COQLIB=/home/coq/.opam/4.13.1+flambda/lib/coq/ COQCORELIB=/home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core/ DOCDIR=/home/coq/.opam/4.13.1+flambda/share/doc/ OCAMLFIND=/home/coq/.opam/4.13.1+flambda/bin/ocamlfind CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 WARN=-warn-error +a-3 HASNATDYNLINK=true COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax COQ_NATIVE_COMPILER_DEFAULT=no + (/github/workspace/run-script.sh @ line 49) $ coqc --version MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.cUPDY7llcp MINIMIZER_DEBUG: files: The Coq Proof Assistant, version 8.20.0 compiled with OCaml 4.13.1 + (/github/workspace/run-script.sh @ line 50) $ true + (/github/workspace/run-script.sh @ line 50) $ coqtop MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqtop MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqtop.orig MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.xW9XXKrOyM MINIMIZER_DEBUG: files: Welcome to Coq 8.20.0 Coq < + (/github/workspace/run-script.sh @ line 52) $ source /github/workspace/coqbot.sh ++ (/github/workspace/run-script.sh @ line 2) $ mkdir foo ++ (/github/workspace/run-script.sh @ line 3) $ cd foo ++ (/github/workspace/run-script.sh @ line 4) $ echo 'Axiom A : Set.' ++ (/github/workspace/run-script.sh @ line 5) $ echo 'Require Import foo. Fail Check A.' ++ (/github/workspace/run-script.sh @ line 6) $ coqc -q foo.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/foo MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q foo.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.uojgGVx9hA MINIMIZER_DEBUG: files: foo.v ++ (/github/workspace/run-script.sh @ line 7) $ coqc -q bar.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/foo MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q bar.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.9FmOtXfVwi MINIMIZER_DEBUG: files: bar.v A : Set File "./bar.v", line 1, characters 21-34: Error: The command has not failed! ```
minimizer log ``` Coq version: 8.20.0 compiled with OCaml 4.13.1 First, I will attempt to absolutize relevant [Require]s in /github/workspace/foo/bar.v, and store the result in /github/workspace/cwd/bug_01.v... getting /github/workspace/foo/bar.v NOTE: The file /github/workspace/foo/bar.v is very new (1726879819, 0 seconds old), delaying until it's a bit older getting /github/workspace/foo/bar.glob Now, I will attempt to coq the file, and find the error... Coqing the file (/github/workspace/cwd/bug_01.v)... Running command: "/home/coq/.opam/4.13.1+flambda/bin/coqc.orig" "-q" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "bar" "-R" "/tmp/tmpjdbkan8f" "" "/tmp/tmpjdbkan8f/bar.v" "-q" The timeout for /home/coq/.opam/4.13.1+flambda/bin/coqc.orig has been set to: 3 This file produces the following output when Coq'ed: File "/tmp/tmpjdbkan8f/bar.v", line 10, characters 15-18: Error: Cannot find a physical path bound to logical path foo. I think the error is 'Error: Cannot find a physical path bound to logical path foo. '. The corresponding regular expression is 'File "[^"]+", line ([0-9]+), characters [0-9-]+:\n(Error:\s+Cannot\s+find\s+a\s+physical\s+path\s+bound\s+to\s+logical\s+path\s+foo\.)'. Now, I will attempt to find the error message in the log... Moving /github/workspace/cwd/bug_01.v to /github/workspace/cwd/tmp.v... The computed error message was not present in the given error log. ```

If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross). If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.

JasonGross commented 3 hours ago

Let's check if this was fixed by #35 @coqbot: minimize

#!/usr/bin/env bash
mkdir foo
cd foo
echo 'Axiom A : Set.' > foo.v
echo 'Require Import foo.  Fail Check A.' > bar.v
coqc -q foo.v
coqc -q bar.v
coqbot-app[bot] commented 3 hours ago

Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.

coqbot-app[bot] commented 3 hours ago

@JasonGross, Error: Could not minimize file /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/foo/bar.v (full log on GitHub Actions, cc @JasonGross)

build log ``` + (/github/workspace/run-script.sh @ line 47) $ ocamlc -config version: 4.13.1 standard_library_default: /home/coq/.opam/4.13.1+flambda/lib/ocaml standard_library: /home/coq/.opam/4.13.1+flambda/lib/ocaml ccomp_type: cc c_compiler: gcc ocamlc_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlc_cppflags: -D_FILE_OFFSET_BITS=64 ocamlopt_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlopt_cppflags: -D_FILE_OFFSET_BITS=64 bytecomp_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 native_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 bytecomp_c_libraries: -lm -lpthread native_c_libraries: -lm native_pack_linker: ld -r -o ranlib: ranlib architecture: amd64 model: default int_size: 63 word_size: 64 system: linux asm: as asm_cfi_supported: true with_frame_pointers: false ext_exe: ext_obj: .o ext_asm: .s ext_lib: .a ext_dll: .so os_type: Unix default_executable_name: a.out systhread_supported: true host: x86_64-pc-linux-gnu target: x86_64-pc-linux-gnu flambda: true safe_string: true default_safe_string: true flat_float_array: true function_sections: true afl_instrument: false windows_unicode: false supports_shared_libraries: true exec_magic_number: Caml1999X030 cmi_magic_number: Caml1999I030 cmo_magic_number: Caml1999O030 cma_magic_number: Caml1999A030 cmx_magic_number: Caml1999y030 cmxa_magic_number: Caml1999z030 ast_impl_magic_number: Caml1999M030 ast_intf_magic_number: Caml1999N030 cmxs_magic_number: Caml1999D030 cmt_magic_number: Caml1999T030 linear_magic_number: Caml1999L030 + (/github/workspace/run-script.sh @ line 48) $ coqc --config MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --config MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.goBoiIQABH MINIMIZER_DEBUG: files: COQLIB=/home/coq/.opam/4.13.1+flambda/lib/coq/ COQCORELIB=/home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core/ DOCDIR=/home/coq/.opam/4.13.1+flambda/share/doc/ OCAMLFIND=/home/coq/.opam/4.13.1+flambda/bin/ocamlfind CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 WARN=-warn-error +a-3 HASNATDYNLINK=true COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax COQ_NATIVE_COMPILER_DEFAULT=no + (/github/workspace/run-script.sh @ line 49) $ coqc --version MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.iTl6gBxDpb MINIMIZER_DEBUG: files: The Coq Proof Assistant, version 8.20.0 compiled with OCaml 4.13.1 + (/github/workspace/run-script.sh @ line 50) $ true + (/github/workspace/run-script.sh @ line 50) $ coqtop MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqtop MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqtop.orig MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.HJkE1Aq52S MINIMIZER_DEBUG: files: Welcome to Coq 8.20.0 Coq < + (/github/workspace/run-script.sh @ line 52) $ source /github/workspace/coqbot.sh ++ (/github/workspace/run-script.sh @ line 2) $ mkdir foo ++ (/github/workspace/run-script.sh @ line 3) $ cd foo ++ (/github/workspace/run-script.sh @ line 4) $ echo 'Axiom A : Set.' ++ (/github/workspace/run-script.sh @ line 5) $ echo 'Require Import foo. Fail Check A.' ++ (/github/workspace/run-script.sh @ line 6) $ coqc -q foo.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/foo MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q foo.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.WM30ghVVFp MINIMIZER_DEBUG: files: foo.v ++ (/github/workspace/run-script.sh @ line 7) $ coqc -q bar.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/foo MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q bar.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.kiO2TFF808 MINIMIZER_DEBUG: files: bar.v A : Set File "./bar.v", line 1, characters 21-34: Error: The command has not failed! ```
minimizer log ``` Coq version: 8.20.0 compiled with OCaml 4.13.1 First, I will attempt to absolutize relevant [Require]s in /github/workspace/foo/bar.v, and store the result in /github/workspace/cwd/bug_01.v... getting /github/workspace/foo/bar.v NOTE: The file /github/workspace/foo/bar.v is very new (1726880323, 0 seconds old), delaying until it's a bit older getting /github/workspace/foo/bar.glob Now, I will attempt to coq the file, and find the error... Coqing the file (/github/workspace/cwd/bug_01.v)... Running command: "/home/coq/.opam/4.13.1+flambda/bin/coqc.orig" "-q" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "bar" "-R" "/tmp/tmplzxmi57i" "" "/tmp/tmplzxmi57i/bar.v" "-q" The timeout for /home/coq/.opam/4.13.1+flambda/bin/coqc.orig has been set to: 3 This file produces the following output when Coq'ed: File "/tmp/tmplzxmi57i/bar.v", line 10, characters 15-18: Error: Cannot find a physical path bound to logical path foo. I think the error is 'Error: Cannot find a physical path bound to logical path foo. '. The corresponding regular expression is 'File "[^"]+", line ([0-9]+), characters [0-9-]+:\n(Error:\s+Cannot\s+find\s+a\s+physical\s+path\s+bound\s+to\s+logical\s+path\s+foo\.)'. Now, I will attempt to find the error message in the log... Moving /github/workspace/cwd/bug_01.v to /github/workspace/cwd/tmp.v... The computed error message was not present in the given error log. ```

If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross). If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.

JasonGross commented 3 hours ago

Needs more work