the main reason for splitting the library modules into XTheorems and XTheorems_proofs isn't performance but to make XTheorems more readable: the idea is that users want to browse the theorems that are available without being distracted by the proofs. We might be able to generate HTML that hides the proofs or even implement some clever search interface in the Toolbox but for the moment we simply provide the module with all proofs stripped away.
We are aware of the performance degradation of TLAPS as modules (including their dependencies) get longer and are working on alleviating it.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8BE7EA10-83C8-44DD-BC35-9BD735FEE7C7%40gmail.com.