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 verify and compile fields from modules to enable caching parsing #4058

Merged

Conversation

keyboardDrummer
Copy link
Member

@keyboardDrummer keyboardDrummer commented May 22, 2023

Changes

  1. Modules no longer contain properties that indicate whether they should be verified and/or compiled, which is required for the upcoming change to cache parsing.

  2. The API of Parser is simplified, so it always takes a TextReader as input.

  3. Change SourceProcessor so it doesn't need to open a file separately to determine what newlines it has, but can instead ride on the existing TextReader that is also used for parsing the file.

Testing

The above is purely refactoring, so no test changes have been made.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@keyboardDrummer keyboardDrummer requested review from robin-aws and alex-chew and removed request for robin-aws May 22, 2023 09:09
Source/DafnyCore/DafnyFile.cs Show resolved Hide resolved
Source/DafnyCore/DafnyMain.cs Show resolved Hide resolved
Source/DafnyCore/AST/ShouldCompileOrVerify.cs Show resolved Hide resolved
Source/DafnyDriver/DafnyDriver.cs Show resolved Hide resolved
Copy link
Contributor

@alex-chew alex-chew left a comment

Choose a reason for hiding this comment

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

LGTM. Thanks for splitting this out into a separate PR!

@keyboardDrummer keyboardDrummer merged commit 4ea662b into dafny-lang:master May 23, 2023
@keyboardDrummer keyboardDrummer deleted the justNoVerifyAndCompileFields branch May 23, 2023 19:41
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.

2 participants