Break up dafny ast

[keyboardDrummer]

Break up DafntyAst.cs into smaller chunks that Rider can process well.

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

[cpitclaudel]

Can we make sure to keep history in this PR? To do that we'll have to change our "squash-only" policy and do each move as a merge commit, but the alternative (merging this as-is) will break git -L, which I use multiple times a day on Dafny's codebase.

[keyboardDrummer]

Can we make sure to keep history in this PR? To do that we'll have to change our "squash-only" policy and do each move as a merge commit, but the alternative (merging this as-is) will break git -L, which I use multiple times a day on Dafny's codebase.

From what I see on stack overflow, retaining the history on a change that splits off part of the code in a file requires a particular sequence of steps. Could you document these in the contributing documentation? I see we don't have a CONTRIBUTING.md but maybe this is a good reason to create one.

but the alternative (merging this as-is) will break git -L, which I use multiple times a day on Dafny's codebase.

Would it be possible to write a script that does git -L in a codebase where the code moves are not tracked? Something like:

1. Find the commit where the line of code was introduced.
2. Check out the previous commit, grep the codebase for the same line
3. If you find a hit, go back to 1

I'm asking because I foresee a lot of code moves in Dafny's future, some large but also many small, and I do not think there's an effective way of tracking these through git so git log -L will work for them. The technique in the stackoverflow post I linked above works for code that is moved to a fresh file, but not for code that is moved between existing files.

[cpitclaudel]

Could you document these in the contributing documentation? I see we don't have a CONTRIBUTING.md but maybe this is a good reason to create one.

Sure, I can do that.

Would it be possible to write a script that does git -L in a codebase where the code moves are not tracked?

Perhaps, though it sounds tricky, due to e.g. code duplication

[keyboardDrummer]

Would it be possible to write a script that does git -L in a codebase where the code moves are not tracked?

Perhaps, though it sounds tricky, due to e.g. code duplication

Have you tried using git log -S <string> ?

-S
Look for differences that change the number of occurrences of the specified string (i.e. addition/deletion) in a file. Intended for the scripter's use.
It is useful when you're looking for an exact block of code (like a struct), and want to know the history of that block since it first came into being: use the feature iteratively to feed the interesting block in the preimage back into -S, and keep going until you get the very first version of the block.

I tried it on several pieces of the code moved in this PR and it detects the last commit these code pieces were changed before this move, at which point you could do git log -L again

[cpitclaudel]

Yes, -S helps a lot when -L fails.

[keyboardDrummer]

Superseded by #2705