Split dafny ast

[keyboardDrummer]

Split DafnyAST.cs into logical chunks smaller than 5K lines

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

[cpitclaudel]

LGTM; it needs a rebase to be merged; you can use --rebase-merges for that

[cpitclaudel]

Should this be called git-cp.sh?

[keyboardDrummer]

LGTM; it needs a rebase to be merged; you can use --rebase-merges for that

I don't follow. Why can't we merge this with a merge commit?

[robin-aws]

Nit, but I would name this file git-copy.sh since that's what it actually does, and add comments describing the workflow of running this and THEN removing duplicate code, so the overall change is a split.

[cpitclaudel]

git-cp.sh, in fact, since that's what the Usage line below refers to?

[cpitclaudel]

Would you like to add the following sentence to CONTRIBUTING.md, or should I make a separate PR?

For pull requests that move large amounts of code to a new file, please use the script found in Scripts/git-cp.sh. Running git-cp.sh src dst will copy file src to dst using a branch and a merge, and you can then remove the duplicated parts from src and dst to complete the code move (this process allows git to track the file copy, as described in this StackOverflow answer).

[robin-aws]

So happy to see this monolith chopped up, thank you! Just nit picking a bit on documenting the workflow.

Can you also add something to the pull request template linking to the new section here? Something like "Are you moving code to new files? Please follow the steps here..."

[robin-aws]

I'm inclined to say something like "that move many lines of code", so we can err on the side of using this approach rather than not, and use our judgement on when it's not worth it. I'd still be sad to lose the history on 900 lines of code. :)

[keyboardDrummer]

Why be vague? When we're not specific then the erring can happen on either side.

[robin-aws]

Actually, perhaps we can just say "pull requests that move code from an existing to a new file...". I don't expect there to be a lot of PRs that purely move only a few lines of code to new files (rather than moving methods between existing files).

[keyboardDrummer]

I don't expect there to be a lot of PRs that purely move only a few lines of code to new files

I do, because a normal workflow of mine is to add things to a single file until it reaches a certain size (say >200 LOC), and then I'll use an IDE refactoring to move some of the classes to separate files. I imagine most of my PRs do this, so using this history preserving technique every time it would otherwise just be an IDE refactoring would be quite a drag.

I like files not being too big because when viewing code, each file gets its own cursor so you can switch between specific contexts within different files with a single hotkey, as opposed to having to remember the line numbers of the different contexts that are in a single file or opening that file multiple times, which often requires working with multiple panes.

One thing that might be practical is to try to look ahead and already split some files up into the pieces that we expect to want to refactor them to in the future. For example, I expect a lot of code in Resolver.cs to move to the individual AST Node classes, so code is more grouped by language feature which means that most PRs have to touch fewer places in the code base, since PRs often touch particular features. Given that the AST Node classes get bigger, I also expect each of them to end up in a separate file, so we could do a single PR that already puts each of them in its own file.

[cpitclaudel]

I imagine most of my PRs do this, so using this history preserving technique every time it would otherwise just be an IDE refactoring would be quite a drag.

This is similar to my workflow, except for the IDE part. Basically what I do is make the changes to the file until I decide "well, it's too large now". Then I commit my changes, and copy the file using the git-cp script. And finally I remove the duplicated bits of code.

Apart from the fact that I have to remove the duplicated bits by hand, the process isn't too much of a drag. But it may also be because I have high tolerance (and preference? ^^) for large files.

[keyboardDrummer]

Apart from the fact that I have to remove the duplicated bits by hand, the process isn't too much of a drag. But it may also be because I have high tolerance (and preference? ^^) for large files.

I wonder whether maybe your workflow supports large files better. Do you open a single file in multiple buffers to have multiple cursor positions? I don't think this would work so well for me since then each buffer doesn't have a clear indication of what component its cursor is focussed on.

[cpitclaudel]

I usually keep a single buffer open for each file, but I use the history feature in rider and the stack of markers in Emacs a lot.

[robin-aws]

I can live with addressing my documentation nit after merging to get this in :)