8000 "Warnings" and "Debug" options are synterp not interp by SkySkimmer · Pull Request #19981 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

"Warnings" and "Debug" options are synterp not interp #19981

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
Merged
merged 1 commit into from
Jan 9, 2025
Merged

"Warnings" and "Debug" options are synterp not interp #19981

merged 1 commit into from
Jan 9, 2025

Conversation

SkySkimmer
Copy link
Contributor
@SkySkimmer SkySkimmer commented Jan 2, 2025 •
edited
Loading

@SkySkimmer SkySkimmer requested a review from a team as a code owner January 2, 2025 21:18
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jan 2, 2025
@proux01
Copy link
Contributor
proux01 commented Jan 3, 2025

@coqbot run full ci

@proux01 proux01 added the kind: user messages Error messages, warnings, etc. label Jan 3, 2025
@proux01 proux01 added this to the 9.0+rc1 milestone Jan 3, 2025
@coqbot-app coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jan 3, 2025
@coqbot-app coqbot-app
Copy link
Contributor
coqbot-app bot commented Jan 3, 2025

🔴 CI failure at commit c5fed9e without any failure in the test-suite

✔️ Corresponding job for the base commit 03dd829 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-metacoq
  • You can also pass me a specific list of targets to minimize as arguments.

@SkySkimmer
Copy link
Contributor Author

@coqbot ci minimize

@coqbot-app coqbot-app
Copy link
Contributor
coqbot-app bot commented Jan 3, 2025

I have initiated minimization at commit c5fed9e for the suggested target ci-metacoq as requested.

@coqbot-app coqbot-app
Copy link
Contributor
coqbot-app bot commented Jan 3, 2025

Error: Could not minimize file (from ci-metacoq) (full log on GitHub Actions, cc @JasonGross)

