Federico Poli

Two quick notes: * I don't think we can easily have a per-crate cache, because we don't use a per-crate server. I'd store the cache under the [global storage path...

> ```js > export function getCachePath(context: vscode.ExtensionContext): string { > return path.join(context.globalStoragePath, "cache.json") > } > ``` I'd use different cache files for different build channels (e.g. `cache-{buildChannel()}.json`?): https://github.com/viperproject/prusti-assistant/blob/8c12156a2298fb99227c6a319998025577d79114/src/config.ts#L12-L16 You...

> For the latter, I hadn't realised that but yes will definitely need to do that. I'm still having trouble getting the Prusti server to even save the cache on...

> Any idea why the CI fails? Mmm, not really. Does it pass locally?

I think it's quicker to do `if (buildChannel() != BuildChannel.LatestRelease) { /* set PRUSTI_CACHE_PATH */ }`. I'd wait a few weeks before doing a release, just to test the changes...

The thread-safety conditions are discussed in [this issue](https://github.com/Z3Prover/z3/issues/4762) and in [this commit](https://github.com/Z3Prover/z3/commit/9026ff28bca557d276c00dad9d225de1c6287b5c). I hope they are still up-to-date.

> We'd need to clone the solver before executing the then or else branch. If the decision to parallelize happens after the branching point, it might be that cloning the...

> If I understand you correctly, you're saying we could clone the solver later, while the then-branch is potentially already being verified (and then pop some asserts to remove whatever...

`download-artifact` uses the `@actions/artifact` package, which in turn uses the `unzip-stream` package. The loss of permissions seems to be due to `unzip-stream`, which does not preserve them at the moment:...

What is the correct way to compile this PR? I tried with the Dockerfile that I just added to the master branch but I get the following error: Click to...