Fix version of Newtonsoft.Json

[MikaelMayer]

This will fix #1722 by expliciting the version of Newtonsoft.json in both DafnyDriver and DafnyLanguageServer.

I added a test in DafnyLanguageServer to ensure the two versions are in sync, to prevent further synchronization problems.

[keyboardDrummer]

How does this relative path work? I thought you can't assume anything about the working directory when running tests. Can you?

[MikaelMayer]

It looks like it work ! It assumes we are in DafnyLanguageServer.Test\bin\Debug\net6.0

[robin-aws]

It's definitely better not to assume anything about the output directory, in which tests run (and I worked really hard not to in the xUnit lit test runner), but in a test that will fail loudly if the assumption is ever violated, I think it's fine.

[keyboardDrummer]

Thus, when we compile DafnyDriver, the DafnyLanguageServer does not work anymore if it's in the same folder.

Is this something we could test, instead of testing the dll versions directly?

[MikaelMayer]

Is this something we could test, instead of testing the dll versions directly?

Testing will not prevent the version from being incompatible for either project, unless you have a way to force DafnyLanguageServer to dynamically load its version of NewtonSoft.json.dll without the need to "install" it next to it?

[keyboardDrummer]

Can I ask, how do you reproduce the bug that this PR wants to solve? Can we create a test that executes that reproduction?

[MikaelMayer]

Can I ask, how do you reproduce the bug that this PR wants to solve? Can we create a test that executes that reproduction?

I understand your question now ! To reproduce the bug, here is how you would proceed on the command-line:

dotnet build Source/DafnyLanguageServer
dotnet build Source/DafnyDriver
dotnet Binaries/DafnyLanguageServer.dll

You'd get the following error:

Unhandled exception. System.IO.FileLoadException: Could not load file or assembl
y 'Newtonsoft.Json, Version=11.0.0.0, Culture=neutral, PublicKeyToken=30ad4fe6b2
a6aeed'. The located assembly's manifest definition does not match the assembly
reference. (0x80131040)
File name: 'Newtonsoft.Json, Version=11.0.0.0, Culture=neutral, PublicKeyToken=3
0ad4fe6b2a6aeed'
at Microsoft.Dafny.LanguageServer.Program.Main(String[] args)
at Microsoft.Dafny.LanguageServer.Program.

(String[] args)

I'm not sure how I am going to implement this test but I'll have a look.

[cpitclaudel]

I'm not sure how I am going to implement this test but I'll have a look.

I'm worried about the complexity of implementing such a test vs. the benefit. In this case the problem seems to be (IIUC) that we have two projects that depend(ed) on two different versions of a DLL.

Now, because we put all of our binaries in the same place instead of partitioning them into separation bin/ directories, the DLL that ended up in there ended up being whichever was selected by the project that got compiled most recently.

The fix to this is to use the same version in both places, and to make that fix robust we can have a check that asserts that the versions match. I don't think it's enough to try to catch load-time bugs: having a different DLL loaded depending on compilation order is a recipe for trouble even if things don't crash right away (ie, the test wouldn't be reliable).

[keyboardDrummer]

Do we need to build DafnyLanguageServer and DafnyDriver to the same directory? What happens if we remove <OutputPath>..\..\Binaries\</OutputPath> ?

[cpitclaudel]

That should fix it, but is it a change we want to make now?

[keyboardDrummer]

That should fix it, but is it a change we want to make now?

If there's no impact from doing that, then yes right? Not building two projects into the same folder will solve the Newtonsoft.Json problem but also potential future problems with different libraries. On first glance the release script release.py doesn't seem to depend on the output going to the binaries directory, so I'm not sure what would depend on it.

[MikaelMayer]

If there's no impact from doing that, then yes right?

There is an impact for doing the change of where the output of the build is going to be placed.
First for every developing environment who rely on Dafny.exe or Dafny.dll being generated in this Binaries/ folder. For example, people using the Dafny IDE plugin with custom Dafny installation - note that there are 186 forks of this project.
It will force everyone to also update their path to where to look for Dafny.exe, Dafny.dll or DafnyLanguageServer.dll
Second, which one should we move? Dafny or DafnyLanguageServer?
This, it will force people copying the binaries to another folder to replicate the folder structure we will have come up with, which is cumbersome.

I think it's an aberration that two Dafny projects in the same solution actually use two different versions of the same library, and if we can handle it by synchronizing the versions, that's a non-breaking change that is way better than changing the directory structure.
I suggest we postpone moving binaries in different folders after careful design of that step, in a next major release, such as Dafny 4.0

[cpitclaudel]

On first glance the release script release.py doesn't seem to depend on the output going to the binaries directory, so I'm not sure what would depend on it.

Wouldn't the same problem happen in the output of release.py? It would copy two different DLLs to the same directory, and we'd be back to this issue.

[keyboardDrummer]

I'll approve this since it's definitely better than not having the change. Thanks for the fix @MikaelMayer

[keyboardDrummer]

If there's no impact from doing that, then yes right?

There is an impact for doing the change of where the output of the build is going to be placed. First for every developing environment who rely on Dafny.exe or Dafny.dll being generated in this Binaries/ folder. For example, people using the Dafny IDE plugin with custom Dafny installation - note that there are 186 forks of this project. It will force everyone to also update their path to where to look for Dafny.exe, Dafny.dll or DafnyLanguageServer.dll Second, which one should we move? Dafny or DafnyLanguageServer? This, it will force people copying the binaries to another folder to replicate the folder structure we will have come up with, which is cumbersome.

I think it's an aberration that two Dafny projects in the same solution actually use two different versions of the same library, and if we can handle it by synchronizing the versions, that's a non-breaking change that is way better than changing the directory structure. I suggest we postpone moving binaries in different folders after careful design of that step, in a next major release, such as Dafny 4.0

Indeed it's a much bigger change than this PR. We can make it later :-)

[keyboardDrummer]

I'm not sure how I am going to implement this test but I'll have a look.

I'm worried about the complexity of implementing such a test vs. the benefit. In this case the problem seems to be (IIUC) that we have two projects that depend(ed) on two different versions of a DLL.

Now, because we put all of our binaries in the same place instead of partitioning them into separation bin/ directories, the DLL that ended up in there ended up being whichever was selected by the project that got compiled most recently.

The fix to this is to use the same version in both places, and to make that fix robust we can have a check that asserts that the versions match. I don't think it's enough to try to catch load-time bugs: having a different DLL loaded depending on compilation order is a recipe for trouble even if things don't crash right away (ie, the test wouldn't be reliable).

Would your language server testing PR would be a good test against this bug, since it tests the language server in non-trivial ways?

[cpitclaudel]

Would your language server testing PR would be a good test against this bug, since it tests the language server in non-trivial ways?

I hope so? I ran into this issue as well while working on the LSP tester :)