search

coq-community / run-coq-bug-minimizer

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

argument parsing loses the final argument when it is the empty string #37

Closed JasonGross closed 1 month ago

JasonGross commented 1 month ago

@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 -Q . "" bar.v
coqbot-app[bot] commented 1 month ago

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

coqbot-app[bot] commented 1 month ago

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

build log ``` + (/github/workspace/run-script.sh @ line 47) $ ocamlc -config version: 4.13.1 standard_library_default: /home/coq/.opam/4.13.1+flambda/lib/ocaml standard_library: /home/coq/.opam/4.13.1+flambda/lib/ocaml ccomp_type: cc c_compiler: gcc ocamlc_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlc_cppflags: -D_FILE_OFFSET_BITS=64 ocamlopt_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlopt_cppflags: -D_FILE_OFFSET_BITS=64 bytecomp_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 native_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 bytecomp_c_libraries: -lm -lpthread native_c_libraries: -lm native_pack_linker: ld -r -o ranlib: ranlib architecture: amd64 model: default int_size: 63 word_size: 64 system: linux asm: as asm_cfi_supported: true with_frame_pointers: false ext_exe: ext_obj: .o ext_asm: .s ext_lib: .a ext_dll: .so os_type: Unix default_executable_name: a.out systhread_supported: true host: x86_64-pc-linux-gnu target: x86_64-pc-linux-gnu flambda: true safe_string: true default_safe_string: true flat_float_array: true function_sections: true afl_instrument: false windows_unicode: false supports_shared_libraries: true exec_magic_number: Caml1999X030 cmi_magic_number: Caml1999I030 cmo_magic_number: Caml1999O030 cma_magic_number: Caml1999A030 cmx_magic_number: Caml1999y030 cmxa_magic_number: Caml1999z030 ast_impl_magic_number: Caml1999M030 ast_intf_magic_number: Caml1999N030 cmxs_magic_number: Caml1999D030 cmt_magic_number: Caml1999T030 linear_magic_number: Caml1999L030 + (/github/workspace/run-script.sh @ line 48) $ coqc --config MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --config MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.36R2yTyNZt MINIMIZER_DEBUG: files: COQLIB=/home/coq/.opam/4.13.1+flambda/lib/coq/ COQCORELIB=/home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core/ DOCDIR=/home/coq/.opam/4.13.1+flambda/share/doc/ OCAMLFIND=/home/coq/.opam/4.13.1+flambda/bin/ocamlfind CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 WARN=-warn-error +a-3 HASNATDYNLINK=true COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax COQ_NATIVE_COMPILER_DEFAULT=no + (/github/workspace/run-script.sh @ line 49) $ coqc --version MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.lr62YpORNb MINIMIZER_DEBUG: files: The Coq Proof Assistant, version 8.20.0 compiled with OCaml 4.13.1 + (/github/workspace/run-script.sh @ line 50) $ true + (/github/workspace/run-script.sh @ line 50) $ coqtop MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqtop MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqtop.orig MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.4x7Rg8Vozt MINIMIZER_DEBUG: files: Welcome to Coq 8.20.0 Coq < + (/github/workspace/run-script.sh @ line 52) $ source /github/workspace/coqbot.sh ++ (/github/workspace/run-script.sh @ line 2) $ mkdir foo ++ (/github/workspace/run-script.sh @ line 3) $ cd foo ++ (/github/workspace/run-script.sh @ line 4) $ echo 'Axiom A : Set.' ++ (/github/workspace/run-script.sh @ line 5) $ echo 'Require Import foo. Fail Check A.' ++ (/github/workspace/run-script.sh @ line 6) $ coqc -q foo.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/foo MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q foo.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.56Pmn04zIv MINIMIZER_DEBUG: files: foo.v ++ (/github/workspace/run-script.sh @ line 7) $ coqc -q -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 -Q /github/workspace/foo '' bar.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.Bfjh0lS8Pr MINIMIZER_DEBUG: files: bar.v A : Set File "./bar.v", line 1, characters 21-34: Error: The command has not failed! ```
minimizer log ``` ```

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

JasonGross commented 1 month ago

@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 -Q . "" bar.v
coqbot-app[bot] commented 1 month ago

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

JasonGross commented 1 month ago

@coqbot: minimize

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

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

coqbot-app[bot] commented 1 month ago

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

