Remove Dyn.anonymous #18529
Merged
Remove Dyn.anonymous #18529
Conversation
This file contains 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
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
ejgallego
approved these changes
Jan 22, 2024
ppedrot
approved these changes
Jan 22, 2024
ppedrot
added
the
needs: overlay
SkySkimmer
added a commit
to SkySkimmer/coq-tactician
that referenced
this pull request
Jan 24, 2024
SkySkimmer
added a commit
to SkySkimmer/vscoq
that referenced
this pull request
Jan 24, 2024
SkySkimmer
added a commit
to SkySkimmer/coq-waterproof
that referenced
this pull request
Jan 24, 2024
The point of Dyn is to be stable across marshallings, but the ints generated for Dyn.anonymous are in general not stable across different plugin dynlink orders. Close coq#17109
SkySkimmer
added
request: full CI
SkySkimmer
force-pushed
the
dyn-no-anon
branch
from
b233085 to
b7a6641
Compare
coqbot-app
bot
removed
the
request: full CI
|
CI failure unrelated, so @coqbot merge now |
|
@ppedrot: Please take care of the following overlays:
|
ppedrot
added a commit
to coq/vscoq
that referenced
this pull request
Jan 28, 2024
Adapt to coq/coq#18529 (no Dyn.anonymous)
LasseBlaauwbroek
added a commit
to coq-tactician/coq-tactician
that referenced
this pull request
Jan 28, 2024
Adapt to coq/coq#18529 (no Dyn.anonymous)
jim-portegies
pushed a commit
to impermeable/coq-waterproof
that referenced
this pull request
Jan 28, 2024
rtetley
added a commit
to coq/vscoq
that referenced
this pull request
Feb 6, 2024
Fixing Coq pin in flake and adding correction to make coq master branch compile.
jellooo038
added a commit
to impermeable/coq-waterproof
that referenced
this pull request
Aug 20, 2024
* Changes for compatibility with 8.19 * Adapt files for the build process * Update README.md * Don't use opam to build and install for now * Adapt dune files to make build with dune possible * Change name field in dune file to Waterproof * Revert to dune language 3.6 * Remove line on theory Ltac2 * Adapt to coq/coq#17836 (sort poly) * Revert "Adapt to coq/coq#17836 (sort poly)" * Adapt to coq/coq#18174 (Clenv.unify takes cv_pb) * Adapt to coq/coq#17836 (sort poly) (#28) * Adapt to coq/coq#18280 (case relevance outside case info) (#37) * Merge features of version 2.1.1 into coq-master (#46) * [build] Initial port to Dune This was done at the interest of Vincent WENDLING for jsCoq use. The setup is fairly standard, other than excluding the deprecated dir (which doesn't compile) * Update README.md * Update dune file in theories * Change importing Ltac2 modules and build only with dune * Update version numbers * Restore changes file and rename license file * Fix metadata in files * Add template tags * Add @install, minimal dune version, dev-repo to opam file * Added infrastructure for enforcing users to mention use of definitions. * Removed some unnecessary lemma's and corresponding tactics (that were apparently throwing errors anyway). * Restored old lemmas in 'SupAndInf' necessary for keeping limsup file working. To be rewritten in future. * Moved tests in SupAndInf.v file to separate test file. Small bug fix in rewrite rule sup and infimum. * 'We need to show'-tactic now also accepts equivalent goals. Added 'By ...' clause to allow for an additional lemma from which equivalence follows. * Replaced use of 'it suffices to show' by 'we need to show' for unfolding definitions. * Added testcases new behaviour tactic. * Improved feedback given new restricted proof automation. * Updated documentation. * Small change in error message. * Moved 'AutomationFailure' exception type to 'Wateprove' file. * Improved feedback 'ItHolds' for new restricted proof automation. * Replaced custom error shielded goal by standard error that can be caught using Ltac2. * Added 'Since ...' clause as alternative to 'By ...' that accepts statements instead of references. (No 'Since ... we need to show ...' because the 'By'-version is to be removed soon. ) * Removed acceptation equivalent goals from 'We need to show' tactic. * Improved feedback 'By ... we conclude ...' for new restricted automated proof finding. Added 'Since ... we conclude that ...' alternative. * Improved feedback, now it says which part of a chain of (in)equalities it failed to prove. Refactored checking whether additional lemma is actually used: now check is done in 'Waterprove.v', it throws errors with relevant information that other tactics use to display user-readable errors. * 'Contradiction' now tries to find a contradiction to the previous statement. * Moved 'Obtain' tactic to separate file. * Simplified old notation 'Obtain' tactic. Now it automatically tries to destruct previous statement and users no longer need to specify the corresponding property. * Simplified names for hypotheses not labeled by user. * Added 'change' to 'Expand definition', so putting in different dummy variables actually has effect. * Added StateGoal wrappers to subgoals of non-natural induction. * Added workaround for unexpected anomalies in restricted automation. * Strengthened workaround. Both to prevent more anomalies with hypotheses and to prevent endless searching for proof with hypothesis because it is used implicitly by the 'assumption' tactic. * Replaced axiomatic definitions with locked ones. Also strengthened shielded automation to depth 3 to be able to use definition supremum.. * Fixed dune build. * feat: add warnings * refactor: change the names of the warning functions * feat: add error function * Add files to _CoqProject.in * feat: use the warning in Conclusion.v * feat: deal with Rabs Rmax Rmin more easily by destructing them * Readded shortened 'Obtain accoriding to ...' tactic. * Reworked shielding to use Shorten database type. Includes new tactics for explicitly unfolding definitions, optimized for speed automation (i.e. they explicitly fail to prevent large growth search tree). * Improved expanding def for sup and inf. * Implemented user-level error throwing in tactics. * Fixed small error from merge. * Disabled debug mode automation. * Reverted back to old SupAndInf.v file. * Replaced wrapping after 'Expand the definition of ...' by throwing errors suggesting user to replace the line by a tactic with a similar effect as unfolding the definitions. (Also slightly simplified notation base case natural induction.) * Added tactic for unfolding that prints a message instead of throwing an errror. For internal use by Waterproof editor only. * chore: bump version number * fix: add internal unfold for general terms and tests for internal unfold * Hint fixes (#30) fix: change hint priorities * Automation debug (#31) * fix: change hint priorities * fix: change hint priorities * fix: fight line endings * feat: add switch for debugging of the automation * feat: Add description on how to enable debugging to readme * feat: use N1 instead of N in definition convergence * Improve either (#32) * fix: definition of divergence to infinity and min infinity * feat: add double_is_even to wp_integers rather than subsequences * feat: let either work with uninformative or if the goal is a prop * feat: also separate either code for prop for three statements. Refactor some decidability statements * refactor: use new either code in alternative characterization of continuity in R * feat: add alternative characterization continuity for natural numbers as subset of metric space of reals * feat: some adaptations for the continuity exercises * chore: update changelog and bump version number in opam file * Tactics for using strong induction to define index sequence (#33) * Added strong induction for defining index sequence. Warning: uses fixed letters 'n' and 'k' for index sequence and induction variable. * Removed 'Check' and 'Print's. * Removed old code. * Show version number (#34) * feat: Add tactic to show version number * fix: Add version file to _CoqProject.in * Allow testing against a folder with dune's runtest and set version number (#35) * feat: add exercises as dune test * feat: add python script for testing * feat: abstract the testing scripts and deal with errors better * fix: call the correct test script * Set Help to use default automation system. (#36) * Change required version number * Try to fix coq requirement * Fix for problems with strong induction for defining index sequence. (#38) * Fix for problems with strong induction for defining subsequence. * Updated formatting goal wrapper. * fix: some small fixes to be compatible with dev * fix: change order fold_right arguments in index sequence * fix: Small changes to the sequences and subsequences files because autorewrite no longer seems to work as before * chore: Change version number * try to allow for dev version * fix: try with version numbers * fix: try to fix version numbers * fix: Remove unnecessary import in Sequences.v * feat: add logging sentence for wp_autorewrite * feat: add logging sentence for wp_autorewrite (#43) * feat: create option to print rewrite hints (#44) * fix: Fix autorewrite (the env variable didn't come through properly) * fix: Compatibility with compilers >= 4.09.0 (#45) * fix: Exclude s390x architecture * refactor: put *.install and *.diags in gitignore --------- Co-authored-by: Emilio Jesus Gallego Arias Co-authored-by: Jelle * Adapt to coq/coq#18327 (projection opacity) (#41) * Adapt to coq/coq#18529 (no Dyn.anonymous) (#47) * Adapt to coq/coq#18624 (Tac2ffi / Tac2val split) (#49) * Adapt to coq/coq#18546. (#48) * Adapt to coq/coq#18880 (#52) * Adapt to coq/coq#18938 (EConstr.ERelevance) (#53) * Update README.md Update installation instructions * Testmaster (#54) Implement a better way to do a case analyse on a type Co-authored-by: DikieDick * fix: Change 'Variable' to 'local Parameter' * feat: add a test for awp_autorewrite from coq-master * Refactor: incorporate some changes from 8.17 and update version numbers (#57) * [build] Fix use of plugin aliases in findlib loading. (#58) Note that both lines where loading the same plugin, but activating different syntax rules; that's not really allowed as it leaves the system in a partial state. If something like that is needed, true two plugins are necessary (Which is not hard to support nowadays). * feat: Postponing choices in the Choose tactic (#59) * Merge 8.17 into main (#61) Main change according to (PR #58): we only declare one plugin now. * Renamed variables to prevent having actual exercise solution in repo (#64) * Specialize (#51) * feat: first version of waterproof specialize tactic * feat: Improve new specialize tactic, so it throws an error when a wrong variable is getting introduced. * Avoid doubling hypothesis, allow for multiple binders, prevent matching on functions, rename hypothesis to user-specified one --------- Co-authored-by: Jelle <jellewemmenhove@live.nl> * feat: Postponing choices in the Choose tactic * No longer rename variables in exists-statements --------- Co-authored-by: Jelle <jellewemmenhove@live.nl> --------- Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> Co-authored-by: Rodolphe Lepigre <lepigre@mpi-sws.org> Co-authored-by: Pierre Roux <pierre.roux@onera.fr> Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org> Co-authored-by: Jelle <jellewemmenhove@live.nl>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
The point of Dyn is to be stable across marshallings, but the ints generated for Dyn.anonymous are in general not stable across different plugin dynlink orders.
Close #17109
Overlays: