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]

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]

@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

+ �[33;1m(/github/workspace/run-script.sh @ line 47) $�[0m 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
+ �[33;1m(/github/workspace/run-script.sh @ line 48) $�[0m 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
+ �[33;1m(/github/workspace/run-script.sh @ line 49) $�[0m 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
+ �[33;1m(/github/workspace/run-script.sh @ line 50) $�[0m true
+ �[33;1m(/github/workspace/run-script.sh @ line 50) $�[0m 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 < 
+ �[33;1m(/github/workspace/run-script.sh @ line 52) $�[0m source /github/workspace/coqbot.sh
++ �[33;1m(/github/workspace/run-script.sh @ line 2) $�[0m mkdir foo
++ �[33;1m(/github/workspace/run-script.sh @ line 3) $�[0m cd foo
++ �[33;1m(/github/workspace/run-script.sh @ line 4) $�[0m echo 'Axiom A : Set.'
++ �[33;1m(/github/workspace/run-script.sh @ line 5) $�[0m echo 'Require Import foo.  Fail Check A.'
++ �[33;1m(/github/workspace/run-script.sh @ line 6) $�[0m 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
++ �[33;1m(/github/workspace/run-script.sh @ line 7) $�[0m 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