build log ``` + (/github/workspace/run-script.sh @ line 47) $ ocamlc -config version: 4.13.1 standard_library_default: /home/coq/.opam/4.13.1+flambda/lib/ocaml standard_library: /home/coq/.opam/4.13.1+flambda/lib/ocaml ccomp_type: cc c_compiler: gcc ocamlc_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlc_cppflags: -D_FILE_OFFSET_BITS=64 ocamlopt_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlopt_cppflags: -D_FILE_OFFSET_BITS=64 bytecomp_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 native_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 bytecomp_c_libraries: -lm -lpthread native_c_libraries: -lm native_pack_linker: ld -r -o ranlib: ranlib architecture: amd64 model: default int_size: 63 word_size: 64 system: linux asm: as asm_cfi_supported: true with_frame_pointers: false ext_exe: ext_obj: .o ext_asm: .s ext_lib: .a ext_dll: .so os_type: Unix default_executable_name: a.out systhread_supported: true host: x86_64-pc-linux-gnu target: x86_64-pc-linux-gnu flambda: true safe_string: true default_safe_string: true flat_float_array: true function_sections: true afl_instrument: false windows_unicode: false supports_shared_libraries: true exec_magic_number: Caml1999X030 cmi_magic_number: Caml1999I030 cmo_magic_number: Caml1999O030 cma_magic_number: Caml1999A030 cmx_magic_number: Caml1999y030 cmxa_magic_number: Caml1999z030 ast_impl_magic_number: Caml1999M030 ast_intf_magic_number: Caml1999N030 cmxs_magic_number: Caml1999D030 cmt_magic_number: Caml1999T030 linear_magic_number: Caml1999L030 + (/github/workspace/run-script.sh @ line 48) $ coqc --config MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --config MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.YbvTR8DZir MINIMIZER_DEBUG: files: COQLIB=/home/coq/.opam/4.13.1+flambda/lib/coq/ COQCORELIB=/home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core/ DOCDIR=/home/coq/.opam/4.13.1+flambda/share/doc/ OCAMLFIND=/home/coq/.opam/4.13.1+flambda/bin/ocamlfind CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 WARN=-warn-error +a-3 HASNATDYNLINK=true COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax COQ_NATIVE_COMPILER_DEFAULT=no + (/github/workspace/run-script.sh @ line 49) $ coqc --version MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.Fy0K3Kpusu MINIMIZER_DEBUG: files: The Coq Proof Assistant, version 8.20.0 compiled with OCaml 4.13.1 + (/github/workspace/run-script.sh @ line 50) $ true + (/github/workspace/run-script.sh @ line 50) $ coqtop MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqtop MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqtop.orig MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.sZ39XfCF5U MINIMIZER_DEBUG: files: Welcome to Coq 8.20.0 Coq < + (/github/workspace/run-script.sh @ line 52) $ source /github/workspace/coqbot.sh ++ (/github/workspace/run-script.sh @ line 2) $ mkdir foo ++ (/github/workspace/run-script.sh @ line 3) $ cd foo ++ (/github/workspace/run-script.sh @ line 4) $ echo 'Axiom A : Set.' ++ (/github/workspace/run-script.sh @ line 5) $ echo 'Require Import foo. Fail Check A.' ++ (/github/workspace/run-script.sh @ line 6) $ coqc -q foo.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/foo MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q foo.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.B5v9lU39MI MINIMIZER_DEBUG: files: foo.v ++ (/github/workspace/run-script.sh @ line 7) $ coqc -q -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 -Q /github/workspace/foo '' bar.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.FNfOZcJGTD MINIMIZER_DEBUG: files: bar.v A : Set File "./bar.v", line 1, characters 21-34: Error: The command has not failed! ```
minimizer log ``` ```

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

coqbot-app[bot] commented 1 month ago

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

