bug minimizer does not correctly handle the implicit binding of `""` to the current directory

[JasonGross]

I'm also not sure it matches Coq's behavior on how it binds the current directory at all / uses Top.

@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]]

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]]

@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.ApeVtwN7of 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.twEEp3t9gP 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.u6IAJd7UBG 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.Hm5QhZO9es 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.v9jmGsyCbo 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 (1726983590, 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/tmpd7ib64__" "" "/tmp/tmpd7ib64__/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/tmpd7ib64__/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]

Probably the right thing to do here is to rip out the existing lib<->filename logic and just parse the output of echo 'Print LoadPath.' | coqtop