[tlaplus] Re: "Cannot find source file for module TLAPS imported in module"

["thomas...@xxxxxxxxx" <thomasgebert@xxxxxxxxx>]

I'm a goofball. I didn't add the folder for /usr/local/lib/tlaps in the Toolbox.

On Saturday, March 26, 2022 at 11:45:38 PM UTC-4 thomas...@xxxxxxxxx wrote:

When I try and go through the TLAPS example here (https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Hierarchical_proofs.html), I get an error claiming it cannot find the TLAPS module.  

Is there another .TLA file I need to import?

-- 
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/6e5024a1-120a-43ae-99b8-cd9b1e97a060n%40googlegroups.com.