Asks users to activate TLC execution statistics

[lemmy]

The Toolbox asks users to activate execution statistics to guide TLC development (see screenshot below). Please add similar functionality to your extension. Technically, a file called esc.txt is dropped into ~/.tlaplus/ whose first line is either a random identifier, "RANDOM_IDENTIFIER", or "NO_STATISTICS" (see https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/util/ExecutionStatisticsCollector.java).

Plaintext of the dialog's content is found online too: https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/util/ExecutionStatisticsCollector.md. The statistics are publicly available: https://exec-stats.tlapl.us/tlaplus.csv. To report TLA+ Jupyter notebook as TLC's frontend, pass -Dtlc2.TLC.ide=tlaplus_jupyter as a Java system property.

@alygin VSCode extension will soon ask users to opt-in too.

---

Thanks for sharing TLA+ Jupyter notebooks with the community! I've already added your releases to the aggregator at http://wall.tlapl.us.

[kelvich]

Sure, will do.

[kelvich]

#5

I've created --tlc-exec-stats install option which is set to share by default. Also added note about that behavior to README.md. Any other suggestions? May be change wording somewhere?

[lemmy]

Have you tested this feature already? If yes, it seems as if it is broken because so far there have been no exec-stats for "tlaplus_jupyter" (d64477f#diff-8f9c6fbaedaf902848b1e9f9e47d60f2R253).

[kelvich]

I'm seeing my id (61a7f9a) now in tlaplus.csv now.
Does tla2tools v1.6.0 support tlc2.TLC.ide? I always download that version during install.

[lemmy]

No, only recent nightlies report the value of tlc2.TLC.ide.

[kelvich]

Okay, I'll then switch download to https://nightly.tlapl.us/dist/tla2tools.jar

[lemmy]

Great, but be aware of tlaplus/tlaplus#393 (comment)