Josselin Poiret

So I've pinpointed the problem: since the GADP server is launched outside of the main ghidra VM, the VM arguments passed to ghidra aren't inherited by the server, especially the...

Sorry to answer you this late: I have successfully been able to use java.library.path to load the dbgeng.dll located in `C:\Program Files (x86)\Windows Kits\10\Debuggers\x64` without moving them anywhere, and I...

One thing I'm still unsure is whether `withVarOcc` should be idempotent (a test that's being falsified by quickcheck) when modalities are included in the mix. All the previous modalities were...

>Is this code modality-correct? No, right? Is that enforced right now? So two things: - This doesn't type-check for now, because we explicitely disallow splitting on non-mixed arguments, which is...

> Is it necessary to check the full type again, or would it suffice to check the polarity annotations? Or could the polarity annotations be checked the first time? It's...

I just rebased on top of your recent erasure changes @nad. I also added some documentation, although it is pretty terse for now, and fixed some failing tests (among them,...

So I'm investigating the test failure of `all/LibSucceed/SizeInconsistentMeta4`, it has to do with the size solver. The part that is causing an issue now seems to be the additional size...

> Could someone summarize the current state of this PR and make a todo list of what still needs to be done to bring it into a mergable state? Sure,...

So I think I've completed the above todo list, but some questions remain: by adding the `--polarity` flag, I also resolved the failing test with sized types because now the...

Thanks @jespercockx for the review! I realised this morning with @anuyts that we actually have some problems with polarities and modules. The following type-checks: ```agda module _ where data ⊤...