Call guard checking with evar handlers in higher layers #18864

SkySkimmer · 2024-03-29T13:59:20Z

Fix #18358
Fix #18680
Fix #18850

Overlays:

Adapt to coq/coq#18864 (search_guard can handle evars) mattam82/Coq-Equations#587

coqbot-app · 2024-03-29T23:08:48Z

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

✔️ Corresponding job for the base commit fc1b697 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-equations_test

You can also pass me a specific list of targets to minimize as arguments.

SkySkimmer · 2024-03-29T23:25:15Z

@coqbot ci minimize

coqbot-app · 2024-03-29T23:25:20Z

I have initiated minimization at commit 8b4c8b9 for the suggested target ci-equations_test as requested.

coqbot-app · 2024-03-29T23:30:21Z

Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/equations/test-suite/issues/issue328.v (from ci-equations_test) (full log on GitHub Actions - verbose log)

We are collecting data on the user experience of the Coq Bug Minimizer.
If you haven't already filled the survey for this PR, please fill out our short survey!

🌟 Minimized Coq File (consider adding this file to the test-suite)

(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/equations/test-suite" "TestSuite" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/equations/theories" "Equations" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Equations" "Equations" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/equations/src" "-top" "TestSuite.issues.issue328") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 35 lines to 17 lines, then from 30 lines to 275 lines, then from 280 lines to 23 lines, then from 36 lines to 216 lines, then from 220 lines to 28 lines, then from 33 lines to 29 lines *)
(* coqc version 8.20+alpha compiled with OCaml 4.09.0
   coqtop version runner-cabngxqim-project-4504-concurrent-1:/builds/coq/coq/_build/default,(HEAD detached at 07d477a472912) (07d477a472912eb0281f963b0ac6b19b899f9d28)
   Expected coqc runtime on this file: 0.091 sec *)
Require Coq.extraction.Extraction.

Declare ML Module "equations_plugin:coq-equations.plugin".

Variant equations_tag@{} : Set := the_equations_tag.

Definition fixproto := the_equations_tag.

Register fixproto as equations.fixproto.

Definition block := the_equations_tag.

Register block as equations.internal.block.
Set Implicit Arguments.

Parameter A : Type.

Inductive nonEmpty (A : Type) : Type :=
| singleton : A -> nonEmpty A
| consNE : A -> nonEmpty A -> nonEmpty A.

Equations? fromList (l : list A) : length l > 0 -> nonEmpty A :=
{
  fromList nil H := _;
  fromList (cons x nil) _ := singleton x;
  fromList (cons x (cons y l))  _ := consNE x (fromList (cons y l) _)
}.

🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)

🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)

📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 2.7MiB file on GitHub Actions Artifacts under build.log)