build log (truncated to last 26KiB; full 5.2MiB file on GitHub Actions Artifacts under build.log) 
ds/coq/coq/stdlib/_build/default/theories Stdlib theories/Reals/NewtonInt.v 
MINIMIZER_DEBUG: info: /tmp/build_bdebcf_dune/tmp-coqbot-minimizer.JZthiDPfqo
MINIMIZER_DEBUG: files:  theories/Reals/NewtonInt.v /builds/coq/coq/stdlib/_build/default/theories/Reals/NewtonInt.v
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin/rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/stdlib/_build/default
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig c -q -w +default -w -deprecated-native-compiler-option -native-output-dir . -native-compiler on -nI /builds/coq/coq/stdlib/.wrappers/kernel -nI theories -nI theories/Arith -nI theories/Array -nI theories/BinNums -nI theories/Bool -nI theories/Classes -nI theories/Compat -nI theories/FSets -nI theories/Floats -nI theories/Init -nI theories/Lists -nI theories/Logic -nI theories/MSets -nI theories/NArith -nI theories/Numbers -nI theories/Numbers/Cyclic -nI theories/Numbers/Cyclic/Abstract -nI theories/Numbers/Cyclic/Int63 -nI theories/Numbers/Integer -nI theories/Numbers/Integer/Abstract -nI theories/Numbers/Integer/Binary -nI theories/Numbers/Integer/NatPairs -nI theories/Numbers/NatInt -nI theories/Numbers/Natural -nI theories/Numbers/Natural/Abstract -nI theories/Numbers/Natural/Binary -nI theories/PArith -nI theories/Program -nI theories/QArith -nI theories/Reals -nI theories/Reals/Abstract -nI theories/Reals/Cauchy -nI theories/Relations -nI theories/Setoids -nI theories/Sets -nI theories/Sorting -nI theories/Strings -nI theories/Structures -nI theories/Unicode -nI theories/Vectors -nI theories/Wellfounded -nI theories/ZArith -nI theories/btauto -nI theories/derive -nI theories/extraction -nI theories/funind -nI theories/micromega -nI theories/nsatz -nI theories/omega -nI theories/rtauto -nI theories/setoid_ring -nI theories/ssr -nI theories/ssrmatching -boot -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/btauto -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/cc -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/cc_core -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/derive -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/extraction -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/firstorder -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/firstorder_core -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/funind -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ltac -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ltac2 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ltac2_ltac1 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/micromega -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/micromega_core -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/nsatz -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/nsatz_core -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/number_string_notation -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ring -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/rtauto -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ssreflect -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ssrmatching -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tauto -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tutorial/p0 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tutorial/p1 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tutorial/p2 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tutorial/p3 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/zify -R /builds/coq/coq/_install_ci/lib/coq/theories Coq -R /builds/coq/coq/stdlib/_build/default/theories Stdlib theories/Reals/Integration.v 
MINIMIZER_DEBUG: info: /tmp/build_bdebcf_dune/tmp-coqbot-minimizer.bMPHLy9X2l
MINIMIZER_DEBUG: files:  theories/Reals/Integration.v /builds/coq/coq/stdlib/_build/default/theories/Reals/Integration.v
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin/rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/stdlib/_build/default
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig c -q -w +default -w -deprecated-native-compiler-option -native-output-dir . -native-compiler on -nI /builds/coq/coq/stdlib/.wrappers/kernel -nI theories -nI theories/Arith -nI theories/Array -nI theories/BinNums -nI theories/Bool -nI theories/Classes -nI theories/Compat -nI theories/FSets -nI theories/Floats -nI theories/Init -nI theories/Lists -nI theories/Logic -nI theories/MSets -nI theories/NArith -nI theories/Numbers -nI theories/Numbers/Cyclic -nI theories/Numbers/Cyclic/Abstract -nI theories/Numbers/Cyclic/Int63 -nI theories/Numbers/Integer -nI theories/Numbers/Integer/Abstract -nI theories/Numbers/Integer/Binary -nI theories/Numbers/Integer/NatPairs -nI theories/Numbers/NatInt -nI theories/Numbers/Natural -nI theories/Numbers/Natural/Abstract -nI theories/Numbers/Natural/Binary -nI theories/PArith -nI theories/Program -nI theories/QArith -nI theories/Reals -nI theories/Reals/Abstract -nI theories/Reals/Cauchy -nI theories/Relations -nI theories/Setoids -nI theories/Sets -nI theories/Sorting -nI theories/Strings -nI theories/Structures -nI theories/Unicode -nI theories/Vectors -nI theories/Wellfounded -nI theories/ZArith -nI theories/btauto -nI theories/derive -nI theories/extraction -nI theories/funind -nI theories/micromega -nI theories/nsatz -nI theories/omega -nI theories/rtauto -nI theories/setoid_ring -nI theories/ssr -nI theories/ssrmatching -boot -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/btauto -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/cc -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/cc_core -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/derive -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/extraction -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/firstorder -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/firstorder_core -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/funind -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ltac -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ltac2 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ltac2_ltac1 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/micromega -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/micromega_core -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/nsatz -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/nsatz_core -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/number_string_notation -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ring -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/rtauto -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ssreflect -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ssrmatching -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tauto -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tutorial/p0 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tutorial/p1 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tutorial/p2 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tutorial/p3 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/zify -R /builds/coq/coq/_install_ci/lib/coq/theories Coq -R /builds/coq/coq/stdlib/_build/default/theories Stdlib theories/Reals/Reals.v 
MINIMIZER_DEBUG: info: /tmp/build_bdebcf_dune/tmp-coqbot-minimizer.58fyztAq7O
MINIMIZER_DEBUG: files:  theories/Reals/Reals.v /builds/coq/coq/stdlib/_build/default/theories/Reals/Reals.v
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin/rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/stdlib/_build/default
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig c -q -w +default -w -deprecated-native-compiler-option -native-output-dir . -native-compiler on -nI /builds/coq/coq/stdlib/.wrappers/kernel -nI theories -nI theories/Arith -nI theories/Array -nI theories/BinNums -nI theories/Bool -nI theories/Classes -nI theories/Compat -nI theories/FSets -nI theories/Floats -nI theories/Init -nI theories/Lists -nI theories/Logic -nI theories/MSets -nI theories/NArith -nI theories/Numbers -nI theories/Numbers/Cyclic -nI theories/Numbers/Cyclic/Abstract -nI theories/Numbers/Cyclic/Int63 -nI theories/Numbers/Integer -nI theories/Numbers/Integer/Abstract -nI theories/Numbers/Integer/Binary -nI theories/Numbers/Integer/NatPairs -nI theories/Numbers/NatInt -nI theories/Numbers/Natural -nI theories/Numbers/Natural/Abstract -nI theories/Numbers/Natural/Binary -nI theories/PArith -nI theories/Program -nI theories/QArith -nI theories/Reals -nI theories/Reals/Abstract -nI theories/Reals/Cauchy -nI theories/Relations -nI theories/Setoids -nI theories/Sets -nI theories/Sorting -nI theories/Strings -nI theories/Structures -nI theories/Unicode -nI theories/Vectors -nI theories/Wellfounded -nI theories/ZArith -nI theories/btauto -nI theories/derive -nI theories/extraction -nI theories/funind -nI theories/micromega -nI theories/nsatz -nI theories/omega -nI theories/rtauto -nI theories/setoid_ring -nI theories/ssr -nI theories/ssrmatching -boot -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/btauto -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/cc -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/cc_core -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/derive -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/extraction -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/firstorder -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/firstorder_core -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/funind -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ltac -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ltac2 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ltac2_ltac1 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/micromega -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/micromega_core -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/nsatz -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/nsatz_core -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/number_string_notation -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ring -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/rtauto -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ssreflect -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/ssrmatching -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tauto -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tutorial/p0 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tutorial/p1 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tutorial/p2 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/tutorial/p3 -I /builds/coq/coq/_install_ci/lib/rocq-runtime/plugins/zify -R /builds/coq/coq/_install_ci/lib/coq/theories Coq -R /builds/coq/coq/stdlib/_build/default/theories Stdlib theories/setoid_ring/Rings_R.v 
MINIMIZER_DEBUG: info: /tmp/build_bdebcf_dune/tmp-coqbot-minimizer.vg0J32E9jW
MINIMIZER_DEBUG: files:  theories/setoid_ring/Rings_R.v /builds/coq/coq/stdlib/_build/default/theories/setoid_ring/Rings_R.v
+ dev/with-rocq-wrap.sh dune install --root . coq-stdlib --prefix=/builds/coq/coq/_install_ci
++ command -v rocq
+ rocq=/builds/coq/coq/_install_ci/bin/rocq
++ md5sum /builds/coq/coq/_install_ci/bin/rocq
+ rocqhash='088679924784dc7f3d97e9859d36b87c  /builds/coq/coq/_install_ci/bin/rocq'
+ rm -rf .wrappers
+ mkdir .wrappers
+ cat
+ cat
+ chmod +x .wrappers/coqc .wrappers/coqdep
++ ocamlfind query rocq-runtime.kernel
+ ln -s /builds/coq/coq/_install_ci/lib/rocq-runtime/kernel .wrappers/kernel
+ cat
+ export PATH=/builds/coq/coq/stdlib/.wrappers:/builds/coq/coq/_install_ci/bin:/builds/coq/coq/_install_ci/bin:/root/.opamcache/4.14.1+flambda/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
+ PATH=/builds/coq/coq/stdlib/.wrappers:/builds/coq/coq/_install_ci/bin:/builds/coq/coq/_install_ci/bin:/root/.opamcache/4.14.1+flambda/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
+ export OCAMLPATH=/builds/coq/coq/stdlib/.wrappers:/builds/coq/coq/_install_ci/lib:
+ OCAMLPATH=/builds/coq/coq/stdlib/.wrappers:/builds/coq/coq/_install_ci/lib:
+ dune install --root . coq-stdlib --prefix=/builds/coq/coq/_install_ci
+ code=0
+ printf '\n%s exit code: %s\n' stdlib 0
+ '[' stdlib '!=' stdlib_test ']'
+ echo 'Aggregating timing log...'
Aggregating timing log...
+ echo

