Asks users to activate TLC execution statistics

[lemmy]

The Toolbox nudges users to activate execution statistics to guide TLC development (see screenshot below). Please add similar functionality to the vscode TLA+ editor. 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).

The statistics are publicly available: https://exec-stats.tlapl.us/tlaplus.csv

[alygin]

Sure.

[lemmy]

The "toolbox" field has been modeled as a boolean but should change to indicate the actual IDE. I suggest we make this a sub-parameter of TLC's -tool parameter, i.e. -tool 2 causes TLC to report 2 in exec stats.

[alygin]

@lemmy, the implementation is in the v1.3 pre-release.

As for the TLC -tool option, I agree that it would be nice to distinguish various TLA+ IDE's by providing different values. But wouldn't a string value (like "toolbox", "vscode-tlaplus", or some kind of mnemonic, like "TB" or "VSC") be more convenient?

[lemmy]

Would it be difficult for the extension to set a Java system property (e.g. -Dtlc2.TLC.tool=vscode)?

[alygin]

Not difficult at all.
Does TLC already handle this property?

[lemmy]

No, but I have to think about how to best migrate the current reporting (evolve existing DB schema, ...).

Given that this is not a user but a developer feature, it doesn't make sense to make it available through the command line. Let's thus use -Dtlc2.TLC.toolName=vscode which TLC will ignore until support is implemented.

[lemmy]

Actually, I like "tlc2.TLC.ide" better.

[lemmy]

Added with tlaplus/tlaplus@fe63662. I suggest you include the TLC nightly build in the final 1.3.0 extension release?

Metabase:

[alygin]

I suggest you include the TLC nightly build in the final 1.3.0 extension release?

Is it stable enough?

[lemmy]

Yes, TLC development is very conservative.

[alygin]

Added to the latest v1.3 pre-release.

[lemmy]

There is a typo "plublicly" in the settings label: Allows you to send the TLC usage statistics to the plublicly available database. You can find more details on what is shared here.

Do you want me to create an exec-stats.md file in the https://github.com/tlaplus/tlaplus repo that lists the shared information?

[lemmy]

Should the drop-down in the settings show if a user has opted-in or not?? Here it shows "doNotShare" even though I have a ~/.tlaplus/esc.txt file with an identifier.

[alygin]

There is a typo

Thanks, fixed.

Do you want me to create an exec-stats.md?

Yeah, I think it would be more appropriate to have a page like this in the tlaplus/tlaplus repo, since it is the source of truth for such information. I'll change the link as soon as such page is available.

Should the drop-down in the settings show if a user has opted-in or not?

Actually, I thought I couldn't update configuration settings programmatically, but it looks like there's a method for that, so yes, I'll do that.

[lemmy]

https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/util/ExecutionStatisticsCollector.md

[alygin]

All fixes are available in the latest pre-release.

[alygin]

@lemmy, I think I'll stick to the stable tla2tools.jar bundled with the extension. Using nightlies will be possible after implementing #134.

[alygin]

Just released v1.3 with statistics sharing, so I'm closing the issue. Please, feel free to reopen it if sharing doesn't work as expected.

I'll put the -Dtlc2.TLC.ide=vscode option back when tla2tools 2.15 is released.

[lemmy]

There is no harm in passing -Dtlc2.TLC.ide=vscode to older TLC releases because it is ignored.

[alygin]

Yeah, I noticed that, but still decided to remove the option because some people look at the full TLC command line and they may be confused by this previously unknown option that actually does nothing at the moment.

[lemmy]

The link to the file explaining the content of the stats has changed to: https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/util/ExecutionStatisticsCollector.md