Currently, there are certain situations where PGo refuses to compile an MPCal specification because it doesn't know how to generate an implementation for it. This happens even if the user requested the MPCal spec to be converted to PlusCal only.
Examples:
Using operators for which there is currently no Go implementation (e.g., DOMAIN);
Importing built-in TLA+ modules for which we don't currently have Go counterparts (e.g., FiniteSets).
In both of these cases, we could still compile a valid PlusCal spec. Separating these validations would allow PGo to be more broadly used in the specification pipeline without code generation (or, at the very least, it would not force the two current pipelines (spec and code generation) to always provide the same set of features -- they could be developed more independently).
rmascarenhas
commented
5 years ago
Currently, there are certain situations where PGo refuses to compile an MPCal specification because it doesn't know how to generate an implementation for it. This happens even if the user requested the MPCal spec to be converted to PlusCal only.
Examples:
DOMAIN);FiniteSets).In both of these cases, we could still compile a valid PlusCal spec. Separating these validations would allow PGo to be more broadly used in the specification pipeline without code generation (or, at the very least, it would not force the two current pipelines (spec and code generation) to always provide the same set of features -- they could be developed more independently).