+ tools/make-one-time-file.py --real stdlib.log
No timing data
+ '[' '' ']'
+ exit 0
./dev/ci/ci-wrapper.sh equations
+ CI_NAME=equations
+ CI_SCRIPT=ci-equations.sh
+++ dirname ./dev/ci/ci-wrapper.sh
++ cd ./dev/ci
++ pwd
+ DIR=/builds/coq/coq/dev/ci
+ cd /builds/coq/coq/dev/ci/../..
+ export TIMED=1
+ TIMED=1
+ '[' '' ']'
+ '[' -t 1 ']'
+ '[' '' ']'
+ COQ_CI_COLOR=
+ export GIT_PAGER=
+ GIT_PAGER=
+ '[' '' = 1 ']'
+ '[' '' = 1 ']'
+ bash /builds/coq/coq/dev/ci/ci-equations.sh
+ tee equations.log
++ : 2
++ export NJOBS
++ which cygpath
++ OCAMLFINDSEP=:
++ '[' -n 1 ']'
++ export COQBIN=/builds/coq/coq/_install_ci/bin
++ COQBIN=/builds/coq/coq/_install_ci/bin
++ export OCAMLPATH=/builds/coq/coq/_install_ci/lib:
++ OCAMLPATH=/builds/coq/coq/_install_ci/lib:
++ export PATH=/builds/coq/coq/_install_ci/bin:/root/.opamcache/4.14.1+flambda/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
++ PATH=/builds/coq/coq/_install_ci/bin:/root/.opamcache/4.14.1+flambda/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
++ CI_INSTALL_DIR=/builds/coq/coq/_install_ci
++ export CI_BRANCH=
++ CI_BRANCH=
++ [[ '' =~ ^[0-9]*$ ]]
++ export CI_PULL_REQUEST=
++ CI_PULL_REQUEST=
++ export PATH=/builds/coq/coq/_install_ci/bin:/builds/coq/coq/_install_ci/bin:/root/.opamcache/4.14.1+flambda/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
++ PATH=/builds/coq/coq/_install_ci/bin:/builds/coq/coq/_install_ci/bin:/root/.opamcache/4.14.1+flambda/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
++ export COQBIN=/builds/coq/coq/_install_ci/bin/
++ COQBIN=/builds/coq/coq/_install_ci/bin/
++ ls -l /builds/coq/coq/_install_ci/bin/
total 221136
-rwxr-xr-x 1 root root     2393 Jan  3 10:25 coq-tex
-rwxr-xr-x 1 root root  2745296 Jan  3 10:25 coq-tex.orig
-rwxr-xr-x 1 root root  6458200 Dec 27 15:33 coq_makefile
-rwxr-xr-x 1 root root     2390 Jan  3 10:25 coqc
-rwxr-xr-x 1 root root  4055656 Jan  3 10:25 coqc.orig
-rwxr-xr-x 1 root root 22435200 Dec 27 15:33 coqchk
-rwxr-xr-x 1 root root  7220568 Dec 27 15:33 coqdep
-rwxr-xr-x 1 root root     2392 Jan  3 10:25 coqdoc
-rwxr-xr-x 1 root root  7013632 Jan  3 10:25 coqdoc.orig
-rwxr-xr-x 1 root root     2392 Jan  3 10:25 coqide
-rwxr-xr-x 1 root root 19219352 Jan  3 10:25 coqide.orig
-rwxr-xr-x 1 root root     2395 Jan  3 10:25 coqidetop
-rwxr-xr-x 1 root root 74653440 Jan  3 10:25 coqidetop.orig
-rwxr-xr-x 1 root root     2395 Jan  3 10:25 coqnative
-rwxr-xr-x 1 root root  4055704 Jan  3 10:25 coqnative.orig
-rwxr-xr-x 1 root root     2391 Jan  3 10:25 coqpp
-rwxr-xr-x 1 root root  3475288 Jan  3 10:25 coqpp.orig
-rwxr-xr-x 1 root root     2401 Jan  3 10:25 coqtimelog2html
-rwxr-xr-x 1 root root  4597304 Jan  3 10:25 coqtimelog2html.orig
-rwxr-xr-x 1 root root     2392 Jan  3 10:25 coqtop
-rwxr-xr-x 1 root root     2397 Jan  3 10:25 coqtop.byte
-rwxr-xr-x 1 root root  4056000 Jan  3 10:25 coqtop.byte.orig
-rwxr-xr-x 1 root root  4055744 Jan  3 10:25 coqtop.orig
-rwxr-xr-x 1 root root     2391 Jan  3 10:25 coqwc
-rwxr-xr-x 1 root root  2335568 Jan  3 10:25 coqwc.orig
-rwxr-xr-x 1 root root     2396 Jan  3 10:25 coqworkmgr
-rwxr-xr-x 1 root root  3433128 Jan  3 10:25 coqworkmgr.orig
-rwxr-xr-x 1 root root     2394 Jan  3 10:25 csdpcert
-rwxr-xr-x 1 root root  6003264 Jan  3 10:25 csdpcert.orig
-rwxr-xr-x 1 root root     2397 Jan  3 10:25 ocamllibdep
-rwxr-xr-x 1 root root  3493488 Jan  3 10:25 ocamllibdep.orig
-rwxr-xr-x 1 root root     2390 Jan  3 10:25 rocq
-rwxr-xr-x 1 root root     2395 Jan  3 10:25 rocq.byte
-rwxr-xr-x 1 root root  6797189 Jan  3 10:25 rocq.byte.orig
-rwxr-xr-x 1 root root 10635904 Jan  3 10:25 rocq.orig
-rwxr-xr-x 1 root root     2393 Jan  3 10:25 rocqchk
-rwxr-xr-x 1 root root 22435208 Jan  3 10:25 rocqchk.orig
-rwxr-xr-x 1 root root     2392 Jan  3 10:25 votour
-rwxr-xr-x 1 root root  7145288 Jan  3 10:25 votour.orig
++ CI_BUILD_DIR=/builds/coq/coq/_build_ci
++ ls -l /builds/coq/coq/_build_ci
total 4
drwxr-xr-x 20 root root 4096 Dec 27 15:42 metacoq
++ declare -A overlays
++ set +x
+ git_download equations
+ local project=equations
+ local dest=/builds/coq/coq/_build_ci/equations
+ local giturl_var=equations_CI_GITURL
+ local giturl=https://github.com/mattam82/Coq-Equations
+ local ref_var=equations_CI_REF
+ local ref=main
+ local parent_project_var=equations_CI_PARENT_PROJECT
+ local parent_project=
+ local submodule_folder_var=equations_CI_SUBMODULE_FOLDER
+ local submodule_folder=
+ local ov_url=
+ local ov_ref=
++ dirname /builds/coq/coq/_build_ci/equations
+ local dest_prefix=/builds/coq/coq/_build_ci/
+ '[' '' = '' ']'
+ local parent_project_dest=/builds/coq/coq/_build_ci/
+ local parent_project_relative_dest=
+ '[' -d /builds/coq/coq/_build_ci/equations ']'
+ [[ -n '' ]]
+ '[' '' = 1 ']'
+ '[' '' = '' ']'
+ '[' -n '' ']'
+ git clone https://github.com/mattam82/Coq-Equations /builds/coq/coq/_build_ci/equations
Cloning into '/builds/coq/coq/_build_ci/equations'...
+ pushd /builds/coq/coq/_build_ci/equations
/builds/coq/coq/_build_ci/equations /builds/coq/coq
+ git checkout main
Already on 'main'
Your branch is up to date with 'origin/main'.
+ git log -n 1
commit 3431c88a7575a3972191c25809c563aafdc6414e
Merge: 596d2093 c745b4e7
Author: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date:   Fri Dec 6 11:34:40 2024 +0100

    Merge pull request #625 from proux01/stdlib_repo
    
    Adapt to https://github.com/coq/coq/pull/19530
