Hmm ... it should not be OS-dependent, but I'll give it a try. I certainly believe having seen this under Linux. Can you use PTL at all in your Linux installation, i.e. for proving a valid temporal formula?
indeed – this is a known bug but apparently it had never been entered in the bug tracker. I just did that as https://github.com/tlaplus/tlaplus/issues/40. For the moment, please make sure that you use PTL only for proving temporal logic formulas, preferably in a context where all assumptions are constant formulas.