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

Compilation to not use a global local variable counter, but a local one #5330

Open
MikaelMayer opened this issue Apr 17, 2024 · 1 comment
Open
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny

Comments

@MikaelMayer
Copy link
Member

Summary

I want counters on generated variables be local, not global

Background and Motivation

Currently, to prevent shadowing from hurting compilers, we append a global counter to local variables.
However, at least in C#, when generating the code, the counters are shared across modules, which makes it that half of the modules change if one module is updated. This prevents compilation optimizations.

Proposed Feature

Reset to zero the global counter variable when resolving when entering a module

Alternatives

N/A

@MikaelMayer MikaelMayer added the kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny label Apr 17, 2024
@MikaelMayer
Copy link
Member Author

This is harder than it seems because compile names are currently assigned. lazily

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Projects
None yet
Development

No branches or pull requests

1 participant