Add SANY as a parser backend option

[ahelwer]

Hidden behind --parser SANY CLI argument

These changes add SANY as a possible parser backend, converting SANY's XML Exporter output to TLAPM's internal parse tree format. This is primarily done in src/sany/xml.ml and src/sany/sany/ml. Some modifications were also made to the command line parameters and library code to enable use of SANY.

Supersedes #255; this PR is the same, just with cleaned-up commit history. That PR can be consulted for a timestamped work log.

Ref #213 tlaplus/tlaplus#1313

[ahelwer]

@muenchnerkindl @damiendoligez pleased to say this PR is now basically feature-complete and merge-ready. There are some insurmountable shortfalls on the SANY side still but they are relatively minor.

[lemmy]

Does TLAPS use the JDK bundled with Isabelle to run SANY, or must users install Java separately? If a separate Java installation is required, would it make sense to distribute an ahead-of-time-compiled version of SANY instead (compare tlaplus/rfcs#16 (comment))?

[ahelwer]

We could possibly use the bundled JDK version although currently it just shells out to java on the user's path. Using a precompiled SANY XML Exporter would be interesting. Could also be added in future changes.

[Copilot]

Pull request overview

This PR adds an experimental SANY-based parser backend (selectable via --parser SANY) by shelling out to SANY’s XMLExporter, parsing the emitted XML, and translating it into TLAPM’s existing internal syntax tree format. It also adds CLI/config plumbing for the new backend, includes support for adding extra module jars to SANY’s classpath, and introduces equivalence tests comparing TLAPM vs SANY parse trees.

Changes:

• Add SANY XML parsing + AST conversion pipeline (src/sany/xml.ml, src/sany/sany.ml/.mli) and expose parse-tree S-expression export.
• Add CLI/config options for selecting parser backend and providing additional module jars (--parser, --module-jar), plus wiring in tlapm_lib.
• Add SANY/TLAPM parse-tree equivalence tests + CI job coverage, and fetch/install tla2tools.jar as a dune site backend.

Reviewed changes

Copilot reviewed 55 out of 55 changed files in this pull request and generated 6 comments.

Show a summary per file

File	Description
.github/workflows/ci.yml	Adds a CI job that runs a subset of examples through the SANY backend.
deps/tla2tools.jar/Makefile	Downloads tla2tools.jar for SANY XMLExporter usage.
deps/tla2tools.jar/dune	Adds a dune rule + site install for tla2tools.jar.
dune-project	Adds xmlm dependency needed by the XML parser.
src/dune	Links xmlm into the main library.
src/params.ml	Adds parser_backend and module_jar_paths params.
src/params.mli	Exposes new params and parser-backend type.
src/paths.ml	Adds classpath construction helper for locating backend jars.
src/paths.mli	Exposes backend_classpath_string.
src/sany/sany.ml	Implements conversion from SANY XML AST to TLAPM AST and S-expression export.
src/sany/sany.mli	Exposes SANY parse entrypoint and S-expression export.
src/sany/translate_syntax_tree.ml	Adjusts module opens for syntax-tree-to-sexp translation.
src/sany/xml.ml	Implements SANY invocation, XML parsing, and typed XML AST.
src/tlapm_args.ml	Adds --parser and --module-jar CLI flags.
src/tlapm_lib.ml	Wires SANY backend into main and modctx_of_string.
test/cli/cli_tests.ml	Adds CLI parsing test coverage for --module-jar.
test/parser/parser_tests.ml	Switches parse-tree sexp comparison to the shared module_to_sexp.
test/sany/equivalence/dune	Adds a new OUnit test executable for SANY/TLAPM equivalence.
test/sany/equivalence/sany_equivalence_tests.ml	Implements test harness to compare TLAPM vs SANY parse trees (via sexp diff).
test/sany/equivalence/00_ConstantRefTest.tla	Adds minimal equivalence corpus module (constants).
test/sany/equivalence/01_VariableRefTest.tla	Adds minimal equivalence corpus module (variables).
test/sany/equivalence/02_OperatorRefTest.tla	Adds minimal equivalence corpus module (operator refs).
test/sany/equivalence/03_AssumeRefTest.tla	Adds minimal equivalence corpus module (ASSUME refs).
test/sany/equivalence/04_TheoremRefTest.tla	Adds minimal equivalence corpus module (theorem refs).
test/sany/equivalence/05_ConstantOperatorTest.tla	Adds minimal equivalence corpus module (constant operator application).
test/sany/equivalence/06_OperatorParameterRefTest.tla	Adds minimal equivalence corpus module (operator parameters).
test/sany/equivalence/07_ExpressionTest.tla	Adds minimal equivalence corpus module (basic expression).
test/sany/equivalence/08_ObviousProofTest.tla	Adds minimal equivalence corpus module (OBVIOUS proof).
test/sany/equivalence/09_BasicByProofTest.tla	Adds minimal equivalence corpus module (BY proof).
test/sany/equivalence/10_BasicStepProofTest.tla	Adds minimal equivalence corpus module (step proofs).
test/sany/equivalence/11_BasicAssumeProveTest.tla	Adds minimal equivalence corpus module (ASSUME/PROVE).
test/sany/equivalence/12_BasicCaseStepProofTest.tla	Adds minimal equivalence corpus module (CASE steps).
test/sany/equivalence/13_BasicProofStepReferenceTest.tla	Adds minimal equivalence corpus module (step references).
test/sany/equivalence/14_BasicPTLProofTest.tla	Adds minimal equivalence corpus module (PTL proof).
test/sany/equivalence/15_SufficesProofTest.tla	Adds minimal equivalence corpus module (SUFFICES).
test/sany/equivalence/16_NewBoundedAssumeTest.tla	Adds minimal equivalence corpus module (NEW + bounded).
test/sany/equivalence/17_ActionOperatorTest.tla	Adds minimal equivalence corpus module (action operators).
test/sany/equivalence/18_PrimeOperatorTest.tla	Adds minimal equivalence corpus module (prime operator).
test/sany/equivalence/19_HierarchicalProofTest.tla	Adds minimal equivalence corpus module (hierarchical proofs).
test/sany/equivalence/20_MixedByProofTest.tla	Adds minimal equivalence corpus module (mixed BY usage).
test/sany/equivalence/21_ExtendsBase.tla	Adds minimal equivalence corpus module (EXTENDS base).
test/sany/equivalence/21_ExtendsTest.tla	Adds minimal equivalence corpus module (EXTENDS usage).
test/sany/equivalence/22_UseDefStepTest.tla	Adds minimal equivalence corpus module (USE DEF step).
test/sany/equivalence/23_SufficesAssumeProveTest.tla	Adds minimal equivalence corpus module (SUFFICES ASSUME/PROVE).
test/sany/equivalence/24_StepAssumeBoundedNewTest.tla	Adds minimal equivalence corpus module (ASSUME NEW bounded step).
test/sany/equivalence/25_ExtendsConstantBase.tla	Adds minimal equivalence corpus module (EXTENDS + constants base).
test/sany/equivalence/25_ExtendsConstantStepTest.tla	Adds minimal equivalence corpus module (EXTENDS + constant proof).
test/sany/equivalence/26_InstanceWithBase.tla	Adds minimal equivalence corpus module (INSTANCE base).
test/sany/equivalence/26_InstanceWithTest.tla	Adds minimal equivalence corpus module (INSTANCE WITH usage).
test/sany/equivalence/27_LabelDefinitionTest.tla	Adds minimal equivalence corpus module (labels in definitions).
test/sany/equivalence/28_LabelParameterTest.tla	Adds minimal equivalence corpus module (labels with params).
test/sany/equivalence/29_LabelInQuantifierTest.tla	Adds minimal equivalence corpus module (labels in quantifiers).
test/sany/equivalence/30_HideDefStepTest.tla	Adds minimal equivalence corpus module (HIDE DEF step).
test/sany/known_failures/LabeledSubexpression.tla	Documents a known conversion gap related to labeled subexpressions.
tlapm.opam	Adds xmlm opam dependency.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[glondu]

Hi,

I had a look at this pull request.

To evaluate how much this could be a drop-in replacement to tlapm's built-in parser, I've patched tlapm (the branch from #275) to default to SANY with an environment variable, and ran the test suite with the variable set.

I also had to implement tlapm_lib.ml's module_of_string to use SANY. (I did it by using a temporary file.)

The branch is there: https://github.com/glondu/tlapm/tree/sany

In the following, I'll focus on the following workflow:

dune exec -- ./parser_tests.exe run from test/parser

This includes 281 test cases.

The following of this message has been written with the help of Claude.

Summary

Ran: 281 tests
Failures: 159–173

Of these failures, once error messages were properly surfaced (see "Harness fixes" below), they break down as:

Category	Count	Action needed
Pre-existing TLAPM parser bugs	31	None — independent of SANY, already tracked (issues #54, #161–173)
SANY eagerly rejects semantically-invalid-but-syntactically-valid fragments	122	Architectural discussion — see below
Genuine syntax/grammar divergences	14	Individual investigation, listed below
Known conversion gaps (Unsupported_language_feature, Conversion_failure)	~8–10	Individual bug fixes, listed below
Real AST structural differences (parens dropped, nested modules, string escapes, decl grouping)	12	Mostly expected/benign, see below
Bugs fixed for free by SANY vs. old TLAPM parser	5	Positive — document as improvements

Harness fixes made during this investigation

One place in the code was silently discarding error information, which made root-causing individual failures impossible until fixed:

1. test/parser/parser_tests.ml — parse caught all exceptions with with _ -> None, discarding the message entirely.

I quickly patched it using a reference, but a more permanent solution has to be designed — it would be useful for regular test failures too, not just this migration.

Main finding: SANY does eager semantic resolution during "parsing"

88% of the failures with real error messages (122/138) come from a single structural mismatch, not from 122 independent bugs.

TLAPM's own parser and the tree-sitter grammar (which the standardized corpus was written against) are purely syntactic — they build a parse tree without resolving identifiers or checking level constraints. SANY, when invoked via tla2sany.xml.XMLExporter, performs full semantic analysis (name resolution, level-checking) as part of what it calls "parsing." The standardized syntax corpus intentionally contains many fragments that are syntactically valid but semantically incomplete or invalid — since it exists to test grammar acceptance, not full program validity. Examples pulled directly from the corpus:

• Undeclared identifiers used as placeholders (Unknown operator: 'x') — by far the most common
• Deliberate re-declaration tests (Multiply-defined symbol, Operator X already defined or declared)
• Deliberate built-in shadowing tests (Symbol \lnot is a built-in operator, and cannot be redefined)
• INSTANCE of a module that doesn't exist (Cannot find source file for module M)
• Custom infix/prefix/postfix operators used without their declaration in scope (Couldn't resolve infix operator symbol '+')
• RECURSIVE f without a body (Symbol f declared in RECURSIVE statement but not defined)

None of these are TLAPM- or SANY-specific bugs; they're a consequence of running a semantic-analysis-eager parser against a syntax-only test corpus.

This needs a decision, not a fix, on one of:

• (a) Modify the local copy of the corpus fixtures to be semantically self-contained (adds maintenance burden, diverges from upstream corpus)
• (b) Check whether tla2sany.xml.XMLExporter (or SANY more broadly) exposes a syntax-only mode that skips semantic analysis
• (c) Accept this as a known, documented limitation of the SANY backend for this particular test suite, and exempt the whole category rather than tracking 122 individual cases

Genuine syntax/grammar divergences (14 cases) — worth individual triage

These are not semantic-resolution noise; they represent real differences in what each parser accepts:

1. Precedence conflict between & and -. — resolved differently by TLAPM vs. SANY
2. Jlist item "not properly indented inside conjunction or disjunction list item" — possible stricter indentation rule in SANY
3. ]_ not handled in some bracket context (Encountered "]_" ... token "}")
4. Lexical error on * following an escaped backslash in a string
5. \X rejected as an infix operator (verify against corpus intent — may be a misclassified Error_test)
6. Unexpected THEOREM placement rejected
7. Unexpected , token in some context
8. << with a missing operand (Nonexistent operand specified by)
9. Internal SANY crash: Internal error: should have name here (Generator.java:755) — worth reporting upstream to tlaplus/tlaplus
10. XML export failure on a raw control character (0xc) inside a string literal — SANY's XML export can't serialize certain control characters that TLA+ string syntax permits

Bonus, unrelated to this migration: found two instances of a genuine upstream SANY bug — java.util.UnknownFormatConversionException: Conversion = ''' in Errors.java:70 — SANY's own error-message formatter crashes when the error text needs to mention the ' operator symbol. Worth filing separately against tlaplus/tlaplus.

Known conversion gaps already caught by custom exceptions

• Conversion_failure(InvalidBoundsOrOperands, ..., "Invalid number of bounds or operands to CHOOSE") — tuple-bound CHOOSE (e.g. CHOOSE <<x, y>> \in S : P) is not handled by the SANY→TLAPM AST conversion for CHOOSE. Concrete, fixable bug in src/sany/sany.ml.
• Unsupported_language_feature — raised deliberately for features not yet wired up (e.g. tuple-bound Set Filter, some RECURSIVE reference cases). Run grep -n "Unsupported_language_feature\|raise.*Unsupported" src/sany/*.ml for the full enumerated list of known gaps.

Real AST structural differences (12 cases) — mostly expected, not bugs

• Grouping parentheses dropped from the AST ((parentheses (nat_number)) vs (nat_number)) — expected: SANY normalizes to a semantic AST and doesn't preserve pure syntactic grouping, unlike the tree-sitter concrete syntax tree. Likely resolvable by adjusting the equivalence test's expectations rather than the converter.
• Nested/sub-modules dropped entirely from the converted tree — this one is a real gap in src/sany/xml.ml/sany.ml; nested MODULE blocks aren't being descended into.
• String escape sequences (escape_char nodes) collapsed into a flat, already-unescaped (string) node — SANY's XML output likely doesn't expose character-level escape structure.
• Multi-identifier CONSTANT/VARIABLE declarations grouped differently in the resulting tree than tree-sitter expects.

Improvements SANY brings "for free" (5 cases) — worth calling out positively

These are pre-existing, tracked TLAPM parser bugs where SANY's behavior is more correct than TLAPM's own parser, not a regression:

• Invalid LOCAL Declaration of USE/ASSUME/THEOREM — TLAPM incorrectly accepts these; SANY correctly rejects them
• Invalid parentheses use in jlist (issue TLAPM parser accepts invalid use of parentheses to escape conjunction list #168) — same pattern
• Label interfering with precedence (issue TLAPM parser accepts incorrect use of labels that break operator precedence #169) — same pattern

[lemmy]

• (b) Check whether tla2sany.xml.XMLExporter (or SANY more broadly) exposes a syntax-only mode that skips semantic analysis

SANY doesn’t provide us with syntax-only today. Instead, it assumes that the resolved UID references have been provided and therefore requires semantic analysis to be done.

[lemmy]

9. Internal SANY crash: Internal error: should have name here (Generator.java:755) — worth reporting upstream to tlaplus/tlaplus
10. XML export failure on a raw control character (0xc) inside a string literal — SANY's XML export can't serialize certain control characters that TLA+ string syntax permits

Bonus, unrelated to this migration: found two instances of a genuine upstream SANY bug — java.util.UnknownFormatConversionException: Conversion = ''' in Errors.java:70 — SANY's own error-message formatter crashes when the error text needs to mention the ' operator symbol. Worth filing separately against tlaplus/tlaplus.

Could you please provide reproducers?

[glondu]

Could you please provide reproducers?

All the errors can be reproduced using my branch and the following command from the test/parser directory:

TLAPM_PARSER_BACKEND=sany dune exec -- ./parser_tests.exe 2>&1 | tee /tmp/tlapm-sany.log

For example, the "internal SANY crash" can be reproduced with the following input:

---- MODULE Test ----
tree_nav == op(a, b)!<<!>>!3!(x, y)!:!@
====

SANY output:

Fatal errors in semantic processing of TLA spec /tmp/tlapm/TestC.tla
null
Stack trace for exception:

line 2, col 25 to line 2, col 26 of module TestC

Internal error: should have name here.
	at tla2sany.semantic.Errors.addMessage(Errors.java:158)
	at tla2sany.semantic.Errors.addError(Errors.java:174)
	at tla2sany.semantic.Generator.selectorToNode(Generator.java:755)
	at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:3118)
	at tla2sany.semantic.Generator.generateExpression(Generator.java:2982)
	at tla2sany.semantic.Generator.processOperator(Generator.java:2595)
	at tla2sany.semantic.Generator.generateModule(Generator.java:2167)
	at tla2sany.semantic.Generator.generate(Generator.java:2108)
	at tla2sany.drivers.SANY.frontEndSemanticAnalysis(SANY.java:452)
	at tla2sany.drivers.SANY.parse(SANY.java:196)
	at tla2sany.xml.XMLExporter.parseSpec(XMLExporter.java:244)
	at tla2sany.xml.XMLExporter.moduleToXML(XMLExporter.java:213)
	at tla2sany.xml.XMLExporter.run(XMLExporter.java:128)
	at tla2sany.xml.XMLExporter.main(XMLExporter.java:114)
Semantic errors detected before the unexpected exception:

*** Errors: 1

line 2, col 25 to line 2, col 26 of module TestC

Internal error: should have name here.



tla2sany.xml.XMLExportingException: Failed to parse module.

[glondu]

I've managed to fix 25 cases in my branch.

However, I'm unsure about:

• 9d9229f: Is there a notion of illegal escapes in strings constants? How are they supposed to be handled?
• fb65e66: I don't understand why \X and \times cannot be passed as parameter while ## and \otimes can.

Are those expected?

[lemmy]

I've managed to fix 25 cases in my branch.

However, I'm unsure about:

• 9d9229f: Is there a notion of illegal escapes in strings constants? How are they supposed to be handled?
• fb65e66: I don't understand why \X and \times cannot be passed as parameter while ## and \otimes can.

Are those expected?

Are you referring to SANY or TLAPS parser behavior?

[glondu]

I've managed to fix 25 cases in my branch.
However, I'm unsure about:

• 9d9229f: Is there a notion of illegal escapes in strings constants? How are they supposed to be handled?
• fb65e66: I don't understand why \X and \times cannot be passed as parameter while ## and \otimes can.

Are those expected?

Are you referring to SANY or TLAPS parser behavior?

SANY

[lemmy]

Page 291 of https://lamport.azurewebsites.net/tla/xmxx00-02-09.pdf defines the legal escapes in strings constants. Page 269 explains that \X and \times is a special construct and not an ordinary infix operator.

[lemmy]

PR tlaplus/tlaplus#1401 includes fixes for the issues you reported. While it has not yet been reviewed and merged, using the changes from the PR should unblock your work in the meantime, if those issues were blocking you.

[glondu]

I've made progress on this.

As of 6b8ffe3, there are 44 failures. I've categorized them as follows:

• 1: case.txt
  • help needed
• 1: conjlist.txt
  • single_line is dropped
  • nested modules are dropped
• 1: disjlist.txt
  • same as in conjlist.txt
• 5: except.txt
  • in [f EXCEPT ![1, 1] = 0]: 1, 1 is parsed as a tuple
  • in [a EXCEPT ![2]["a"][3] = @ + 1]: "a" is parsed as an identifier
• 1: infix_op.txt
  • extra module_definition coming from TestPrelude
• 5: let_in.txt
  • 2: likely a bug in the XML Exporter
  • 3: recursive_declaration is dropped
• 4: modules.txt
  • 3: nested modules are dropped
  • 1: SANY bug, cf. naming a theorem after a submodule raises a parsing error tlaplus#430
• 3: number.txt
  • 1: SANY bug in parsing \h0123456789abcdef
  • 1: extra module_definition coming from TestPrelude
  • 1: SANY bug, cf. SANY differs from TLA+ language spec for parsing number values with decimals tlaplus#596
• 3: operators.txt
  • all due to SANY bug, cf. SANY fails to parse negative and !! operators in nonfix form tlaplus#884
• 1: postfix_op.txt
  • extra module_definition coming from TestPrelude
• 1: prefix_op.txt
  • extra module_definition coming from TestPrelude
• 5: proofs.txt
  • help needed
• 1: quantification.txt
  • conversion failure (Invalid number of bounds or operands to CHOOSE)
• 5: recursive.txt
  • 4: RECURSIVE not supported (?)
  • 1: unexplained SANY error about -.
• 1: sets.txt
• 1: step_expressions.txt
  • extra module_definition coming from TestPrelude
• 3: subexpressions.txt
  • 1: extra module_definition coming from TestPrelude
  • 2: help needed
• 1: unit.txt
  • module_definition is not local while it is expected to be
• 1: use_or_hide.txt
  • likely a bug in the XML Exporter