8000 Push Library.indirect_accessor references up in the call stack by SkySkimmer · Pull Request #18422 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Push Library.indirect_accessor references up in the call stack #18422

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 6 commits into from
Apr 7, 2024
Merged

Push Library.indirect_accessor references up in the call stack #18422

merged 6 commits into from
Apr 7, 2024

Conversation

SkySkimmer
Copy link
Contributor
@SkySkimmer SkySkimmer commented Dec 19, 2023 •
edited
Loading

@SkySkimmer SkySkimmer added kind: cleanup Code removal, deprecation, refactorings, etc. request: full CI Use this label when you want your next push to trigger a full CI. labels Dec 19, 2023
@SkySkimmer SkySkimmer requested review from a team as code owners December 19, 2023 14:01
@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 Dec 19, 2023
@ejgallego ejgallego self-assigned this Dec 19, 2023
@ejgallego ejgallego added this to the 8.20+rc1 milestone Dec 19, 2023
@ejgallego ejgallego added part: extraction The extraction mechanism. part: vernac High level command interpretation. needs: overlay This is breaking external developments we track in CI. labels Dec 19, 2023
@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 Jan 10, 2024
@coqbot-app coqbot-app bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Jan 26, 2024
SkySkimmer
SkySkimmer commented Jan 26, 2024
View reviewed changes
plugins/extraction/g_extraction.mlg Outdated
@@ -60,6 +60,8 @@ let pr_language = function
| Scheme -> str "Scheme"
| JSON -> str "JSON"

let access = Library.indirect_accessor[@@warning "-3"]
Copy link
Contributor Author

Choose a reason for hiding this comment

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

This is not very satisfying IMO, I'll probably wait for a better solution before doing overlays (probably after #18421 is merged)

Copy link
Member

Choose a reason for hiding this comment

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

I'm OK with this, but indeed it'd be good to head towards a more principled solution.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

TBH I don't want to do this for the overlays so this PR is waiting for the more principled solution.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

step towards making it possible #18832

@SkySkimmer SkySkimmer added the needs: progress Work in progress: awaiting action from the author. label Feb 5, 2024
@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 Feb 19, 2024
@coqbot-app coqbot-app
Copy link
Contributor
coqbot-app bot commented Mar 20, 2024

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

@coqbot-app coqbot-app bot added the stale This PR will be closed unless it is rebased. label Mar 20, 2024
@ejgallego
Copy link
Member

Happy to help with this (overlays and vernac types) if you need a hand @SkySkimmer

@coqbot-app coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. labels Mar 21, 2024
SkySkimmer added a commit to SkySkimmer/Coq-Equations that referenced this pull request Mar 22, 2024
@SkySkimmer
Don't pierce Qed in debug message (adapt to rocq-prover/rocq#18422)
eba7646
SkySkimmer added a commit to SkySkimmer/paramcoq that referenced this pull request Mar 22, 2024
@SkySkimmer
Adapt to rocq-prover/rocq#18422 (indirect accessor handled through ve…
faa9d3c 
…rnactypes)
SkySkimmer added a commit to SkySkimmer/coq-simple-io that referenced this pull request Mar 22, 2024
@SkySkimmer
Adapt to rocq-prover/rocq#18422 (indirect accessor handled through ve…
e81e10e 
…rnactypes)
@SkySkimmer
Use vernactypes to get indirect accessor in commands
0d768dc 
The indirect accessor is still directly used in

- dev/base_include (Drop stuff)
- stm/stm (accessing the local opaques to get the just-now-defined body,
  probably could be written in a more direct way)
- toplevel/coqc (-output-context)
@SkySkimmer
Update comment in stm
d39d3b4
@SkySkimmer
overlay for deprecated Library.indirect_accessor
495379b
SkySkimmer added a commit to SkySkimmer/MetaRocq that referenced this pull request Apr 5, 2024
@SkySkimmer
Adapt to rocq-prover/rocq#18422 (indirect accessor handled through ve…
142cff1 
…rnactypes)
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: discussion Further discussion is needed. needs: overlay This is breaking external developments we track in CI. labels Apr 5, 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: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Apr 5, 2024
@SkySkimmer
Copy link
Contributor Author

metacoq overlay done

ejgallego
ejgallego approved these changes Apr 5, 2024
View reviewed changes
Copy link
Member
@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

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

Great!

@ejgallego ejgallego added the kind: internal API, ML documentation... label Apr 5, 2024
@ejgallego
Copy link
Member

@coqbot: merge now

@coqbot-app coqbot-app bot merged commit c481f44 into rocq-prover:master Apr 7, 2024
@coqbot-app coqbot-app
Copy link
Contributor
coqbot-app bot commented Apr 7, 2024

@ejgallego: Please take care of the following overlays:

  • 18422-SkySkimmer-indirect.sh

ejgallego added a commit to rocq-archive/coq-serapi that referenced this pull request Apr 7, 2024
@ejgallego
Merge pull request #401 from SkySkimmer/indirect
7bea13d 
Adapt to rocq-prover/rocq#18422 (indirect accessor handled through vernactypes)
ppedrot added a commit to MetaRocq/metarocq that referenced this pull request Apr 7, 2024
@ppedrot
Merge pull request #1074 from SkySkimmer/indirect
9aa9086 
Adapt to rocq-prover/rocq#18422 (indirect accessor handled through vernactypes)
ppedrot added a commit to rocq-community/paramcoq that referenced this pull request Apr 7, 2024
@ppedrot
Merge pull request #121 from SkySkimmer/indirect
4eba947 
Adapt to rocq-prover/rocq#18422 (indirect accessor handled through vernactypes)
ejgallego pushed a commit to SkySkimmer/coq-lsp that referenced this pull request Apr 7, 2024
@SkySkimmer @ejgallego
Adapt to rocq-prover/rocq#18422 (indirect accessor handled through ve…
4bc0355 
…rnactypes)
ejgallego pushed a commit to SkySkimmer/coq-lsp that referenced this pull request Apr 7, 2024
@SkySkimmer @ejgallego
Adapt to rocq-prover/rocq#18422 (indirect accessor handled through ve…
46799a4 
…rnactypes)
SkySkimmer added a commit to SkySkimmer/vscoq that referenced this pull request Apr 7, 2024
@SkySkimmer
Adapt to rocq-prover/rocq#18422 (indirect accessor handled through ve…
7756152 
…rnactypes)
SkySkimmer added a commit to ejgallego/coq-lsp that referenced this pull request Apr 7, 2024
@SkySkimmer
Merge pull request #659 from SkySkimmer/indirect
21de511 
Adapt to rocq-prover/rocq#18422 (indirect accessor handled through vernactypes)
liyishuai pushed a commit to SkySkimmer/coq-simple-io that referenced this pull request Apr 7, 2024
@SkySkimmer @liyishuai
Adapt to rocq-prover/rocq#18422 (indirect accessor handled through ve…
74c44e3 
…rnactypes)
Lysxia pushed a commit to Lysxia/coq-simple-io that referenced this pull request Apr 8, 2024
@SkySkimmer @Lysxia
Adapt to rocq-prover/rocq#18422 (indirect accessor handled through ve…
cf3bd1f 
…rnactypes)
rtetley pushed a commit to SkySkimmer/vscoq that referenced this pull request Apr 8, 2024
@SkySkimmer @rtetley
Adapt to rocq-prover/rocq#18422 (indirect accessor handled through ve…
7531ba1 
…rnactypes)
rtetley added a commit to rocq-prover/vsrocq that referenced this pull request Apr 8, 2024
@rtetley
Merge pull request #756 from SkySkimmer/indirect
50b2913 
Adapt to rocq-prover/rocq#18422 (indirect accessor handled through vernactypes)
Lysxia pushed a commit to SkySkimmer/QuickChick that referenced this pull request Apr 8, 2024
@SkySkimmer @Lysxia
(CHEATING) Adapt to rocq-prover/rocq#18422 (indirect accessor handled…
1271572 
… through vernactypes)

Not sure we want to allow opaque access through tactics.
liyishuai pushed a commit to QuickChick/QuickChick that referenced this pull request Apr 8, 2024
@SkySkimmer @liyishuai
(CHEATING) Adapt to rocq-prover/rocq#18422 (indirect accessor handled…
ad3279c 
… through vernactypes)

Not sure we want to allow opaque access through tactics.
@SkySkimmer SkySkimmer deleted the indirect branch April 15, 2024 11:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ejgallego ejgallego ejgallego approved these changes

Assignees

@ejgallego ejgallego

Labels
kind: cleanup Code removal, deprecation, refactorings, etc. kind: internal API, ML documentation... part: extraction The extraction mechanism. part: vernac High level command interpretation.
Projects
Proof Handling
Status: Done
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.
6 participants
@SkySkimmer @ejgallego @Lysxia @ppedrot @herbelin @mattam82
0