+ [[ -n '' ]]
+ '[' '' = 1 ']'
+ popd
/builds/coq/coq
+ '[' '' ']'
+ export 'COQEXTRAFLAGS=-native-compiler no'
+ COQEXTRAFLAGS='-native-compiler no'
+ cd /builds/coq/coq/_build_ci/equations
+ '[' -e Makefile.coq ']'
+ ./configure.sh coq
+ make -f Makefile.coq .merlin
+ '[' -z x ']'
+ command make -f Makefile.coq .merlin
make[1]: Entering directory '/builds/coq/coq/_build_ci/equations'
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin//rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig makefile -sources-of -f _CoqProject 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.KCpz2G0Thy
MINIMIZER_DEBUG: files: 
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin///rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig c --print-version 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.YGrv6Gj0CA
MINIMIZER_DEBUG: files: 
ROCQ DEP VFILES
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin///rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig dep -vos -dyndep var -f _CoqProject 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.plUNzgio1l
MINIMIZER_DEBUG: files: 
.Makefile.coq.d (real: 0.06, user: 0.02, sys: 0.03, mem: 14848 ko)
COQPP src/g_equations.mlg
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin///rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig pp-mlg src/g_equations.mlg 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.mELudv4u8i
MINIMIZER_DEBUG: files: 
CAMLDEP src/extra_tactics.mli
CAMLDEP src/noconf.mli
CAMLDEP src/noconf_hom.mli
CAMLDEP src/equations.mli
CAMLDEP src/principles.mli
CAMLDEP src/principles_proofs.mli
CAMLDEP src/covering.mli
CAMLDEP src/splitting.mli
CAMLDEP src/simplify.mli
CAMLDEP src/context_map.mli
CAMLDEP src/syntax.mli
CAMLDEP src/depelim.mli
CAMLDEP src/eqdec.mli
CAMLDEP src/subterm.mli
CAMLDEP src/sigma_types.mli
CAMLDEP src/ederive.mli
CAMLDEP src/equations_common.mli
OCAMLLIBDEP src/equations_plugin.mllib
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin///ocamllibdep
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/ocamllibdep.orig -c -I /builds/coq/coq/_build_ci/equations/src -I /builds/coq/coq/_build_ci/equations/test-suite -I /builds/coq/coq/_build_ci/equations/theories -I /builds/coq/coq/_build_ci/equations/examples src/equations_plugin.mllib 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.60CUrtAUpH
MINIMIZER_DEBUG: files: 
CAMLDEP src/extra_tactics.ml
CAMLDEP src/noconf.ml
CAMLDEP src/noconf_hom.ml
CAMLDEP src/equations.ml
CAMLDEP src/principles.ml
CAMLDEP src/principles_proofs.ml
CAMLDEP src/covering.ml
CAMLDEP src/splitting.ml
CAMLDEP src/simplify.ml
CAMLDEP src/context_map.ml
CAMLDEP src/syntax.ml
CAMLDEP src/depelim.ml
CAMLDEP src/eqdec.ml
CAMLDEP src/subterm.ml
CAMLDEP src/sigma_types.ml
CAMLDEP src/ederive.ml
CAMLDEP src/equations_common.ml
CAMLDEP src/g_equations.ml
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin//rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig makefile -sources-of -f _CoqProject 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.T8MfvATApv
MINIMIZER_DEBUG: files: 
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin///rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig c --print-version 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.PxzkHi2L3r
MINIMIZER_DEBUG: files: 
FILL .merlin
make[2]: Entering directory '/builds/coq/coq/_build_ci/equations'
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin////rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig makefile -sources-of -f _CoqProject 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.R7IvKMVk9m
MINIMIZER_DEBUG: files: 
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin/////rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig c --print-version 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.V6DLOoTcuy
MINIMIZER_DEBUG: files: 
make[2]: Leaving directory '/builds/coq/coq/_build_ci/equations'
make[1]: Leaving directory '/builds/coq/coq/_build_ci/equations'
+ make
+ '[' -z x ']'
+ command make
make[1]: Entering directory '/builds/coq/coq/_build_ci/equations'
make -f Makefile.coq
make[2]: Entering directory '/builds/coq/coq/_build_ci/equations'
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin//rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig makefile -sources-of -f _CoqProject 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.h0Ks1XqpIM
MINIMIZER_DEBUG: files: 
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin///rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig c --print-version 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.PnY9oHfxdW
MINIMIZER_DEBUG: files: 
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin////rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig makefile -sources-of -f _CoqProject 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.gAgJeGVPVz
MINIMIZER_DEBUG: files: 
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin/////rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig c --print-versio
8000
n 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.uLjKARDCtx
MINIMIZER_DEBUG: files: 
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin////rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig makefile -sources-of -f _CoqProject 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.shg5tZZ4dt
MINIMIZER_DEBUG: files: 
MINIMIZER_DEBUG_EXTRA: coqc: /builds/coq/coq/_install_ci/bin/////rocq
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/builds/coq/coq/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /builds/coq/coq/_install_ci/bin/rocq.orig c --print-version 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.MF30HO263o
MINIMIZER_DEBUG: files: 
make[3]: *** No rule to make target '/builds/coq/coq/_build_ci/equations/src/equations_common.cmx', needed by 'src/equations_plugin.cmxa'.  Stop.
make[2]: *** [Makefile.coq:416: all] Error 2
make[2]: Leaving directory '/builds/coq/coq/_build_ci/equations'
make[1]: *** [Makefile:6: all] Error 2
make[1]: Leaving directory '/builds/coq/coq/_build_ci/equations'
+ code=2
+ printf '\n%s exit code: %s\n' equations 2
+ '[' equations '!=' stdlib_test ']'
+ echo 'Aggregating timing log...'
Aggregating timing log...
+ echo