e examples
make[1]: Entering directory '/github/workspace/builds/coq/coq-failing/_build_ci/equations'
make -f Makefile.coq
make[2]: Entering directory '/github/workspace/builds/coq/coq-failing/_build_ci/equations'
MINIMIZER_DEBUG_EXTRA: coqc: /github/workspace/builds/coq/coq-failing/_install_ci/bin///coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig --print-version 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.Vu00lWyOvF
MINIMIZER_DEBUG: files: 
MINIMIZER_DEBUG_EXTRA: coqc: /github/workspace/builds/coq/coq-failing/_install_ci/bin/////coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig --print-version 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.tjY8ft42dN
MINIMIZER_DEBUG: files: 
MINIMIZER_DEBUG_EXTRA: coqc: /github/workspace/builds/coq/coq-failing/_install_ci/bin/////coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig --print-version 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.0bQVDeuogy
MINIMIZER_DEBUG: files: 
make[3]: Nothing to be done for 'real-all'.
MINIMIZER_DEBUG_EXTRA: coqc: /github/workspace/builds/coq/coq-failing/_install_ci/bin/////coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/equations
MINIMIZER_DEBUG_EXTRA: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig --print-version 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.tGJsi1ggCQ
MINIMIZER_DEBUG: files: 
make[2]: Leaving directory '/github/workspace/builds/coq/coq-failing/_build_ci/equations'
test -f Makefile.hott && make -f Makefile.hott || true
cd test-suite && make
make[2]: Entering directory '/github/workspace/builds/coq/coq-failing/_build_ci/equations/test-suite'
MINIMIZER_DEBUG_EXTRA: coqc: /github/workspace/builds/coq/coq-failing/_install_ci/bin///coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/equations/test-suite
MINIMIZER_DEBUG_EXTRA: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig --print-version 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.7hZ4s5RmEv
MINIMIZER_DEBUG: files: 
MINIMIZER_DEBUG_EXTRA: coqc: /github/workspace/builds/coq/coq-failing/_install_ci/bin/////coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/equations/test-suite
MINIMIZER_DEBUG_EXTRA: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig --print-version 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.ab5RvGxexk
MINIMIZER_DEBUG: files: 
MINIMIZER_DEBUG_EXTRA: coqc: /github/workspace/builds/coq/coq-failing/_install_ci/bin/////coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/equations/test-suite
MINIMIZER_DEBUG_EXTRA: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig --print-version 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.JmcmvG9G4n
MINIMIZER_DEBUG: files: 
COQC Basics.v
MINIMIZER_DEBUG_EXTRA: coqc: /github/workspace/builds/coq/coq-failing/_install_ci/bin/////coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/equations/test-suite
MINIMIZER_DEBUG_EXTRA: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -I /github/workspace/builds/coq/coq-failing/_build_ci/equations/src -R /github/workspace/builds/coq/coq-failing/_build_ci/equations/test-suite TestSuite -R /github/workspace/builds/coq/coq-failing/_build_ci/equations/theories Equations Basics.v 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.n9FWQb5dOO
MINIMIZER_DEBUG: files:  Basics.v
File "./Basics.v", line 9, characters 0-46:
Warning: Using Vector.t is known to be technically difficult, see
<https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v>.
[warn-library-file-stdlib-vector,stdlib-vector,warn-library-file,user-warn,default]
File "./Basics.v", line 124, characters 0-30:
Warning: Using Vector.t is known to be technically difficult, see
<https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v>.
[warn-library-file-stdlib-vector,stdlib-vector,warn-library-file,user-warn,default]
File "./Basics.v", line 438, characters 0-23:
Warning: Using Vector.t is known to be technically difficult, see
<https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v>.
[warn-library-file-stdlib-vector,stdlib-vector,warn-library-file,user-warn,default]
File "./Basics.v", line 630, characters 0-23:
Warning: Using Vector.t is known to be technically difficult, see
<https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v>.
[warn-library-file-stdlib-vector,stdlib-vector,warn-library-file,user-warn,default]
Basics.vo (real: 2.53, user: 2.40, sys: 0.12, mem: 441776 ko)
COQC issues/issue95_2.v
MINIMIZER_DEBUG_EXTRA: coqc: /github/workspace/builds/coq/coq-failing/_install_ci/bin/////coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/equations/test-suite
MINIMIZER_DEBUG_EXTRA: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -I /github/workspace/builds/coq/coq-failing/_build_ci/equations/src -R /github/workspace/builds/coq/coq-failing/_build_ci/equations/test-suite TestSuite -R /github/workspace/builds/coq/coq-failing/_build_ci/equations/theories Equations issues/issue95_2.v 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.cj1Ojqc6DY
MINIMIZER_DEBUG: files:  issues/issue95_2.v
issues/issue95_2.vo (real: 0.26, user: 0.15, sys: 0.11, mem: 318420 ko)
COQC issues/issue328.v
MINIMIZER_DEBUG_EXTRA: coqc: /github/workspace/builds/coq/coq-failing/_install_ci/bin/////coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/equations/test-suite
MINIMIZER_DEBUG_EXTRA: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -I /github/workspace/builds/coq/coq-failing/_build_ci/equations/src -R /github/workspace/builds/coq/coq-failing/_build_ci/equations/test-suite TestSuite -R /github/workspace/builds/coq/coq-failing/_build_ci/equations/theories Equations issues/issue328.v 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.FCQ2ZxTmga
MINIMIZER_DEBUG: files:  issues/issue328.v
File "./issues/issue328.v", line 11, characters 11-19:
Error:
Anomaly
"File "kernel/cClosure.ml", line 134, characters 26-32: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

Command exited with non-zero status 1
issues/issue328.vo (real: 0.25, user: 0.16, sys: 0.08, mem: 286080 ko)
make[3]: *** [Makefile:833: issues/issue328.vo] Error 1
make[2]: *** [Makefile:417: all] Error 2
make[2]: Leaving directory '/github/workspace/builds/coq/coq-failing/_build_ci/equations/test-suite'
make[1]: *** [Makefile:36: test-suite] Error 2
make[1]: Leaving directory '/github/workspace/builds/coq/coq-failing/_build_ci/equations'
+ code=2
+ echo 'Aggregating timing log...'
Aggregating timing log...
+ echo

+ python ./tools/make-one-time-file.py --real equations_test.log
    Time |  Peak Mem | File Name            
--------------------------------------------
0m03.04s | 441776 ko | Total Time / Peak Mem
--------------------------------------------
0m02.53s | 441776 ko | Basics.vo            
0m00.26s | 318420 ko | issues/issue95_2.vo  
0m00.25s | 286080 ko | issues/issue328.vo   
+ '[' '' ']'
+ exit 2
make: *** [Makefile.ci:193: ci-equations_test] Error 2
/github/workspace/builds/coq /github/workspace
::endgroup::

📜 🔎 Minimization Log (truncated to last 8.0KiB; full 64KiB file on GitHub Actions Artifacts under bug.log)

uilds/coq/coq-passing/_build_ci/equations/test-suite TestSuite -R /github/workspace/builds/coq/coq-passing/_build_ci/equations/theories Equations -Q /github/workspace/cwd Top -Q /github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/user-contrib/Equations Equations -Q /github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/user-contrib/Ltac2 Ltac2 -I /github/workspace/builds/coq/coq-passing/_build_ci/equations/src -top issue328 -o /tmp/bug_01.vo -dump-glob bug_01.glob bug_01.v
getting bug_01.glob (/github/workspace/cwd/bug_01.glob)
getting bug_01.glob (/github/workspace/cwd/bug_01.glob)
�[92m
Succeeded in normalizing Requires.�[0m

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 (1711755012, 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.
�[92m
Splitting successful.�[0m

I will now attempt to remove any lines after the line which generates the error.

No lines to trim.

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...
�[92m
Splitting to definitions successful.�[0m

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions

Non-fatal error: Failed to remove definitions and preserve the error.  
The new error was:
File "/tmp/tmp9lydklq3/TestSuite/issues/issue328.v", line 5, characters 23-40:
Error: The reference the_equations_tag was not found in the current
environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions

Non-fatal error: Failed to remove non-instance definitions and preserve the error.  
The new error was:
File "/tmp/tmp9lydklq3/TestSuite/issues/issue328.v", line 5, characters 23-40:
Error: The reference the_equations_tag was not found in the current
environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to replace Qed Obligation with Admit Obligations
�[92m
Admitting Qed Obligations successful.�[0m
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
�[92m
Admitting Qeds successful.�[0m
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.
�[92m
Admitting Qeds successful.�[0m
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.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions

Non-fatal error: Failed to remove definitions and preserve the error.  
The new error was:
File "/tmp/tmp9lydklq3/TestSuite/issues/issue328.v", line 5, characters 23-40:
Error: The reference the_equations_tag was not found in the current
environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions

Non-fatal error: Failed to remove non-instance definitions and preserve the error.  
The new error was:
File "/tmp/tmp9lydklq3/TestSuite/issues/issue328.v", line 5, characters 23-40:
Error: The reference the_equations_tag was not found in the current
environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to admit [abstract ...]s
�[92m
Admitting [abstract ...] successful.�[0m
�[92m
Admitting [abstract ...] successful.�[0m
Admitting [abstract ...] unsuccessful.
Admitting [abstract ...] unsuccessful.

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions

Non-fatal error: Failed to remove definitions and preserve the error.  
The new error was:
File "/tmp/tmp9lydklq3/TestSuite/issues/issue328.v", line 5, characters 23-40:
Error: The reference the_equations_tag was not found in the current
environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions

Non-fatal error: Failed to remove non-instance definitions and preserve the error.  
The new error was:
File "/tmp/tmp9lydklq3/TestSuite/issues/issue328.v", line 5, characters 23-40:
Error: The reference the_equations_tag was not found in the current
environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to replace Obligation with Admit Obligations
�[92m
Admitting Obligations successful.�[0m
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
�[92m
Admitting lemmas successful.�[0m
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
�[92m
Admitting definitions successful.�[0m
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
�[92m
Admitting lemmas successful.�[0m
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
�[92m
Admitting definitions successful.�[0m
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.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions

Non-fatal error: Failed to remove definitions and preserve the error.  
The new error was:
File "/tmp/tmp9lydklq3/TestSuite/issues/issue328.v", line 5, characters 23-40:
Error: The reference the_equations_tag was not found in the current
environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions

Non-fatal error: Failed to remove non-instance definitions and preserve the error.  
The new error was:
File "/tmp/tmp9lydklq3/TestSuite/issues/issue328.v", line 5, characters 23-40:
Error: The reference the_equations_tag was not found in the current
environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

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...

No strippable newlines or 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.

Fix rocq-prover#18358 Fix rocq-prover#18680 Fix rocq-prover#18850

SkySkimmer · 2024-04-01T10:21:23Z

IDK what made that equations test start failing, AFAICT this PR shouldn't change what happens since equations called search_guard without evar handler. The overlay to make it work again looks more correct than the previous code so not spending much time on figuring it out.

ppedrot · 2024-04-04T08:53:49Z

@coqbot run full ci

ppedrot · 2024-04-05T09:19:10Z

@coqbot merge now

coqbot-app · 2024-04-05T09:19:14Z

@ppedrot: Please take care of the following overlays:

18864-SkySkimmer-check-guard-evars.sh

Adapt to rocq-prover/rocq#18864 (search_guard can handle evars)

…rocq#18864

SkySkimmer added 4 commits March 29, 2024 14:30

Remove deprecated functions in reduction.ml

e0534b6

Add optional ?evars argument to functions in reduction.ml

f5f78d9

Monomorphize cclosure.evar_handler

7655f3b

add ?evars argument to inductive.ml functions

b89e01f

SkySkimmer added kind: fix This fixes a bug or incorrect documentation. request: full CI Use this label when you want your next push to trigger a full CI. labels Mar 29, 2024

SkySkimmer requested review from a team as code owners March 29, 2024 13:59

coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 29, 2024

SkySkimmer added this to the 8.20+rc1 milestone Mar 29, 2024

SkySkimmer added a commit to SkySkimmer/Coq-Equations that referenced this pull request Apr 1, 2024

Adapt to rocq-prover/rocq#18864 (search_guard can handle evars)

7146740

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2024

Call guard checking with evar handlers in higher layers

354c1f4

Fix rocq-prover#18358 Fix rocq-prover#18680 Fix rocq-prover#18850

SkySkimmer force-pushed the check-guard-evars branch from 8b4c8b9 to 354c1f4 Compare April 1, 2024 10:19

coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2024

ppedrot self-assigned this Apr 1, 2024

ppedrot approved these changes Apr 1, 2024

View reviewed changes

coqbot-app bot merged commit 14ae18e into rocq-prover:master Apr 5, 2024

ppedrot added a commit to mattam82/Coq-Equations that referenced this pull request Apr 5, 2024

Merge pull request #587 from SkySkimmer/check-guard-evars

6010562

Adapt to rocq-prover/rocq#18864 (search_guard can handle evars)

SkySkimmer deleted the check-guard-evars branch April 5, 2024 10:23

blume0 mentioned this pull request May 28, 2025

Assertion error from cClosure.ml due to rocq-prover/rocq#16442 unicoq/unicoq#102

Open

blume0 added a commit to blume0/unicoq that referenced this pull request May 28, 2025

Fix unicoq#104 by adapting to rocq-prover/rocq#16442 and rocq-prover/…

1bb2e43

…rocq#18864

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Call guard checking with evar handlers in higher layers #18864

Call guard checking with evar handlers in higher layers #18864

Uh oh!

SkySkimmer commented Mar 29, 2024 •

edited

Loading

Uh oh!

coqbot-app bot commented Mar 29, 2024

Uh oh!

SkySkimmer commented Mar 29, 2024

Uh oh!

coqbot-app bot commented Mar 29, 2024

Uh oh!

coqbot-app bot commented Mar 29, 2024

Uh oh!

SkySkimmer commented Apr 1, 2024

Uh oh!

ppedrot commented Apr 4, 2024

Uh oh!

ppedrot commented Apr 5, 2024

Uh oh!

coqbot-app bot commented Apr 5, 2024

Uh oh!

Uh oh!

Call guard checking with evar handlers in higher layers #18864

Call guard checking with evar handlers in higher layers #18864

Uh oh!

Conversation

SkySkimmer commented Mar 29, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

coqbot-app bot commented Mar 29, 2024

Uh oh!

SkySkimmer commented Mar 29, 2024

Uh oh!

coqbot-app bot commented Mar 29, 2024

Uh oh!

coqbot-app bot commented Mar 29, 2024

Uh oh!

SkySkimmer commented Apr 1, 2024

Uh oh!

ppedrot commented Apr 4, 2024

Uh oh!

ppedrot commented Apr 5, 2024

Uh oh!

coqbot-app bot commented Apr 5, 2024

Uh oh!

Uh oh!

SkySkimmer commented Mar 29, 2024 •

edited

Loading