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

feat: Don't force :extern members to be implemented in derived classes #2446

Merged
merged 9 commits into from
Jul 22, 2022

Conversation

cpitclaudel
Copy link
Member

Closes #2212.

@cpitclaudel cpitclaudel force-pushed the cpitclaudel_extern-in-trait-2212 branch from 2981e9e to 56f7650 Compare July 21, 2022 00:53
@fabiomadge fabiomadge added the run-deep-tests Tells CI to run all tests label Jul 21, 2022
fabiomadge
fabiomadge previously approved these changes Jul 21, 2022
Comment on lines +9389 to +9390
// Extern functions do not need to be reimplemented.
// TODO: When `:extern` is separated from `:compile false`, this should become `:compile false`.
Copy link
Collaborator

Choose a reason for hiding this comment

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

Should we add this to the SinglePassCompiler as well?

Source/Dafny/Compilers/SinglePassCompiler.cs Show resolved Hide resolved
Test/comp/ExternCopyFromTrait.dfy Outdated Show resolved Hide resolved
Test/comp/ExternCopyFromTrait.dfy Outdated Show resolved Hide resolved
@cpitclaudel cpitclaudel enabled auto-merge (squash) July 22, 2022 07:36
@fabiomadge fabiomadge removed the run-deep-tests Tells CI to run all tests label Jul 22, 2022
@cpitclaudel cpitclaudel merged commit c5cd1fd into master Jul 22, 2022
@cpitclaudel cpitclaudel deleted the cpitclaudel_extern-in-trait-2212 branch July 22, 2022 15:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Feature request: ignore {:extern} method in trait
2 participants