Added bug report template generator #1094

Kukovec · 2021-11-12T17:12:44Z

~~Tests added for any new code~~
Ran make fmt-fix (or had formatting run automatically on all files edited)
~~Documentation added for any new functionality~~
~~Entry added to UNRELEASED.md for any new functionality~~

Part 1 of addressing #943:
A bug report file is now automatically generated on FailureMessage in the run directory.

TODO: Add documentation/unreleased

shonfeder · 2021-11-15T15:47:58Z

I believe we can construct a URL that will open an issue on GitHub, with a parameterized template, rather than pointing users towards a file. Do you think this would be a nicer UI?

See: https://docs.github.com/en/enterprise-server@3.1/issues/tracking-your-work-with-issues/creating-an-issue#creating-an-issue-from-a-url-query

Kukovec · 2021-11-16T14:24:06Z

I believe we can construct a URL that will open an issue on GitHub, with a parameterized template, rather than pointing users towards a file. Do you think this would be a nicer UI?

See: https://docs.github.com/en/enterprise-server@3.1/issues/tracking-your-work-with-issues/creating-an-issue#creating-an-issue-from-a-url-query

We discussed this idea with Igor, and the overall conclusion is that it's beneficial to have an artificial barrier between error and bug report, for the simple reason that some users might now want to, or be allowed to, share their specs, and it'd be dangerous if they could accidentally misclick on a link and post the spec.

shonfeder

That makes sense, as far as motive for not using the URL to create an issue (tho I'll note that just following the URL doesn't automatically open an issue, the user would still have the chance to remove any sensitive info they wanted to).

I do have one question about the implementation details, regarding how the file location is threaded through, and one suggestion about the approach that leads us to implement an adhoc templating.

shonfeder · 2021-11-16T14:29:19Z

mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala

+            handleExceptions(injector, runParse(injector, parse))(parse.file)

          case Some(check: CheckCmd) =>
            val injector = injectorFactory(check)
-            handleExceptions(injector, runCheck(injector, check))
+            handleExceptions(injector, runCheck(injector, check))(check.file)

          case Some(test: TestCmd) =>
            val injector = injectorFactory(test)
-            handleExceptions(injector, runTest(injector, test))
+            handleExceptions(injector, runTest(injector, test))(test.file)

          case Some(typecheck: TypeCheckCmd) =>
            val injector = injectorFactory(typecheck)
-            handleExceptions(injector, runTypeCheck(injector, typecheck))
+            handleExceptions(injector, runTypeCheck(injector, typecheck))(typecheck.file)


It seems strange to me that the file is added as an extra argument in all these. Wouldn't the location of this file be a perfect fit for the OutputManager?

Not really, since this is not an output file, but the input specification file passed by the user. It's used to read the specification string, to copy into the issue body.

True the file is not input, but iiuc, it's only use it to construct output for the user (the report template)!

No, this file is the example.tla in e.g. check example.tla, which can be anywhere on the filesystem and doesn't get copied into the rundir at any point.

I understand that. But the only reason you need to pass it in here is in order to use it for generating the bug report output, no? Anyhow, this isn’t a critical thing. Just seems a bit off to me to be passing in additional arguments here when we already have access to the data via the output manager, which we need anyhow in the bug report template generator.

The thing is, the OutputManager doesn't know about this file, because it's not otherwise related to outputs.

It doesn't know currently, true :)

My main rationale here is about keeping the dataflow simple. With this change, we get something like the following:

CLIArgs -----------------------------------+ | | | | \/ \/ OutputManager ---------------> exceptionHandler ------> ReportGenerator

And what I'm advocating for is keeping this flat, mostly because I just don't see a good reason not to:

CLIArgs -----> OutputManager ---------------> exceptionHandler ------> ReportGenerator

The main practical implication being we don't need to extract and thread through the file argument for each subsequent invocation of the exceptionHandler we might add.

But the stakes around this are small, so happy to leave to your discretion.

That seems sensible, but at the same time, probably scope creep for this particular PR. You should make an issue for it though, since I can see it being relevant again with the other part of #943, where the error explainer displays the contents of the input file line where the issue is, for which it will need access to the source file too.

I think it should only a take a few lines of code to make the proposed change, but if you'd rather, perhaps leave a note on #1069 that this should be corrected as part of that work, and I can take care of it later this week?

shonfeder · 2021-11-17T04:25:11Z

tla-io/src/main/resources/issueTemplate.md

+<!-- Thank you for filing a report! Please ensure you have filled out all -->
+<!-- sections, as it help us to address the problem effectively. -->
+
+## Input specification
+
+```
+__SPEC
+```
+
+## The command line parameters used to run the tool
+
+```


Any added value to making this a standalone file that has to be included in the resources that you have in mind?

My initial thought is that this adds some unneeded complexity (an additional resource, then adhoc templating logic), but it seems our usecase could be served just as well with a function that has this string in and just uses Scala's string interpolation for templating. What do you think?

You could just have a string, that's true, but the string would be messy to write, and it's easy to edit the .md file as a standalone file to get the desired formatting. I guess string interpolation is better than replacement, so the question is really whether we intend to change the bug report template at all. If the answer is "not really", I suppose we can copy the file into a string.

IMO, it would simplify the code enough to justify, and editing a multiline string in a .scala file is just as easy as editing a multiline string a .md file IMO :) But I won't block on this and am OK leaving it up to whatever you think best.

I'm ambivalent on this, if you'd prefer a string it's easy enough to include.

So, the reasons for making it a string, imo, are these:

Eliminate an external resource.

Eliminate one IO operation.

Reduce the logic of this changeset (I think approximately halving it)?

The one advantage I've thought of for keeping this as an external .md file is that could enable us to keep the github issue template and this template in sync. However, that's not currently the case, and it's not immediately clear to me how we'd achieve that synchronization.

So, in my estimation, unless we want to invest in ensuring those two files are kept in sync, I do find the idea of just inlining the string preferable.

But, as I said, this isn't a super hard preference on my side.

shonfeder · 2021-11-17T13:58:22Z

tla-io/src/main/resources/issueTemplate.md

+<!-- Thank you for filing a report! Please ensure you have filled out all -->
+<!-- sections, as it help us to address the problem effectively. -->
+
+## Input specification
+
+```
+__SPEC
+```
+
+## The command line parameters used to run the tool
+
+```


IMO, it would simplify the code enough to justify, and editing a multiline string in a .scala file is just as easy as editing a multiline string a .md file IMO :) But I won't block on this and am OK leaving it up to whatever you think best.

shonfeder · 2021-11-17T13:59:08Z

mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala

+            handleExceptions(injector, runParse(injector, parse))(parse.file)

          case Some(check: CheckCmd) =>
            val injector = injectorFactory(check)
-            handleExceptions(injector, runCheck(injector, check))
+            handleExceptions(injector, runCheck(injector, check))(check.file)

          case Some(test: TestCmd) =>
            val injector = injectorFactory(test)
-            handleExceptions(injector, runTest(injector, test))
+            handleExceptions(injector, runTest(injector, test))(test.file)

          case Some(typecheck: TypeCheckCmd) =>
            val injector = injectorFactory(typecheck)
-            handleExceptions(injector, runTypeCheck(injector, typecheck))
+            handleExceptions(injector, runTypeCheck(injector, typecheck))(typecheck.file)


True the file is not input, but iiuc, it's only use it to construct output for the user (the report template)!

shonfeder · 2021-11-17T14:50:21Z

tla-io/src/main/scala/at/forsyte/apalache/io/ReportGenerator.scala

+
+    new File(
+        OutputManager.runDirPathOpt
+          .getOrElse(throw new IllegalStateException("run directory is not configured"))


Using OutputManager.runDir will already check for the state validity, and raise an appropriate error if its not configurd, so think this can OutputManager.runDir.resolve(reportFile).normalize.toString to

OutputManager.runDir does not exist.

apalache/tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala

Lines 78 to 85 in 79e00c1

/**

* Accessor for the configured run directory.

*

* @throws IllegalStateException if called before OutputManager is configured: this is considered an implementator error

*/

def runDir: Path = {

runDirOpt.getOrElse(throw new IllegalStateException("run directory does not exist"))

}

This is from a recent commit merged into unstable that isn't on this branch yet. I guess we can use that after I rebase in unstable.

Right. All our PR's should assume the code available in unstable I think.

Ah, but I understand. This was only just slipped in with the latest changes to the OutputManager I think. Make sense it wasn't used initially!

tla-io/src/main/scala/at/forsyte/apalache/io/ReportGenerator.scala

shonfeder · 2021-11-30T16:29:02Z

mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala

+            handleExceptions(injector, runParse(injector, parse))(parse.file)

          case Some(check: CheckCmd) =>
            val injector = injectorFactory(check)
-            handleExceptions(injector, runCheck(injector, check))
+            handleExceptions(injector, runCheck(injector, check))(check.file)

          case Some(test: TestCmd) =>
            val injector = injectorFactory(test)
-            handleExceptions(injector, runTest(injector, test))
+            handleExceptions(injector, runTest(injector, test))(test.file)

          case Some(typecheck: TypeCheckCmd) =>
            val injector = injectorFactory(typecheck)
-            handleExceptions(injector, runTypeCheck(injector, typecheck))
+            handleExceptions(injector, runTypeCheck(injector, typecheck))(typecheck.file)


I think it should only a take a few lines of code to make the proposed change, but if you'd rather, perhaps leave a note on #1069 that this should be corrected as part of that work, and I can take care of it later this week?

shonfeder · 2021-11-30T16:30:32Z

mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala

+                s"${Version.version} build ${Version.build}"
+            )
+            Console.err.println(
+                s"Please report an issue at $ISSUES_LINK: $e\nA bug report template has been generated at [$absPath]."


Suggested change

s"Please report an issue at $ISSUES_LINK: $e\nA bug report template has been generated at [$absPath]."

s"Please report an issue at $ISSUES_LINK: $e\nA bug report has been generated at [$absPath]."

Iiuc, we are generating the report using the template?

Technically, the user is still meant to fill in "Expected Behavior". I'll add a prompt to do that in the stdout string.

tla-io/src/main/scala/at/forsyte/apalache/io/ReportGenerator.scala

shonfeder · 2021-12-01T17:42:06Z

Whenever you're ready for me to have another look, please re-request review by clicking the little recycle symbol by my name in the requested reviewers :)

shonfeder

Two questions, but not all blocking. LGTM!

Nice that we have removed even more IO operations by caching the source file!

shonfeder · 2021-12-01T18:18:13Z

tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala

+  // Should be called only if input is a .tla file
+  def initSourceLines(file: File): Unit =
+    if (sourceLinesOpt.isEmpty) {
+      val src = Source.fromFile(file)
+      try sourceLinesOpt = Some(src.getLines().toIndexedSeq)
+      finally src.close()
+    }


Why should it only be called on TLA files? Why not also store the lines from other kinds of input?

Because JSON file lines don't correspond to anything sensible (in fact, the location fields in the JSON reference the original spec's line numbers) and tnt isn't implemented yet.

The JSON file lines would correspond to the JSON source data, at least. Couldn't we get an error that related to some data coming from a bit of bad json?

the location fields in the JSON reference the original spec's line numbers

This makes me wonder whether we are asking for trouble by introducing a new way to count line numbers (outside of the one we are currently using for source mapping.....).

Would the correct logic here not then be to parse the spec from the JSON file that was input and save that in memory here?

shonfeder · 2021-12-01T18:18:50Z

tla-io/src/main/scala/at/forsyte/apalache/io/ReportGenerator.scala

+
+  // Can't access Version in IO, have to pass at call site
+  def prepareReportFile(cmdStr: String, versionStr: String): String = {
+    val specTxt = OutputManager.getAllSrc.getOrElse("")


Should this perhaps return some message if the spec cannot be loaded? Like unable to read specification or something?

You mean as a log/stdout message or as a replacement for "" in getOrElse?
The latter sounds like a good idea, the former not so much. The only scenario where this returns "" is when you call Apalache on a .json file. In that case, there's really no spec to attach to the template (I do not want to encourage people to attach JSON specs in bug reports).

I meant in the generated bug template, yeah, just so we know what it means if we get an empty string there. Not at all critical. Makes sense about not getting giant json outputs :)

OK, it should now print a  in the else case.

shonfeder

Nice! Still LGTM :)

shonfeder

Sorry! I’d meant to approve before too.

Closes #1502 Followup to #1094, which added a file read for the debug template that is outside the scope of our standard error handling. The fix here is just to ensure the file exists before trying to initialize the "sourceLines" tracker.

Kukovec requested review from konnov and shonfeder November 12, 2021 17:12

shonfeder suggested changes Nov 17, 2021

View reviewed changes

Kukovec added 6 commits November 18, 2021 11:58

added bug report template generator

eaef8e7

that dumb java version thing with strip

64c47e9

file flag fix

2bd9601

tweaks

28ae0ff

docs&UR

11f8af9

PR comments

dc9d117

Kukovec force-pushed the jk/autoBugReport branch from c29025f to dc9d117 Compare November 18, 2021 11:29

fmt

eb7cb3e

shonfeder self-requested a review November 30, 2021 16:27

shonfeder suggested changes Nov 30, 2021

View reviewed changes

Kukovec added 3 commits December 1, 2021 17:55

PR comments

da5d75e

template completion prompt

aacddcc

Merge branch 'unstable' into jk/autoBugReport

2a52621

Kukovec requested a review from shonfeder December 1, 2021 17:58

shonfeder approved these changes Dec 1, 2021

View reviewed changes

tweaks

1af2953

shonfeder reviewed Dec 1, 2021

View reviewed changes

shonfeder approved these changes Dec 1, 2021

View reviewed changes

Kukovec merged commit 6857ddc into unstable Dec 1, 2021

Kukovec deleted the jk/autoBugReport branch December 1, 2021 19:30

This was referenced Dec 6, 2021

[release] 0.17.6 #1145

Closed

[release] 0.18.0 #1146

Merged

shonfeder mentioned this pull request Mar 17, 2022

Fix traceback on non-existent files #1503

Merged

3 tasks

	/**
	* Accessor for the configured run directory.
	*
	* @throws IllegalStateException if called before OutputManager is configured: this is considered an implementator error
	*/
	def runDir: Path = {
	runDirOpt.getOrElse(throw new IllegalStateException("run directory does not exist"))
	}

	s"Please report an issue at $ISSUES_LINK: $e\nA bug report template has been generated at [$absPath]."
	s"Please report an issue at $ISSUES_LINK: $e\nA bug report has been generated at [$absPath]."

Added bug report template generator #1094

Added bug report template generator #1094

Conversation

Kukovec commented Nov 12, 2021

shonfeder commented Nov 15, 2021

Kukovec commented Nov 16, 2021

shonfeder left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shonfeder commented Dec 1, 2021

shonfeder left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shonfeder left a comment

Choose a reason for hiding this comment

shonfeder left a comment

Choose a reason for hiding this comment