search

will62794 / tla-web

Interactive, web-based environment for exploring TLA+ specifications.
MIT License
69 stars 7 forks source link

Support module semantics #14

Open will62794 opened 2 years ago

will62794 commented 2 years ago

For the use cases I envision, I was not planning to implement full blown semantics of modules and module imports e.g. EXTENDS, etc. For example, for now I'm just considering operators from the standard modules to be globally available at all times, even without being explicitly imported. This behavior could be re-considered in the future, though, if necessary.

will62794 commented 1 year ago

See module notes: http://lamport.azurewebsites.net/tla/newmodule.html.

will62794 commented 1 year ago

Preliminary implementation in 6c12345, starting with limited support of EXTENDS based imports.

Handling INSTANCE based imports is a remaining task. Will also need to handle LOCAL INSTANCE semantics.

lemmy commented 5 months ago

Can the CommunityModules be added to the default search path? The root modules of both the CCF Consistency spec and the Azure CosmosDB spec extend them.

lemmy commented 5 months ago

Confirmed that the below doesn't work for CCF's consistency spec because resolving the CommunityModule's Functions and Folds from the CCF repo obviously results in a 404.

https://github.com/will62794/tla-web/blob/aeaf642766073bd3d82586bd98066dd0466aa16b/js/eval.js#L24-L30

https://github.com/will62794/tla-web/blob/aeaf642766073bd3d82586bd98066dd0466aa16b/js/eval.js#L1290-L1297

will62794 commented 5 months ago

See 538d398.

will62794 commented 2 months ago

Further progress towards module instantiation in 64a44dc.

Does not yet include full handling of parameterized instantiation.

will62794 commented 2 months ago

And initial handling of parameterized module instantiation in 799f00d.

Proper support of LOCAL definitions also still needed.