TLAPS getting slower

[JosEdu Solsona]

Hello!

I have a spec A that refines another spec B. I found that TLAPS is noticeable slower when working on spec A. I guess this is kind of obvious, because A needs to instantiate B, so it is a more "complex" spec.

In any case, i would like to get some advice on the matter. For example, some pattern i see on the TLAPS library is to have modules like X.tla, XTheorems.tla and XTheorems_proofs.tla. As i also have a custom library of operators and another module with theorems about this operators, i wonder if separating the proofs from the statement would have some benefit on performance.

Cheers,

José

[Stephan Merz]

Hello José,

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.

Regards,

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/37f2fde7-1042-4e11-a249-3f853eaf2280n%40googlegroups.com.