prusti-dev Test's config not transferred to Prusti server

In compiletest, the server is only spawned once and with the default config (or with the config defined with the env PRUSTI_...=... variables). So if a test uses a config flag that is used in the server, the server will not use the value specified in the test file.

Feb 01 '23 18:02 Pialex99

Thanks for reporting this. As a workaround, does it work to add the flag -Pserver_address="" or -Pserver_address=MOCK to the tests that need to set configuration flags for the server?

Feb 01 '23 19:02 fpoli

Using -Pserver_address=MOCK worked! Using -Pserver_address="" results in a panic a parsed Url should always be a valid Uri: InvalidUri(InvalidUriChar) at reqwest-0.11.13/src/into_url.rs:70:14.

Feb 02 '23 08:02 Pialex99

Using -Pserver_address=MOCK worked!

I'm glad that the 3-years old feature that nobody used so far is actually useful :rofl: It spawns a new server in a thread.

Feb 02 '23 08:02 fpoli

But IIUC this is not good to do for the test suite in general, since it would not share the same server for all the tests and so reduce performance, right?

Feb 02 '23 10:02 Aurel300