Skip to content

Add persistent caching - #134

Open
JonasAlaif wants to merge 8 commits into
masterfrom
prusti-cache
Open

Add persistent caching#134
JonasAlaif wants to merge 8 commits into
masterfrom
prusti-cache

Conversation

@JonasAlaif

Copy link
Copy Markdown
Contributor

No description provided.

@fpoli

fpoli commented Jan 20, 2022

Copy link
Copy Markdown
Member

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 of the extension, in the (existing) folder of the configured toolchain build channel.
  • When deleting the cache file, I think we have to stop the server before and re-start the server after.

@JonasAlaif

JonasAlaif commented Jan 21, 2022

Copy link
Copy Markdown
Contributor Author

Thanks! Very good points, the former I realised as I was trying to implement the per-crate cache, I now use (makes it infinitely easier to delete the cache as well, since we don't have to go looking for the file):

export function getCachePath(context: vscode.ExtensionContext): string {
     return path.join(context.globalStoragePath, "cache.json")
 }

Should I additionally put the cache.json inside an extra directory?
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 exit - using SIGTERM instead of KILL doesn't seem to help.

@fpoli

fpoli commented Jan 21, 2022

Copy link
Copy Markdown
Member
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?):

export enum BuildChannel {
LatestRelease = "LatestRelease",
LatestDev = "LatestDev",
Local = "Local"
}

You can look it up with:
export function buildChannel(): BuildChannel {

Also, I'd move the getCachePath to the config.rs file (and call it cachePath). We could then let the user override its location (independently from the build channel) in the future.

@fpoli

fpoli commented Jan 21, 2022

Copy link
Copy Markdown
Member

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 exit - using SIGTERM instead of KILL doesn't seem to help.

To understand if it's a Prusti or Prusti-assistant issue, does the server save the cache if you manually start and terminate it from the command line? If that's too hard to fix, we can add a POST /save entry point to the API of the prusti-server, such that we can call that from the IDE before stopping the server.

@JonasAlaif

Copy link
Copy Markdown
Contributor Author

Any idea why the CI fails?

@fpoli

fpoli commented Jan 21, 2022

Copy link
Copy Markdown
Member

Any idea why the CI fails?

Mmm, not really. Does it pass locally?

@JonasAlaif

Copy link
Copy Markdown
Contributor Author

Not when I run the tests no - it gets stuck on Checking Prusti dependencies and warns that activating the extension failed because Prusti server took more than 10 seconds to start.
But when I have the project open in VSCode and run it with F5 it works just fine.

@JonasAlaif

JonasAlaif commented Jan 21, 2022

Copy link
Copy Markdown
Contributor Author

Ah, I've found the answer:

[stderr] thread '[stderr] main' panicked at 'environment variables contains unknown configuration flag: “cache_path”', prusti-common/src/config.rs:168:9

Is there any solution to this, other than waiting for caching to be included in a Prusti release?

@fpoli

fpoli commented Jan 21, 2022

Copy link
Copy Markdown
Member

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 for a while.

@fpoli fpoli changed the title Add caching support Add persistent caching Apr 15, 2022
@JonasAlaif
JonasAlaif marked this pull request as ready for review July 19, 2022 14:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants