Janno/test 21247#2
Draft
Janno wants to merge 151 commits into
Draft
Conversation
(cherry picked from commit 1a7d060)
- force printing universes on to avoid printing sort variables as Type - add quotes - more intentional break hints and slightly improve wording Close rocq-prover#20722 (cherry picked from commit ac6e253)
…or message (with elim constraints)
(cherry picked from commit 8001204)
We don't use this script for master so we could also remove this check (cherry picked from commit 1641e74)
…c hypotheses (where &id is static)
(cherry picked from commit d3976ee)
This prevents rocqtop to display many warnings in the refman. (cherry picked from commit 4c59526)
(cherry picked from commit 8837689)
(cherry picked from commit 912b88b)
Fix rocq-prover#20582 (cherry picked from commit 48137f5)
…nts in ssr saturate
(cherry picked from commit b7dfa70)
(cherry picked from commit d5e4ad2)
(cherry picked from commit 7c523af)
(cherry picked from commit a0ffec9)
…ing the stack as in check_one_fix
…ning. The previous code was only substituting the inner delta resolvers and ignoring the codomain of functors. In particular this was generating ill-formed constants whose canonical component was pointing to a bound name that did not exist in the global environment. We fix the code by also substituting the codomain of module bodies. This is actually in line with what we do in the related function strengthen_and_subst_module_body, where we were also correctly substituting the codomain. This is a quite old soundness bug that was also affecting the checker. It seems to have been introduced by c5b699f by an oversight when refactoring tricky code. Fixes rocq-prover#21051: Unsoundness with heavy module machinery. (cherry picked from commit daa20b9)
(cherry picked from commit 56bbb9b)
…lvers when performing strengthening
(cherry picked from commit 7019882)
(cherry picked from commit 58ffc96)
The other URLs are still using "coq" in 9.1 but not in master
With corelib being small now, there is no real point in trying to build just the prelude instead of world. Consequently these scripts have become unmaintained (in my experience) and are not worth keeping.
There is no real point in exposing this implementation detail, all callers immediately evaluate the resulting thunk.
We leverage the fact that a ~> unit -> b ≅ a -> b where ~> stands for a hypothetical pure arrow type. This allows replacing all instances of the NonLogical.t monad in the logic monad type with basically nothing, leaving effects implicits in the rightmost arrow type. Since all clients evaluate the thunk directly, the new code should be equivalent to the previous one. Actually, it may even be more correct given that we already implicitly use the function space in the monadic bind operator to perform side-effects.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
rlepigre-skylabs-ai
force-pushed
the
skylabs-master
branch
from
2ede3c9 to
bef7df5
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
14 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Benchmark rocq-prover#21247