Closed JasonGross closed 1 year 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 minimize coq-8.16
#!/usr/bin/env bash
opam install -y coq-equations
git clone https://github.com/JasonGross/metacoq.git --branch=coq-8.16+all-polymorphic
cd metacoq
./configure.sh local
make safechecker TIMED=1 -j2
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@JasonGross, Error: Could not minimize file /github/workspace/metacoq/safechecker/theories/PCUICSafeConversion.v (full log on GitHub Actions, cc @JasonGross)
build.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 minimize coq-8.16
#!/usr/bin/env bash
opam install -y coq-equations
git clone https://github.com/JasonGross/metacoq.git --branch=coq-8.16+all-polymorphic
cd metacoq
./configure.sh local
make safechecker TIMED=1 -j2
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@JasonGross, Minimized File /github/workspace/metacoq/safechecker/theories/PCUICSafeConversion.v (interrupted by timeout) (full log on GitHub Actions)
bug.v
)build.log
)bug.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 minimize coq-8.16
#!/usr/bin/env bash
opam install -y coq-equations
git clone https://github.com/JasonGross/metacoq.git --branch=zzz-bug-equations-anomaly
cd metacoq
./configure.sh local
make safechecker TIMED=1 -j2
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@coqbot minimize coq-8.16
#!/usr/bin/env bash
opam install -y coq-equations
git clone https://github.com/JasonGross/metacoq.git --branch=zzz-bug-equations-anomaly
cd metacoq
./configure.sh local
make safechecker TIMED=1 -j2
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@JasonGross, Error: Could not minimize file (full log on GitHub Actions, cc @JasonGross)
build.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 minimize coq-8.16
#!/usr/bin/env bash
opam install -y --criteria=paranoid coq-equations
git clone https://github.com/JasonGross/metacoq.git --branch=zzz-bug-equations-anomaly
cd metacoq
./configure.sh local
make safechecker TIMED=1 -j2
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@JasonGross, Minimized File /github/workspace/metacoq/utils/theories/ReflectEq.v (full log on GitHub Actions)
build.log
)bug.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 minimize coq-8.16
#!/usr/bin/env bash
opam reinstall -y coq-equations
git clone https://github.com/JasonGross/metacoq.git --branch=zzz-bug-equations-anomaly
cd metacoq
./configure.sh local
make safechecker TIMED=1 -j2
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@coqbot minimize coq-8.16
#!/usr/bin/env bash
opam reinstall -y coq-equations
wrap_opam coqc coqtop
for i in coqc coqtop; do
pushd "$(dirname "$(which "$i")")"
wrap_file "$i"
popd
done
git clone https://github.com/JasonGross/metacoq.git --branch=zzz-bug-equations-anomaly
cd metacoq
./configure.sh local
make safechecker TIMED=1 -j2
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@coqbot minimize coq-8.16
#!/usr/bin/env bash
opam install -y coq-equations
wrap_opam coqc coqtop
for i in coqc coqtop; do
pushd "$(dirname "$(which "$i")")"
wrap_file "$i"
popd
done
git clone https://github.com/JasonGross/metacoq.git --branch=zzz-bug-equations-anomaly
cd metacoq
./configure.sh local
make safechecker TIMED=1 -j2
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@JasonGross, Error: Could not minimize file (full log on GitHub Actions, cc @JasonGross)
build.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, Error: Could not minimize file (full log on GitHub Actions, cc @JasonGross)
build.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, Error: Could not minimize file (full log on GitHub Actions, cc @JasonGross)
build.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 minimize coq-8.16
#!/usr/bin/env bash
opam list
opam pin add coq 8.16.1
opam pin add dune || opam pin add dune $(dune -v)
opam install -y coq-equations
git clone https://github.com/JasonGross/metacoq.git --branch=zzz-bug-equations-anomaly
cd metacoq
./configure.sh local
make safechecker TIMED=1 -j2
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@JasonGross, Error: Could not minimize file (full log on GitHub Actions, cc @JasonGross)
build.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 minimize coq-8.16
#!/usr/bin/env bash
opam install -y coq-equations
git clone https://github.com/JasonGross/metacoq.git --branch=zzz-bug-equations-anomaly
cd metacoq
./configure.sh local
make safechecker TIMED=1 -j2
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@JasonGross, Error: Could not minimize file (full log on GitHub Actions, cc @JasonGross)
build.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 minimize coq-8.16
#!/usr/bin/env bash
opam install -y coq-equations
git clone https://github.com/JasonGross/metacoq.git --branch=zzz-bug-equations-anomaly
cd metacoq
./configure.sh local
make safechecker TIMED=1 -j2
@JasonGross, Minimized File /github/workspace/metacoq/safechecker/theories/PCUICSafeConversion.v (interrupted by timeout) (full log on GitHub Actions)
build.log
)bug.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 minimize coq-8.16
#!/usr/bin/env bash
opam install -y coq-equations
git clone https://github.com/JasonGross/metacoq.git --branch=zzz-bug-equations-anomaly
cd metacoq
./configure.sh local
make safechecker TIMED=1 -j2
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@JasonGross, Minimized File /github/workspace/metacoq/safechecker/theories/PCUICSafeConversion.v (full log on GitHub Actions)
build.log
)bug.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.
tracking https://github.com/coq/coq/issues/18660 @coqbot minimize coq.dev
set -ex
git clone https://github.com/meta-introspector/metacoq.git --branch=feature/ltac_debug
cd metacoq
git checkout 6c23b8f5649d7dc8f51bce9310a0b70a28607853
opam install -y --deps-only coq-metacoq
make
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@coqbot minimize coq.dev
git clone https://github.com/meta-introspector/metacoq.git --branch=feature/ltac_debug
cd metacoq
git checkout 6c23b8f5649d7dc8f51bce9310a0b70a28607853
opam install -y --deps-only coq-metacoq
make
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@coqbot minimize coq.dev
set -ex
printf -- git clone https://github.com/meta-introspector/metacoq.git --branch=feature/ltac_debug
yes | git clone https://github.com/meta-introspector/metacoq.git --branch=feature/ltac_debug
cd metacoq
git checkout 6c23b8f5649d7dc8f51bce9310a0b70a28607853
opam install -y --deps-only coq-metacoq
make
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@JasonGross, Error: Could not minimize file (full log on GitHub Actions, cc @JasonGross)
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, Error: Could not minimize file (full log on GitHub Actions, cc @JasonGross)
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, Error: Could not minimize file (full log on GitHub Actions, cc @JasonGross)
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 minimize coq.dev
git clone https://github.com/meta-introspector/metacoq.git --branch=feature/ltac_debug
cd metacoq
git checkout 6c23b8f5649d7dc8f51bce9310a0b70a28607853
opam install -y --deps-only coq-metacoq-utils
./configure.sh local
make
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
@JasonGross, Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/metacoq/utils/theories/All_Forall.v (full log on GitHub Actions - verbose log)
build.log
)bug.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 minimize coq-8.16