"Cannot find source file for module TLAPS imported in module"

254 views

Skip to first unread message

unread,

Mar 26, 2022, 11:45:38 PM3/26/22

to tlaplus

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?

unread,

Mar 27, 2022, 12:18:20 AM3/27/22

to tlaplus

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

Reply all

Reply to author

Forward

0 new messages