build log ``` + (/github/workspace/run-script.sh @ line 47) $ ocamlc -config version: 4.13.1 standard_library_default: /home/coq/.opam/4.13.1+flambda/lib/ocaml standard_library: /home/coq/.opam/4.13.1+flambda/lib/ocaml ccomp_type: cc c_compiler: gcc ocamlc_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlc_cppflags: -D_FILE_OFFSET_BITS=64 ocamlopt_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlopt_cppflags: -D_FILE_OFFSET_BITS=64 bytecomp_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 native_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 bytecomp_c_libraries: -lm -lpthread native_c_libraries: -lm native_pack_linker: ld -r -o ranlib: ranlib architecture: amd64 model: default int_size: 63 word_size: 64 system: linux asm: as asm_cfi_supported: true with_frame_pointers: false ext_exe: ext_obj: .o ext_asm: .s ext_lib: .a ext_dll: .so os_type: Unix default_executable_name: a.out systhread_supported: true host: x86_64-pc-linux-gnu target: x86_64-pc-linux-gnu flambda: true safe_string: true default_safe_string: true flat_float_array: true function_sections: true afl_instrument: false windows_unicode: false supports_shared_libraries: true exec_magic_number: Caml1999X030 cmi_magic_number: Caml1999I030 cmo_magic_number: Caml1999O030 cma_magic_number: Caml1999A030 cmx_magic_number: Caml1999y030 cmxa_magic_number: Caml1999z030 ast_impl_magic_number: Caml1999M030 ast_intf_magic_number: Caml1999N030 cmxs_magic_number: Caml1999D030 cmt_magic_number: Caml1999T030 linear_magic_number: Caml1999L030 + (/github/workspace/run-script.sh @ line 48) $ coqc --config MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --config MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.y6LaFt0QBm MINIMIZER_DEBUG: files: COQLIB=/home/coq/.opam/4.13.1+flambda/lib/coq/ COQCORELIB=/home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core/ DOCDIR=/home/coq/.opam/4.13.1+flambda/share/doc/ OCAMLFIND=/home/coq/.opam/4.13.1+flambda/bin/ocamlfind CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 WARN=-warn-error +a-3 HASNATDYNLINK=true COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax COQ_NATIVE_COMPILER_DEFAULT=no + (/github/workspace/run-script.sh @ line 49) $ coqc --version MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.ehxNfyQu4Z MINIMIZER_DEBUG: files: The Coq Proof Assistant, version 8.20.0 compiled with OCaml 4.13.1 + (/github/workspace/run-script.sh @ line 50) $ true + (/github/workspace/run-script.sh @ line 50) $ coqtop MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqtop MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqtop.orig MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.417CktKaKe MINIMIZER_DEBUG: files: Welcome to Coq 8.20.0 Coq < + (/github/workspace/run-script.sh @ line 52) $ source /github/workspace/coqbot.sh ++ (/github/workspace/run-script.sh @ line 2) $ mkdir -p foo/bar ++ (/github/workspace/run-script.sh @ line 3) $ cd foo ++ (/github/workspace/run-script.sh @ line 4) $ echo 'Axiom A : Set.' ++ (/github/workspace/run-script.sh @ line 5) $ echo 'Require Import foo. Fail Check A.' ++ (/github/workspace/run-script.sh @ line 6) $ coqc -q -Q bar '' bar/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 -Q /github/workspace/foo/bar '' bar/foo.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.ZweOwmmIZW MINIMIZER_DEBUG: files: bar/foo.v ++ (/github/workspace/run-script.sh @ line 7) $ coqc -q -Q bar '' bar/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 -Q /github/workspace/foo/bar '' bar/bar.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.xv4PGDV6cz MINIMIZER_DEBUG: files: bar/bar.v A : Set File "./bar/bar.v", line 1, characters 21-34: Error: The command has not failed! ```
minimizer log ``` ```

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

JasonGross commented 1 month ago

@coqbot: minimize

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

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

coqbot-app[bot] commented 1 month ago

@JasonGross, Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/foo/bar/bar.v (full log on GitHub Actions - verbose log)

