agda
System.Directory.Primitive - XdgDirectory problem
This is related to v2.0 and other's trouble with running the tests.
So the released stdlib 2.0 has https://github.com/agda/agda-stdlib/blob/2b8fff10f4033b91a6df4007e4a65cb10047c89c/src/System/Directory/Primitive.agda#L29
whereas released stdlib 2.1 has https://github.com/agda/agda-stdlib/blob/039e1f4abda49f307f7ed1f5e15232a1c8e9c48c/src/System/Directory/Primitive.agda#L29
git blame says that this was fixed by @gallais in https://github.com/agda/agda-stdlib/commit/307152fd7a5e294225d68c63784a6af272eb0fc1
This seems to be a GHC synchronization issue (that I have not tracked down in full) where XdgState was added. This is new to directory-1.3.7.0 (which itself is quite old) but it is hard to tell when that became the default for Agda / MAlonzo.
Best guess: v2.0 was released without this particular test suite being run. Probably because the release instructions do not have a make testsuite step! @MatthewDaggitt
I guess we could back-patch v2.0 with this fix? I'm not entirely sure what the best path forward is, which is why I am keeping this commentary as a separate comment rather that as part of the issue itself.
Backpatching seems a reasonable suggestion, but would that change which release(s) of Agda are available to build it?
Any other imaginable knock-on consequences?
This seems to be a GHC synchronization issue (that I have not tracked down in full) where XdgState was added. This is new to directory-1.3.7.0 (which itself is quite old) but it is hard to tell when that became the default for Agda / MAlonzo.
Can we force 2.0 to use directory<1.3.7.0? I don't know that there's any easy way to do that because Agda does not really have a good story when it comes to building projects with dependencies on Haskell libs: https://github.com/agda/agda/issues/4627
At the momment IIRC we install the libs globally and hope for the best that they're the right sort of version. :s
I suppose we could hand-cook a .cabal file just for the test suite.
So unfortunately we can't backpatch to the v2.0 tag as that will break all sorts of CI scripts that depend on v2.0 of the library, e.g. Wen's github actions. If we back patched it to the v2.0 branch we'd then have to release v2.0.1 which would be a little bit odd this late in the day... I guess we can ask the reviewers of the paper whether they're happy for the test suite to work for current versions but not for the released 2.0?
We could backpatch to the v2.0-joss-submission branch?
Is v2.1 different enough from v2.0 that we can't make this paper about that? I know it is mainly about the jump from < v2.0 to v2.0.
[Also, we should make sure that this isn't the only bug in the test suite!]
Yes, we could backpatch to v2.0-joss-submission branch, good idea! If we can find a fix...
@gallais given that the XDGState constructor isn't actually used in that PR, could we simply create a patch for the v2.0-joss-submission branch that removes it again?
I expect that would mean that it would stop building for other reviewers?
The principled solution is to have a cabal file that specifies the proper constraints
on directory (and other dependencies) for the given version of the library.
I may have time to look at it tomorrow morning.
@gallais might you have time to look at this week? Unfortunately I don't have any experience with the FFI to Haskell, otherwise I would try and tackle this. If you don't have time, I can have a go though...
Alright, I got something working locally. I'll let the CI run and it'll hopefully work on the build servers too.
Looks like we should close this issue now - right @gallais and @MatthewDaggitt ? Or is there some back-porting to master that should be done first?
There's an open PR for the backport I still need to fix when I'll have time