+ tools/make-one-time-file.py --real equations.log
    Time | Peak Mem | File Name            
-------------------------------------------
0m00.06s | 14848 ko | Total Time / Peak Mem
-------------------------------------------
0m00.06s | 14848 ko | .Makefile.coq.d      
+ '[' '' ']'
+ exit 2
make: *** [Makefile.ci:262: ci-equations] Error 2
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.

SkySkimmer added a commit to SkySkimmer/MetaRocq that referenced this pull request Jan 7, 2025
@SkySkimmer
Adapt to rocq-prover/rocq#19981 (Set Warnings is synterp phase)
9e681cb
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jan 7, 2025
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jan 7, 2025
@SkySkimmer
Copy link
Contributor Author

There is a change of behaviour even in coqc: if Foo does #[export] Set Warnings "-foo". Command. #[export] Set Warnings "+foo". , when doing Import Foo the Command used to see warning foo at its default value in synterp and disabled in interp phase, and now sees it disabled in synterp phase and as-error in interp phase.

@proux01
Copy link
Contributor
proux01 commented Jan 8, 2025

Indeed, and applying to both synterp and interp would lead to similarly unexpected behaviors with the flags still being in a strange state at the beginning of the interp phase.
Maybe "resetting" the flags at the end on the synterp phase would work, but that's no longer a one line PR.

