theorems from instantiated modules in `tlapm` version 2

[Ioannis Filippidis]

I encountered the following behavior with v2-tlapm @ fd345f78c7e356b53c67e24f17e99df449d7b3a3 [1].
It may be internally unsupported syntax, but the old `tlapm == 1.4.3 (build 34695)` is happy with the modules involved,
and `tla2sany` too, so it seems worth reporting.


Issue 1:

The statement [2]:

```
    try
      Ok (Sany.import_xml channel)
    with
    | e ->
      Error e
```

appears to be catching errors that do not originate from `sany.jar`.
(I am not familiar with OCaml, but see issue 2 below.)
Those are later reported as "TLA to XML conversion error... java return code is 0".

This behavior initially suggested that something is wrong with the syntax,
but running `sany.jar` directly showed no errors (as suggested by the return code).
Changing the invocation from within OCaml to dump the XML to
a file showed the same result (no errors from `sany.jar`).


Issue 2:

Removing the `try` statement to obtain:

```
Ok (Sany.import_xml channel)
```

produces the message:

```
Exception: (Failure
  "We expected exactly one matching child in <AssumeProveNode> but got 0")
Backtrace: Raised at file "format.ml", line 185, characters 41-52
Called from file "format.ml", line 412, characters 8-33
Called from file "format.ml", line 427, characters 6-24
```

However, the module that causes this is `B` from below.
(Module `A` is in the include paths, and is seen by `sany.jar`.)
The issue seems to relate to instantiation of module `A`,
because if I change the statements to either

`Inst == INSTANCE Nat`  and  `Inst!Nat`

or remove the `BY` statement, then the error disappears.

------------------------------- MODULE B ---------------------------------------
Inst == INSTANCE A

THEOREM
    ASSUME TRUE
    PROVE TRUE
BY Inst!SomeTheorem
================================================================================


----------------------------- MODULE A -----------------------------------------
THEOREM SomeTheorem ==
    ASSUME TRUE
    PROVE TRUE
================================================================================

Please let me know in case I should open an issue at [1] for this or similar issues in the future.

[1] https://github.com/tlaplus/v2-tlapm
[2] https://github.com/tlaplus/v2-tlapm/blob/fd345f78c7e356b53c67e24f17e99df449d7b3a3/src/tlapm.ml#L59

Best regards,
ioannis

[Stephan Merz]

Dear Ioannis,

thanks for reporting this, and if you encounter such behavior, please do open an issue on GitHub so that we can keep track easily.

The code that you are experimenting with is in internal development, not even an alpha release yet, and the TLA to XML converter still has a number of issues that we are hunting down (be they bugs or misunderstandings on our side).

Regards,

Stephan

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Ioannis Filippidis]

Hi Stephan,

Thanks for noting the pre-alpha status of the code. I will report further issues on GitHub.

I will note in this thread another observation, about `tlapm == 1.4.3`, due to its relevance.
If module A contains a local instantiation `Inst` (without parameters), and module B extends A,
then mentioning `Inst!SomeDef` in a proof within B works for `tlapm`, though `tla2sany` cannot
find the definition, because it is local. Parameterized instantiation is mentioned in the
unsupported features, so seems to be a related issue.

Making the instance visible avoids the errors from `tla2sany`.
Duplicating the instantiation within the proof in B works for `tla2sany`, but not for `tlapm`.
My hypothesis is that the definition in module B shadows the local one in module A.

In the development version of `tlapm`, `tla2sany` still raises errors when the instantiation
is local, but it generates XML output, so `tlapm` proceeds (with a later error due to absence
of `nunchaku` in my current installation).

Best regards,
ioannis