Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Minimizer fails when coqc loads from the pwd implicitly #36

Open
JasonGross opened this issue Sep 21, 2024 · 19 comments
Open

Minimizer fails when coqc loads from the pwd implicitly #36

JasonGross opened this issue Sep 21, 2024 · 19 comments

Comments

@JasonGross
Copy link
Member

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

Originally posted by @JasonGross in coq/coq#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 coqbot-app
Copy link

coqbot-app bot commented Sep 21, 2024

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

1 similar comment
@coqbot-app coqbot-app
Copy link

coqbot-app bot commented Sep 21, 2024

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

@JasonGross
Copy link
Member Author

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 coqbot-app
Copy link

coqbot-app bot commented Sep 21, 2024

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

1 similar comment
@coqbot-app coqbot-app
Copy link

coqbot-app bot commented Sep 21, 2024

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 coqbot-app
Copy link

coqbot-app bot commented Sep 21, 2024

@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 coqbot-app
Copy link

coqbot-app bot commented Sep 21, 2024

@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 coqbot-app
Copy link

coqbot-app bot commented Sep 21, 2024

@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 coqbot-app
Copy link

coqbot-app bot commented Sep 21, 2024

@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
Copy link
Member Author

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 coqbot-app
Copy link

coqbot-app bot commented Sep 21, 2024

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 coqbot-app
Copy link

coqbot-app bot commented Sep 21, 2024

@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
Copy link
Member Author

Needs more work

@JasonGross
Copy link
Member Author

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 coqbot-app
Copy link

coqbot-app bot commented Sep 21, 2024

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 coqbot-app
Copy link

coqbot-app bot commented Sep 21, 2024

@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.XoSpy6pCjY
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.0n1ZjiQMxR
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.GEyhiPJNfO
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.qYQyZydR1w
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.BGnEDbEa4v
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 (1726917923, 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/tmplhz6xepj" "" "/tmp/tmplhz6xepj/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/tmplhz6xepj/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
Copy link
Member Author

@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 coqbot-app
Copy link

coqbot-app bot commented Sep 22, 2024

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 coqbot-app
Copy link

coqbot-app bot commented Sep 22, 2024

@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.8AcBOJOuJI
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.lB5NuVYfIl
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.EjotgNzc18
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.7huOEqpRN9
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.NKRQETg3ir
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 (1726980976, 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/tmpysb68xgm" "" "/tmp/tmpysb68xgm/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/tmpysb68xgm/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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@JasonGross