[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] "Cannot find source file for module TLAPS imported in module"
- From: "thomas...@xxxxxxxxx" <thomasgebert@xxxxxxxxx>
- Date: Sat, 26 Mar 2022 20:45:38 -0700 (PDT)
- Ironport-data: A9a23:cofs+qBmD2w78xVW/4Pmw5YqxClBgxIJ4kV8jS/XYbTApD8j1TFUy WBKWm/UOqrcZmTxKtt3aNmy8hsA65CHmoJmOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yE6jMlkf5KkYAL+EnkZqTRMFWFw0XqPp8Zj2tQy2YPjXVvW0 T/Pi5S31GGNi2Yc3l08sPrrRCNH5JwebxtF1rCWTakjUG72zxH5PrpHTU2CByeQrr1vIwKPb 72rIIdVUY/u10xF5tuNyt4Xe6CRK1LYFVDmZnF+A8BOjvXez8A/+v5TCRYSVatYo2rSpoFB0 /x/j6efESgkE4ztv748SCANRkmSPYUekFPGCX22sMjWyEqfNnWxnbNhC0Y5OYBe8eFyaY1M3 aZAeXZdM1ba2bvwnezTpupE3qzPKOH3OIoHvmx7jjvfBtwKfrPxY4jt2eJ+9h0B25sRQ9fnQ uUgRGFdXjn9PTRnNVAQB5Yzk/2vm2HkNTZfrTp5oIJtszSNnV0ri9ABNvLOIOylWcdrz3qEi XLP82DwMg8GDNWAnG/tHnWE37eTx0sXQrk6GLyj/eNxm3WPwmVVDQYMEFq9u/iwzE+4QdNWb UIOkhfCtoA3/U2vC976Bli2/SDCsRkbVN5dVeY97Wlh15Y4/S7GXVFVfiVoWuYdm5cZSBEL9 3jTvsjQUGkHXKKudVqR8bKdrDWXMCcTLHMfaSJscefjy4m8yG3UpkKfJuuPAJJZnfWuQ2ypm GniQDwWwuRO3JZUjc1X6Hie22r0zqUlWDLZ8ek+soiNxQp/eImjD2BDwQeGtK4bRGp1o6Xog ZTps82X7eRLCpbU0SLQHqMCG7am4/vDOzrZ6bKOI3XD32vxk5JAVdoKiN2bGKuPGppVEdMOS BKL0T69HLcJYBOXgVZfOupd8fgCw6n6DsjCXfvJdNdIaZUZXFbZoHE1PB/MhziyzhVEfUQD1 XGzIZnE4ZEyWfQP8dZKb7p1PUIDmnhulDqLG/gXMTz+ieXBOhZ5tovpwHPXNrxjhE91iArS9 NlbOqO3J+Z3AYXDjt3s2d9DRXhTdSZTLcmv+6R/K7DfSiI7RjBJI6KBkNsJJt0594wIx7eg1 i/nBidwlgGl7VWZclXiV5yWQO+HsWBX8CllbUTB/D+AgBAeXGpYxPpGL8JsJ+h+roSOD5dcF pE4RilJOdwXIhyvxtjXRcCVQFVKeEv5iASQETCiZTRjLZdsSxaQpI3reQzg8CQBFC2qrdB4q Lqlj1uJTZ0GTgVkLcDXdPP+nwjq5CNCxr1/DxnSP91eWETw64w2eSb/ufk6fpMXIhLZyzrGi gubWE9KpeTEr4Iv3sPOgKSI89WgH+dkTxhVGmDa6fC9MiyDpjivxopJUeCpezHBVTOsqP/yO 7kNl/ylaa8JhldHtYZ4Ao1H96Nm6ou9vaJewyRlAG7PMAamB7ZmFX+MgptCu6hL8blG4FfkV 0+K/O5aDrWHIsbSFlAceVg+ZeOZ2PBIwzTf4K1uckX37SN65oCKSUFDIx6IhHAPJbd5Ktp7k +gmv8ES5gOljQcyKZCNiSUNrzaAKXkJUqMGsJAGAd670VFykQ4cPpGMWDXr5JyvaslXNhV4K DGjgqef1a9XwVDPciZuGHXAgbhdiJAJtEwYxVMOPQ7SyN/Mh/ty2xoItDpqEEJayRJI1+81M W9ubhUnKaKL9jZupc5CQ2H8RF0bVUPBohT8mwkTiWnUb0i0TWiRfmczDuCAoRIC+GVGczkHo byVmTThUC32QcfqwyE2VRI3ovDvV4IhpAjLmcS7GJaKGJ41ZTfqmKizfXFNrhLhCMw8xxaY9 bg2obggNvSia20NpbYmAZKRz7UaRTiLI2tNRfxu5qQUBXqacza3gGDcJ0e0c8JLBvrL7U7pW 5c1f5kQCUuzhHSUszQWJa8QOLsozvQn09wPJ+HwLmkcvrrD8zdkvM6C/yTynjN6EdVyjd4me MSWeCiFD3SLw3RTnGDJoY9PPW//bsMDeRW7wOS86OEUDNUYret3elsz2La5sinHKgdh5B7I7 grPa7WMlL5nwIVo2ozrS+BNWlvyJtT0W+CFtgu0to0WP9/INM7PsSITq0Xmb1sKZ+pPA4wvm OTfqsPz0WPEoK0yDzLTla6HGvQb/s61RudWbp/6IXQycfFugyMwD8bvOlxUKKClVPtY78ijA gy/MY6+KIBTVNBay3lYLSNZFn7xzkgxgrjI/UuAQzakU3DxEjAr6Puo8njmaWxUbCgVI4a4A Qjx0xprzs4Nt5xCXXfoGNk/a6KV4zbftW8OeNr2uj2VAXOvn0uZ/LDlkHLMLN0N5masSK7H3 H4OevQymNledk0FIBG1frGeZiEqMUs=
- Ironport-hdrordr: A9a23:1hpPOKNHpAwewsBcTl6jsMiBIKoaSvp037BL7TEKdfUxSKb0qy nApoV+6faZskd3ZJnP8erwTJVpbxvnhOtICMoqTMaftDCPghrbEGga1/qU/9SCIVyEygbpvp 0QDZSWdueAdGSS1vyKnzVQeuxIqLL3kpxA492us0uFYjsEV0gK1XYANu/0KDwReOGGbaBJd6 Z0JfAom9NjQxgqhnTRPAh3YwEOnbz2fGKMW296O/fv0mn+6A+A2frBChCdmj0eXzlMzbpn0W +AvRf++rzLiYDK9iPh
- Ironport-sdr: HJD8RfO3PhswcuRYcYdGDfDY0lgiY840vCH+l+gBI5IaVRYwBVA6hTAM2nH9Kc4XgjDq8D5YlP DUuuBT/0+iuZj67b+g3ZFMzDy6aEAwrXkx6RfFqIKiyQYcKhP7fIkDNun5Qp9fssFrwePfThkF 6Uw5BxqjQg6pq5t1pPiZOoEnRjO/mTMrEq1DArSVRusIhy+rasmCt2nzlRepPvioXM3q59uPUl rakRKeqjHWcYwXCSWzIIP2JzJNLeNb3hyAftr98bAhlPTncn7cRl4thtHMXdfHy+RVkxOnd0XM 4zvY/rwVjXF8tZOnLN8GhNzj
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/bfa52fdc-2588-4591-8eba-3602bf18f8dan%40googlegroups.com.