@ppedrot
Copy link
Member
ppedrot commented Jan 9, 2025

This looks like there is some design to pin down, shouldn't this be postponed?

@proux01
Copy link
Contributor
proux01 commented Jan 9, 2025

I also think we'd better not rush the design. Postponing seems the reasonable thing to do then.

@SkySkimmer
Copy link
Contributor Author

Master is bugged IMO, it also makes UI behave differently from compilation
This PR may have issues but it's still better than the current state

@proux01 proux01 added the needs: changelog entry This should be documented in doc/changelog. label Jan 9, 2025
@proux01 proux01 self-assigned this Jan 9, 2025
@proux01
Copy link
Contributor
proux01 commented Jan 9, 2025

Considering impact on CI seems minimal, ok by me for "the new bug is less bad than the current one" but we need at least a small changelog entry.
I'll merge once the overlay is merged and we have a changelog entry.

ppedrot added a commit to MetaRocq/metarocq that referenced this pull request Jan 9, 2025
@ppedrot
Merge pull request #1132 from SkySkimmer/classify-warn
17ba45f 
Adapt to rocq-prover/rocq#19981 (Set Warnings is synterp phase)
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jan 9, 2025
@SkySkimmer SkySkimmer removed needs: changelog entry This should be documented in doc/changelog. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Jan 9, 2025
@SkySkimmer
Copy link
Contributor Author

done
8000

proux01
proux01 approved these changes Jan 9, 2025
View reviewed changes
doc/changelog/08-vernac-commands-and-options/19981-classify-warn.rst
@@ -0,0 +1,5 @@
- **Fixed:**
:opt:`Debug` and :opt:`Warnings` are classified as Synterp.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's a shame that #19759 is not merged yet, otherwise we could refer to it here.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Cc @Zimmi48 FYI (but definitely not a serious/urgent issue)

@proux01
Copy link
Contributor
proux01 commented Jan 9, 2025

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 01f4cb5 into rocq-prover:master Jan 9, 2025
5 checks passed
@coqbot-app coqbot-app
Copy link
Contributor
coqbot-app bot commented Jan 9, 2025

@proux01: Please take care of the following overlays:

  • 19981-SkySkimmer-classify-warn.sh

@SkySkimmer SkySkimmer deleted the classify-warn branch January 9, 2025 16:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@proux01 proux01 proux01 approved these changes

Assignees

@proux01 proux01

Labels
kind: user messages Error messages, warnings, etc.
Projects
None yet
Milestone
9.0+rc1
Development

Successfully merging this pull request may close these issues.
3 participants
@SkySkimmer @proux01 @ppedrot
0