Skip to content
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

Obligations, Proof, Hint Extern, tactic option commands do not depend on ltac1 #19690

Open
wants to merge 13 commits into
base: master
Choose a base branch
from
Open

Obligations, Proof, Hint Extern, tactic option commands do not depend on ltac1 #19690

wants to merge 13 commits into from
+417 −222

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Oct 14, 2024 •
edited
Loading

Some parts of the code already use genargs to handle tactic expressions without depending on ltac1, eg the implementation of obligations.
We expand on this and provide a grammar entry generic_tactic which produces those genargs depending on the current default proof mode.

Overlays:

Backward compatible overlays:

@SkySkimmer SkySkimmer added kind: documentation Additions or improvement to documentation. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: changelog entry This should be documented in doc/changelog. request: full CI Use this label when you want your next push to trigger a full CI. labels Oct 14, 2024
@SkySkimmer SkySkimmer added this to the 9.0+rc1 milestone Oct 14, 2024
@SkySkimmer SkySkimmer requested review from a team as code owners October 14, 2024 14:49
@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 Oct 14, 2024
SkySkimmer
SkySkimmer commented Oct 14, 2024
View reviewed changes
tactics/gentactic.mli Outdated
Comment on lines 33 to 38
val intern : Environ.env -> ?ltacvars:Id.Set.t -> raw_generic_tactic -> glob_generic_tactic

val interp : ?lfun:Geninterp.Val.t Id.Map.t -> glob_generic_tactic -> unit Proofview.tactic
Copy link
Contributor Author

Choose a reason for hiding this comment

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

The handling of the extra variables could be improved, currently ltac2 simply ignores them.

@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Oct 15, 2024
SkySkimmer added a commit to SkySkimmer/neural-net-coq-interp that referenced this pull request Oct 15, 2024
@SkySkimmer
Adapt to coq/coq#19690 (Hint Extern respects default proof mode)

Verified

This commit was signed with the committer’s verified signature. The key has expired.
yinzara Matthew Vance
GPG key ID: 579D870DC9FFBCDE
Expired
Verified
Learn about vigilant mode
5e187e8
SkySkimmer added a commit to SkySkimmer/rupicola that referenced this pull request Oct 15, 2024
@SkySkimmer
Adapt to coq/coq#19690 (Hint Extern respects default proof mode)

Verified

This commit was signed with the committer’s verified signature. The key has expired.
yinzara Matthew Vance
GPG key ID: 579D870DC9FFBCDE
Expired
Verified
Learn about vigilant mode
Loading
Loading status checks…
1c9562e
SkySkimmer added a commit to SkySkimmer/Mtac2 that referenced this pull request Oct 15, 2024
@SkySkimmer
Adapt to coq/coq#19690 (proof mode needs a genarg for tactics inlined…
e3e439d 
… in commands)
SkySkimmer added a commit to SkySkimmer/paramcoq that referenced this pull request Oct 15, 2024
@SkySkimmer
Adapt to coq/coq#19690 (generic_tactic avoids dependency on ltac(?))
f335b8e
SkySkimmer added a commit to SkySkimmer/coq-waterproof that referenced this pull request Oct 15, 2024
@SkySkimmer
Adapt to coq/coq#19690 (Hint Extern respects default proof mode)
Loading
Loading status checks…
dfbb8fd
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. needs: documentation Documentation was not added or updated. and removed kind: documentation Additions or improvement to documentation. labels Oct 15, 2024
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Oct 15, 2024
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 15, 2024
@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 Oct 15, 2024
SkySkimmer added a commit to SkySkimmer/coq-waterproof that referenced this pull request Mar 11, 2025
@SkySkimmer
Adapt to coq/coq#19690 (Hint Extern respects default proof mode)
Loading
Loading status checks…
707d53f
SkySkimmer added a commit to SkySkimmer/coq-waterproof that referenced this pull request Mar 11, 2025
@SkySkimmer
Adapt to coq/coq#19690 (Hint Extern respects default proof mode)
Loading
Loading status checks…
585b1c6
SkySkimmer added a commit to SkySkimmer/coq-waterproof that referenced this pull request Mar 11, 2025
@SkySkimmer
Adapt to coq/coq#19690 (Hint Extern respects default proof mode)
Loading
Loading status checks…
d073788
SkySkimmer added a commit to SkySkimmer/coq-tactician that referenced this pull request Mar 11, 2025
@SkySkimmer
Adapt to coq/coq#19690 (register_proof_mode is mode than the command …
Loading
Loading status checks…
ced3f47 
…entry)
SkySkimmer added a commit to SkySkimmer/coq-lsp that referenced this pull request Mar 11, 2025
@SkySkimmer
Adapt to coq/coq#19690 (gentactic)
ab3a11c
SkySkimmer added a commit to SkySkimmer/coq-lsp that referenced this pull request Mar 11, 2025
@SkySkimmer
Adapt to coq/coq#19690 (gentactic)
448f1dc
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: documentation Documentation was not added or updated. needs: changelog entry This should be documented in doc/changelog. labels Mar 11, 2025
SkySkimmer added a commit to SkySkimmer/rewriter that referenced this pull request Mar 11, 2025
@SkySkimmer
Adapt to coq/coq#19690 (Hint Extern follows default proof mode)
4cc49a3
@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 Mar 11, 2025
@SkySkimmer
Copy link
Contributor Author

Should be ready, can I get an assignee? Maybe @ppedrot

@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Mar 11, 2025
@SkySkimmer
Copy link
Contributor Author

unimath failure is spurious, fiat crypto isn't

SkySkimmer added a commit to SkySkimmer/fiat-crypto that referenced this pull request Mar 12, 2025
@SkySkimmer
Adapt to coq/coq#19690 (Hint Extern follows proof mode)
Loading
Loading status checks…
d2fb128
SkySkimmer added a commit to SkySkimmer/fiat-crypto that referenced this pull request Mar 12, 2025
@SkySkimmer
Adapt to coq/coq#19690 (Hint Extern follows proof mode)
Loading
Loading status checks…
87684fe
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: overlay This is breaking external developments we track in CI. labels Mar 12, 2025
@SkySkimmer
overlays for generic_tactic
Loading
Loading status checks…
13aca15
@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 Mar 12, 2025
JasonGross pushed a commit to mit-plv/rewriter that referenced this pull request Mar 12, 2025
@SkySkimmer
Adapt to coq/coq#19690 (Hint Extern follows default proof mode) (#171)
Loading
Loading status checks…
e8da092
JasonGross pushed a commit to JasonGross/neural-net-coq-interp that referenced this pull request Mar 12, 2025
@SkySkimmer
Adapt to coq/coq#19690 (Hint Extern respects default proof mode) (#67)
Loading
Loading status checks…
7e0c381
samuelgruetter added a commit to mit-plv/rupicola that referenced this pull request Mar 12, 2025
@samuelgruetter
Merge pull request #132 from SkySkimmer/ltacX-obligations
Loading
Loading status checks…
00778a5 
Adapt to coq/coq#19690 (Hint Extern respects default proof mode)
JasonGross pushed a commit to mit-plv/fiat-crypto that referenced this pull request Mar 13, 2025
@SkySkimmer
Adapt to coq/coq#19690 (Hint Extern follows proof mode) (#2058)
Loading
Loading status checks…
ce9e409
@ppedrot ppedrot self-assigned this Mar 20, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jfehrle jfehrle

At least 1 approving review is required to merge this pull request.

Assignees

@ppedrot ppedrot

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc.
Projects
None yet
Milestone
9.1+rc1
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@SkySkimmer @jfehrle @ppedrot