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.

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

Remove uses of _tac methods from nondet #671

Merged
merged 1 commit into from
Oct 5, 2023

Conversation

corlewis
Copy link
Member

@corlewis corlewis commented Sep 29, 2023

In particular, try to remove as many _tac methods that refer to system-generated variable names as possible. Any remaining uses are explicitly protected by a rename_tac.

@corlewis corlewis self-assigned this Sep 29, 2023
Copy link
Member

@lsf37 lsf37 left a comment

Choose a reason for hiding this comment

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

Nice, these are pretty much all improvements. I don't have a very good solution for the second apply followed by proof bit. That one might need a bit more experimentation.

lib/Monads/nondet/Nondet_Det.thy Show resolved Hide resolved
lib/Monads/nondet/Nondet_More_VCG.thy Outdated Show resolved Hide resolved
lib/Monads/nondet/Nondet_More_VCG.thy Outdated Show resolved Hide resolved
lib/Monads/nondet/Nondet_While_Loop_Rules.thy Outdated Show resolved Hide resolved
lib/Monads/nondet/Nondet_While_Loop_Rules.thy Outdated Show resolved Hide resolved
lib/Monads/nondet/Nondet_While_Loop_Rules_Completeness.thy Outdated Show resolved Hide resolved
@Xaphiosis
Copy link
Member

I'm fine with this, no further review comments. Not sure what the motivation for it was, AFP requirements?

@corlewis corlewis changed the base branch from corlewis-nondet_more_changes to master October 5, 2023 01:01
@lsf37
Copy link
Member

lsf37 commented Oct 5, 2023

I'm fine with this, no further review comments. Not sure what the motivation for it was, AFP requirements?

Yes, AFP requirements

In particular, try to remove as many as possible _tac methods that refer
to system-generated variable names. Any remaining uses are explicitly
protected by a rename_tac.

Signed-off-by: Corey Lewis <[email protected]>
@corlewis corlewis merged commit 34038fc into seL4:master Oct 5, 2023
13 checks passed
@corlewis corlewis deleted the nondet_remove_tac branch October 5, 2023 11:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants