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

Cache parsing #4085

Merged
merged 96 commits into from
May 31, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
96 commits
Select commit Hold shift + click to select a range
148a2fd
Remove verify and compile fields from modules to enable caching parsing
keyboardDrummer May 22, 2023
c9c071d
Fix test
keyboardDrummer May 22, 2023
1b1908b
Add TODOs
keyboardDrummer May 22, 2023
3f0b3c5
Return a module after parsing, insteadf of mutating one
keyboardDrummer May 22, 2023
6201104
7 server tests fail after merging CLI and server parsing code
keyboardDrummer May 22, 2023
8bc4492
Only one failing integration test
keyboardDrummer May 23, 2023
7b878b3
Get last language server test to pass
keyboardDrummer May 23, 2023
fef7ae1
Test fixes
keyboardDrummer May 23, 2023
234423e
Test generation tests now pass
keyboardDrummer May 23, 2023
d43a210
Fix bug and correctly set parent relationships when merging FileModul…
keyboardDrummer May 23, 2023
7141154
Fix clone method of ModuleDefinition
keyboardDrummer May 23, 2023
42041b6
Complete ModuleDefinition clone function
keyboardDrummer May 23, 2023
087b5fc
Lots of changes to resolve issues around the default class
keyboardDrummer May 23, 2023
0dbd1ce
Bugfixes
keyboardDrummer May 23, 2023
1c9d845
Merge remote-tracking branch 'origin/master' into justNoVerifyAndComp…
keyboardDrummer May 23, 2023
7c195b1
Merge remote-tracking branch 'fork/justNoVerifyAndCompileFields' into…
keyboardDrummer May 23, 2023
768404a
Merge commit '4ea662bce05e6' into pureParseFunction
keyboardDrummer May 23, 2023
9629518
Merge remote-tracking branch 'origin/master' into pureParseFunction
keyboardDrummer May 23, 2023
8b20527
Several bugfixes and workarounds
keyboardDrummer May 24, 2023
8d0fc92
Cloner and other fixes
keyboardDrummer May 24, 2023
bc09b4f
Fix compilation module cloning bug
keyboardDrummer May 24, 2023
02f55cc
Fix move declarations bug
keyboardDrummer May 24, 2023
4b9493f
Change the StartToken of the FileModuleDefinition so it's an actual t…
keyboardDrummer May 24, 2023
acc76d2
Fix refinement transformer code using pointers
keyboardDrummer May 24, 2023
151b6bf
Fix transcripts
keyboardDrummer May 24, 2023
96366cf
Let module.RangeToken.StartToken also include the include directives …
keyboardDrummer May 24, 2023
4592b19
add missing pointer file
keyboardDrummer May 24, 2023
bda14d4
Do not parse libraries twice when they're also in an include directive
keyboardDrummer May 24, 2023
76b4929
Fix bug in FormatterTestBase
keyboardDrummer May 24, 2023
55b2bbb
More passing formatter tests
keyboardDrummer May 24, 2023
4b1f763
Add another call to SetMembersBeforeResolution
keyboardDrummer May 24, 2023
285dd91
Formatting fixes and ran formatter
keyboardDrummer May 24, 2023
021d491
Merge remote-tracking branch 'origin/master' into pureParseFunction
keyboardDrummer May 25, 2023
244d11c
Fix tests and small Uri fix
keyboardDrummer May 25, 2023
ebb1150
Turn off direct test running
keyboardDrummer May 25, 2023
3fce874
Fix some allocation tests
keyboardDrummer May 25, 2023
c06abb1
Fix project file output writing
keyboardDrummer May 25, 2023
33dc99c
Test fixes, resolve TODO, and small refactoring
keyboardDrummer May 25, 2023
c6fcf22
Cleanup
keyboardDrummer May 25, 2023
3e2bca0
Turn off direct test invocation
keyboardDrummer May 25, 2023
5d3c38e
Fix errors
keyboardDrummer May 25, 2023
e8987a2
Put ErrorReporter in parse result
keyboardDrummer May 25, 2023
f3ddf7b
Only trigger error for included file for actual errors in the include…
keyboardDrummer May 25, 2023
1328136
No longer modify Builtins during parsing
keyboardDrummer May 25, 2023
bc7aa30
Merge branch 'master' into reallyPureParseFunction
keyboardDrummer May 25, 2023
9b8bf01
Adding the cache
keyboardDrummer May 25, 2023
d30aa54
Cleanup
keyboardDrummer May 25, 2023
ef635b3
Fix error ordering and update test expect files
keyboardDrummer May 26, 2023
047f9a0
Merge branch 'reallyPureParseFunction' of github.com:keyboardDrummer/…
keyboardDrummer May 26, 2023
52470e9
Merge branch 'pureParseFunction' into reallyPureParseFunction
keyboardDrummer May 26, 2023
167b6b8
Merge commit '3e555a0ec048~1' into reallyPureParseFunction
keyboardDrummer May 26, 2023
78b9b1e
Merge commit '3e555a0ec048' into reallyPureParseFunction
keyboardDrummer May 26, 2023
b6c457c
Merge remote-tracking branch 'origin/master' into reallyPureParseFunc…
keyboardDrummer May 26, 2023
428cc85
Small refactoring and test fixes
keyboardDrummer May 26, 2023
ec6abb1
Add parse caching
keyboardDrummer May 26, 2023
436f855
Merge commit '428cc8567' into cacheParsing2
keyboardDrummer May 26, 2023
0835f3e
Merge commit 'a8d2cfd0' into cacheParsing2
keyboardDrummer May 26, 2023
f9d1219
Clone declarartions after they're retrieved from the cache
keyboardDrummer May 26, 2023
6ab2771
Run formatter
keyboardDrummer May 26, 2023
f335c38
Bring back lost logging
keyboardDrummer May 26, 2023
8454b57
Merge branch 'master' into cacheParsing2
keyboardDrummer May 26, 2023
74152e7
Add tests for errors inside included files
keyboardDrummer May 26, 2023
b50318c
Fix warning
keyboardDrummer May 26, 2023
c43aa13
Merge branch 'cacheParsing2' of github.com:keyboardDrummer/dafny into…
keyboardDrummer May 26, 2023
1801a3c
Merge branch 'master' into cacheParsing2
keyboardDrummer May 26, 2023
a9ac9e4
Merge remote-tracking branch 'origin/master' into cacheParsing2
keyboardDrummer May 30, 2023
1eb1f77
Fix empty document issue
keyboardDrummer May 30, 2023
aa6fac2
Fix hashing bug, add Uri to hash, don't mutate the cached file, and i…
keyboardDrummer May 30, 2023
a411fc0
Merge branch 'master' into cacheParsing2
keyboardDrummer May 30, 2023
a33df95
Fix expression cloning
keyboardDrummer May 30, 2023
f7e436a
Fix cloning of RangeToken for Expressions
keyboardDrummer May 30, 2023
2e32698
Merge branch 'cacheParsing2' of github.com:keyboardDrummer/dafny into…
keyboardDrummer May 30, 2023
5e81b72
Merge remote-tracking branch 'origin/master' into cacheParsing2
keyboardDrummer May 30, 2023
7c6c029
Add additional caching test
keyboardDrummer May 30, 2023
a8b3647
Fix test
keyboardDrummer May 30, 2023
4c05670
Add comments
keyboardDrummer May 30, 2023
3b8fbe9
Add fixes and parse time telemetry
keyboardDrummer May 30, 2023
02d62d8
Fixes
keyboardDrummer May 31, 2023
285552f
Fix cloner bugs
keyboardDrummer May 31, 2023
16dda1e
Merge branch 'master' into cacheParsing2
keyboardDrummer May 31, 2023
ada233d
Add the Uri to the parse time telemetry
keyboardDrummer May 31, 2023
61038d3
Merge remote-tracking branch 'origin/master' into cacheParsing2
keyboardDrummer May 31, 2023
2b723db
Merge branch 'cacheParsing2' of github.com:keyboardDrummer/dafny into…
keyboardDrummer May 31, 2023
21741ae
Merge branch 'master' into cacheParsing2
keyboardDrummer May 31, 2023
0b3bbfe
Add more tests, fix bug in TextReaderFromCharArrays
keyboardDrummer May 31, 2023
552330d
Documentation changes
keyboardDrummer May 31, 2023
fc80872
Update docs/dev/news/4083.feat
keyboardDrummer May 31, 2023
358f80c
Update docs/dev/news/4085.feat
keyboardDrummer May 31, 2023
570652c
Code review
keyboardDrummer May 31, 2023
39af210
Merge branch 'cacheParsing2' of github.com:keyboardDrummer/dafny into…
keyboardDrummer May 31, 2023
f7d939e
Merge branch 'master' into cacheParsing2
keyboardDrummer May 31, 2023
0fb915c
Update Source/DafnyLanguageServer/Language/CachingParser.cs
keyboardDrummer May 31, 2023
7a87f38
Update Source/DafnyLanguageServer/Caching/TextReaderFromCharArrays.cs
keyboardDrummer May 31, 2023
4cb8cab
Add tests and fixes to TextReaderFromCharArrays
keyboardDrummer May 31, 2023
d9f93c7
Merge branch 'cacheParsing2' of github.com:keyboardDrummer/dafny into…
keyboardDrummer May 31, 2023
3e8b722
Merge branch 'master' into cacheParsing2
keyboardDrummer May 31, 2023
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion Source/DafnyCore.Test/DooFileTest.cs
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
using Microsoft.Dafny;
using Microsoft.Extensions.Logging;
using Microsoft.Extensions.Logging.Abstractions;
using Tomlyn;

namespace DafnyCore.Test;
Expand Down Expand Up @@ -33,7 +35,7 @@ private static Program ParseProgram(string dafnyProgramText, DafnyOptions option
var rootUri = new Uri(fullFilePath);
Microsoft.Dafny.Type.ResetScopes();
var errorReporter = new ConsoleErrorReporter(options);
var program = ParseUtils.Parse(dafnyProgramText, rootUri, errorReporter);
var program = new ProgramParser().Parse(dafnyProgramText, rootUri, errorReporter);
Assert.Equal(0, errorReporter.ErrorCount);
return program;
}
Expand Down
3 changes: 3 additions & 0 deletions Source/DafnyCore/AST/BuiltIns.cs
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,9 @@ public static Attributes AxiomAttribute() {
return new Attributes("axiom", new List<Expression>(), null);
}

/// <summary>
/// Ensures this instance contains the requested type
/// </summary>
public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass) {
Contract.Requires(1 <= dims);
Contract.Requires(arg != null);
Expand Down
194 changes: 53 additions & 141 deletions Source/DafnyCore/AST/Cloner.cs

Large diffs are not rendered by default.

Loading