:star2: Minimized Coq File (consider adding this file to the test-suite) ```coq (* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/foo/bar" "" "-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") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 16 lines to 5 lines, then from 18 lines to 26 lines, then from 31 lines to 4 lines, then from 9 lines to 5 lines *) (* coqc version 8.20.0 compiled with OCaml 4.13.1 coqtop version 8.20.0 Expected coqc runtime on this file: 0.086 sec *) Axiom A : Set. Fail Check A. ```
:hammer_and_wrench: Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted) ```coq ```
:hammer_and_wrench: :scroll: Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted) ```coq ```
:scroll: Build Log (contains the Coq error message) ``` + (/github/workspace/run-script.sh @ line 47) $ ocamlc -config version: 4.13.1 standard_library_default: /home/coq/.opam/4.13.1+flambda/lib/ocaml standard_library: /home/coq/.opam/4.13.1+flambda/lib/ocaml ccomp_type: cc c_compiler: gcc ocamlc_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlc_cppflags: -D_FILE_OFFSET_BITS=64 ocamlopt_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlopt_cppflags: -D_FILE_OFFSET_BITS=64 bytecomp_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 native_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 bytecomp_c_libraries: -lm -lpthread native_c_libraries: -lm native_pack_linker: ld -r -o ranlib: ranlib architecture: amd64 model: default int_size: 63 word_size: 64 system: linux asm: as asm_cfi_supported: true with_frame_pointers: false ext_exe: ext_obj: .o ext_asm: .s ext_lib: .a ext_dll: .so os_type: Unix default_executable_name: a.out systhread_supported: true host: x86_64-pc-linux-gnu target: x86_64-pc-linux-gnu flambda: true safe_string: true default_safe_string: true flat_float_array: true function_sections: true afl_instrument: false windows_unicode: false supports_shared_libraries: true exec_magic_number: Caml1999X030 cmi_magic_number: Caml1999I030 cmo_magic_number: Caml1999O030 cma_magic_number: Caml1999A030 cmx_magic_number: Caml1999y030 cmxa_magic_number: Caml1999z030 ast_impl_magic_number: Caml1999M030 ast_intf_magic_number: Caml1999N030 cmxs_magic_number: Caml1999D030 cmt_magic_number: Caml1999T030 linear_magic_number: Caml1999L030 + (/github/workspace/run-script.sh @ line 48) $ coqc --config MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --config MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.rjsF95UFRT MINIMIZER_DEBUG: files: COQLIB=/home/coq/.opam/4.13.1+flambda/lib/coq/ COQCORELIB=/home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core/ DOCDIR=/home/coq/.opam/4.13.1+flambda/share/doc/ OCAMLFIND=/home/coq/.opam/4.13.1+flambda/bin/ocamlfind CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 WARN=-warn-error +a-3 HASNATDYNLINK=true COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax COQ_NATIVE_COMPILER_DEFAULT=no + (/github/workspace/run-script.sh @ line 49) $ coqc --version MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.IpcU1cucGI MINIMIZER_DEBUG: files: The Coq Proof Assistant, version 8.20.0 compiled with OCaml 4.13.1 + (/github/workspace/run-script.sh @ line 50) $ true + (/github/workspace/run-script.sh @ line 50) $ coqtop MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqtop MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqtop.orig MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.G3jIevHm7U MINIMIZER_DEBUG: files: Welcome to Coq 8.20.0 Coq < + (/github/workspace/run-script.sh @ line 52) $ source /github/workspace/coqbot.sh ++ (/github/workspace/run-script.sh @ line 2) $ mkdir -p foo/bar ++ (/github/workspace/run-script.sh @ line 3) $ cd foo ++ (/github/workspace/run-script.sh @ line 4) $ echo 'Axiom A : Set.' ++ (/github/workspace/run-script.sh @ line 5) $ echo 'Require Import foo. Fail Check A.' ++ (/github/workspace/run-script.sh @ line 6) $ coqc -q -Q bar '' bar/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 -Q /github/workspace/foo/bar '' bar/foo.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.Iax81scBnb MINIMIZER_DEBUG: files: bar/foo.v ++ (/github/workspace/run-script.sh @ line 7) $ coqc -q -Q bar '' bar/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 -Q /github/workspace/foo/bar '' bar/bar.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.DHJBA9eNWD MINIMIZER_DEBUG: files: bar/bar.v A : Set File "./bar/bar.v", line 1, characters 21-34: Error: The command has not failed! ```
:scroll: :mag_right: Minimization Log (truncated to last 8.0KiB; full 39KiB file on GitHub Actions Artifacts under bug.log) ``` -compiler ondemand -Q /github/workspace/cwd Top -Q /github/workspace/foo/bar -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 -o /tmp/bug_01.vo -dump-glob bug_01.glob bug_01.v  Sanity check passed. Now, I will attempt to strip repeated newlines and trailing spaces from this file... No strippable newlines or spaces. Now, I will attempt to strip the comments from this file...  Succeeded in stripping comments. Now, I will attempt to factor out all of the [Require]s... getting bug_01.v (/github/workspace/cwd/bug_01.v) NOTE: The file bug_01.v is very new (1726917521, 0 seconds old), delaying until it's a bit older /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -Q /github/workspace/cwd Top -Q /github/workspace/foo/bar "" -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 -q -w -deprecated-native-compiler-option,-native-compiler-disabled -native-compiler ondemand -Q /github/workspace/cwd Top -Q /github/workspace/foo/bar -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 -o /tmp/bug_01.vo -dump-glob bug_01.glob bug_01.v /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -Q /github/workspace/cwd Top -Q /github/workspace/foo/bar "" -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 -q -w -deprecated-native-compiler-option,-native-compiler-disabled -native-compiler ondemand -Q /github/workspace/cwd Top -Q /github/workspace/foo/bar -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 -o /tmp/bug_01.vo -dump-glob bug_01.glob bug_01.v /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -Q /github/workspace/cwd Top -Q /github/workspace/foo/bar "" -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 -q -w -deprecated-native-compiler-option,-native-compiler-disabled -native-compiler ondemand -Q /github/workspace/cwd Top -Q /github/workspace/foo/bar -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 -o /tmp/bug_01.vo -dump-glob bug_01.glob bug_01.v  Succeeded in normalizing Requires. Now, I will attempt to split up [Require] statements... getting /github/workspace/cwd/bug_01.v NOTE: The file /github/workspace/cwd/bug_01.v is very new (1726917524, 0 seconds old), delaying until it's a bit older getting /github/workspace/cwd/bug_01.glob getting /github/workspace/cwd/bug_01.glob No Requires to split. In order to efficiently manipulate the file, I have to break it into statements. I will attempt to do this by matching on periods.  Splitting successful. I will now attempt to remove any lines after the line which generates the error.  Trimming successful. We removed all lines after 9; the error was on line 9. In order to efficiently manipulate the file, I have to break it into definitions. I will now attempt to do this. Sending statements to coqtop... Done. Splitting to definitions...  Splitting to definitions successful. I will now attempt to remove goals ending in [Abort.]  Aborted removal successful. I will now attempt to remove unused Ltacs  Ltac removal successful. I will now attempt to remove unused definitions  Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions  Non-instance definition removal successful. I will now attempt to remove unused variables  Variable removal successful. I will now attempt to remove unused contexts  Context removal successful. I will now attempt to replace Qed Obligation with Admit Obligations  Admitting Qed Obligations successful. Failed to do everything at once; trying one at a time. Admitting Qed Obligations unsuccessful. No successful changes. I will now attempt to replace Qeds with Admitteds  Admitting Qeds successful. Failed to do everything at once; trying one at a time. Admitting Qeds unsuccessful. No successful changes. I will now attempt to replace Qeds with admit. Defined.  Admitting Qeds successful. Failed to do everything at once; trying one at a time. Admitting Qeds unsuccessful. No successful changes. I will now attempt to remove goals ending in [Abort.]  Aborted removal successful. I will now attempt to remove unused Ltacs  Ltac removal successful. I will now attempt to remove unused definitions  Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions  Non-instance definition removal successful. I will now attempt to remove unused variables  Variable removal successful. I will now attempt to remove unused contexts  Context removal successful. I will now attempt to admit [abstract ...]s  Admitting [abstract ...] successful.  Admitting [abstract ...] successful. Admitting [abstract ...] unsuccessful. Admitting [abstract ...] unsuccessful. I will now attempt to remove goals ending in [Abort.]  Aborted removal successful. I will now attempt to remove unused Ltacs  Ltac removal successful. I will now attempt to remove unused definitions  Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions  Non-instance definition removal successful. I will now attempt to remove unused variables  Variable removal successful. I will now attempt to remove unused contexts  Context removal successful. I will now attempt to replace Obligation with Admit Obligations  Admitting Obligations successful. Failed to do everything at once; trying one at a time. Admitting Obligations unsuccessful. No successful changes. I will now attempt to admit lemmas with Admitted  Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions with Admitted  Admitting definitions successful. Failed to do everything at once; trying one at a time. Admitting definitions unsuccessful. No successful changes. I will now attempt to admit lemmas with admit. Defined  Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions with admit. Defined  Admitting definitions successful. Failed to do everything at once; trying one at a time. Admitting definitions unsuccessful. No successful changes. I will now attempt to export modules Module exportation unsuccessful. I will now attempt to split imports and exports Import/Export splitting unsuccessful. I will now attempt to split := definitions One-line definition splitting unsuccessful. I will now attempt to remove all lines, one at a time Line removal unsuccessful. I will now attempt to remove goals ending in [Abort.]  Aborted removal successful. I will now attempt to remove unused Ltacs  Ltac removal successful. I will now attempt to remove unused definitions  Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions  Non-instance definition removal successful. I will now attempt to remove unused variables  Variable removal successful. I will now attempt to remove unused contexts  Context removal successful. I will now attempt to remove empty sections No empty sections to remove. Now, I will attempt to strip repeated newlines and trailing spaces from this file...  Succeeded in stripping newlines and spaces. ```

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.