Minimizer fails when coqc loads from the pwd implicitly

[JasonGross]

I guess the runner fails when coqc is loading files from pwd implicitly. That might be fixed by #35

Originally posted by @JasonGross in rocq-prover/rocq#19587 (comment)

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

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]

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

[JasonGross]

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]

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]

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/puiseuxth/coq/F1Eq.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.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
+ �[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.4J3YvbMwzy
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.ZsmKoaeTJy
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 git clone https://github.com/roglo/puiseuxth.git -b coq-8.20.0
Cloning into 'puiseuxth'...
++ �[33;1m(/github/workspace/run-script.sh @ line 3) $�[0m cd puiseuxth/coq
++ �[33;1m(/github/workspace/run-script.sh @ line 4) $�[0m 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]

@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

+ �[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.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
+ �[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.TIQJbZ57AP
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.OHjjlbyGCO
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 git clone https://github.com/roglo/puiseuxth.git -b coq-8.20.0
Cloning into 'puiseuxth'...
++ �[33;1m(/github/workspace/run-script.sh @ line 3) $�[0m cd puiseuxth/coq
++ �[33;1m(/github/workspace/run-script.sh @ line 4) $�[0m 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]

@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.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
+ �[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.D59lUuRgNp
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.DnyYESI7oJ
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.uy6L4gbwRM
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.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]

@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.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
+ �[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.cUPDY7llcp
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.xW9XXKrOyM
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.uojgGVx9hA
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.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]

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]

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.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
+ �[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.iTl6gBxDpb
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.HJkE1Aq52S
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.WM30ghVVFp
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.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]

Needs more work

[JasonGross]

Let's look at the log after JasonGross/coq-tools#222
@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.