Between MPS major versions, the MPS global caches are nicely separated (e.g. for MPS 2017.1, the cache directory is $HOME/.MPS2017.1 and for MPS 2017.2, the cache directory is $HOME/.MPS2017.2, where $HOME is your home directory, e.g. C:\Users\<yourusername> on Windows or /home/<yourusername> on Linux). Sometimes, there are reasons why you would want to change the cache for a specific MPS distribution on your filesystem. Some of these reasons are:

  • Run different distributions or RCPs of MPS that have the same major version at the same time on your machine
  • Separate two MPS global caches (e.g. a cache for production in some project you work on and another cache for a course you have to give tomorrow), so they don’t interfere with each other.
  • Be able to open two modules (language or solution) with the same name/ID, without the two getting intermixed in the global cache (or MPS thinking that one has already been loaded, making the other read-only).

By default, the MPS cache-directory for an MPS major version called <version> (located under your $HOME directory) is .MPS<version>, e.g.: .MPS2017.2.

You can change this default location by adding a line like this in your vmoptions (for Windows, it’s located under your <mps installdir>\bin\mps64.exe.vmoptions):

-Didea.paths.selector=MPS34-MYOWNTHING

This would lead to the MPS that you run from <mps installdir> to maintain a cache directory called .MPS-MYOWNTHING in your $HOME directory.

 

Advertisements