Add error handling for file loading #353

shonfeder · 2022-11-21T19:35:43Z

Closes #215

This is introduced in a way to suggest turning to sweet-monads/either
for sequencing our error-prone computations.

The sequencing and composition of our top-level routines exposed by CLI
is currently done via imperative early exits. This makes it hard to
reason about the code in general, but also breaks our ability to compose
these routines. Looking towards #345, we'll need typecheck to receive
the output of parse, then add it's typing information, before finally
printing to the --out location. This requires composing the routines
while handling possible error states, and just bailing with exit codes
won't work for that. Since we are already using Either, and since it
is designed for facilitating the composition of error-prone code, I
think we can massage these routines into shape with a few well-placed
Either's. ;)

I've added a few notes in commits and review comments to explain some of the
choices.

shonfeder · 2022-11-21T19:40:20Z

tntc/cli-tests.md

+<!-- !test program
+bash -
+-->
+
+<!-- !test in non-existent file -->
+    tntc parse ../examples/non-existent.file
+
+<!-- !test exit 1 -->
+<!-- !test err non-existent file -->
+    error: file ../examples/non-existent.file does not exist


I think this is closer to the intended usage of the txm library than what I see in this file. In particular, it saves us having to duplicate each example by writing the program input in a code block under the program. Removing this copy-pasta serves the aims of correctness, since it reduces the chance that the visible documentation of our tests will diverge from what is actually being tested.

This approach lets us specify program input and the expected output (along with any error codes) rather than having us define a new program for each test case. Because we are testing a CLI app, our "program" is just the shell, and and our input is the invocation of our command :)

If y'all agree, I can do a pass to fix the rest of the integration tests here. WDYT, @bugarela ?

Looks much better! Please do and I'd say you could close #42 on the way 😄

shonfeder · 2022-11-21T19:42:12Z

tntc/src/cli.ts

+  const res = loadFile(argv.input)
+  if (res.isRight()) {
+    return parseText(argv, res.value)
+  } else {
+    console.error(res.value)
+    process.exit(1)
+  }


This is not a nice way to handle the errors here: instead, we should chance the error-prone computations, and have error reporting at the outermost layer. But I'm introducing the change in this way just to open the conversation.

If anyone feels strongly about avoiding use of Either to faciliate composition of our error-apt computations here, I can revert this easily.

I think we should totally use Either here. There are some other parse and name resolution functions that return kind: 'ok' or kind: 'error' objects instead of Either because we wrote them before introducing the Either library. We should update all of them at some point.

Excellent. I'll swap this over while I'm refactoring to get the type map out. Thanks for the guidance and confirmation :)

shonfeder · 2022-11-21T19:42:47Z

tntc/src/cli.ts

 }

 // a callback to parse the text that we get from readFile
 function parseText(argv: any, text: string): [Phase1Result, LookupTableByModule, string] {
  const path = resolve(cwd(), argv.input)
  const phase1Result = parsePhase1(text, path)
  if (phase1Result.kind === 'error') {
-    reportError(argv, text, phase1Result)
+    reportParseError(argv, text, phase1Result)


This is just an incidental change to document the nature of this function, which is not suitable for general purpose error reporting.

shonfeder · 2022-11-21T20:12:32Z

Hmm, not sure why the windows test is failing... will have to try to debug a git. Unless anyone has alternative ideas on how to test the error output here.

bugarela

Thanks for looking into the integration tests!

bugarela · 2022-11-21T21:35:30Z

tntc/src/cli.ts

+  const res = loadFile(argv.input)
+  if (res.isRight()) {
+    return parseText(argv, res.value)
+  } else {
+    console.error(res.value)
+    process.exit(1)
+  }


I think we should totally use Either here. There are some other parse and name resolution functions that return kind: 'ok' or kind: 'error' objects instead of Either because we wrote them before introducing the Either library. We should update all of them at some point.

bugarela · 2022-11-21T21:39:35Z

Hmm, not sure why the windows test is failing... will have to try to debug a git. Unless anyone has alternative ideas on how to test the error output here.

My shell knowledge is very limited, specially on windows. Sorry, I have no idea. The only thing I thought was that you removed the --no-color flag that maybe was there for a reason? But doesn't seem related to the error message in the CI report at all.

shonfeder · 2022-11-21T23:17:04Z

The only thing I thought was that you removed the --no-color flag that maybe was there for a reason?

Funny enough, I removed this flag because it was failing on my system, with txm saying the flag is unsupported. But our CI isn't actually running that command, rather it runs https://github.com/informalsystems/tnt/blob/b31ff1f1e4b1aa6071564f1c29125a9e8d8e6bb8/.github/workflows/main.yml#L46 :)

I think the failure on windows was initially due to windows line endings not matching the line endings in the output to compare against... but not sure!

shonfeder · 2022-11-21T23:51:59Z

Looks to me like it may be a bug in tmx, and I've filed an issue anko/txm#10

Relative link will work on github but also for navigating around locally.

Closes #215 This is introduced in a way to suggest turning to sweet-monads/either for sequencing our error-prone computations. The sequencing and composition of our top-level routines exposed by CLI is currently done via imperative early exits. This makes it hard to reason about the code in general, but also breaks our ability to compose these routines. Looking towards #345, we'll need typecheck to receive the output of parse, then add it's typing information, before finally printing to the `--out` location. This requires composing the routines while handling possible error states, and just bailing with exit codes won't work for that. Since we are already using `Either`, and since it is designed for facilitating the composition of error-prone code, I think we can massage these routines into shape with a few well-placed Either's. ;)

`txm` does not support a `--no-color` flag as far as I can tell: indeed, we don't call it with this flag in our CI.

shonfeder · 2022-11-22T22:10:08Z

As per our discussion in the standup, I've broken out the IO integrations tests, i.e., those that actually inspect output, into their own file, and I've configured the workflow to only run that file if we are not on windows.

shonfeder · 2022-11-22T22:10:27Z

Thanks for the review!

Closes #42 Followup to #353 This cleans up the integration tests by setting the program to run tests as `bash`, and then using the `check` annotation to run the tntc command as input.

shonfeder requested review from bugarela and konnov and removed request for bugarela November 21, 2022 19:35

shonfeder commented Nov 21, 2022

View reviewed changes

bugarela approved these changes Nov 21, 2022

View reviewed changes

Shon Feder added 3 commits November 22, 2022 16:05

Fix link in readme

cee63da

Relative link will work on github but also for navigating around locally.

Fix txm invocation

b9cce5d

`txm` does not support a `--no-color` flag as far as I can tell: indeed, we don't call it with this flag in our CI.

shonfeder force-pushed the 215/fix-exception-on-missing-files branch 2 times, most recently from 41ca7b2 to 0dcffd8 Compare November 22, 2022 21:47

Add regression test for #215

2047dba

shonfeder force-pushed the 215/fix-exception-on-missing-files branch from 8340b36 to 5d3700e Compare November 22, 2022 22:05

Run io-cli-tests.md only on windows

a0cb9cb

shonfeder force-pushed the 215/fix-exception-on-missing-files branch from 5d3700e to a0cb9cb Compare November 22, 2022 22:09

shonfeder enabled auto-merge November 22, 2022 22:10

shonfeder merged commit dcb6252 into main Nov 22, 2022

shonfeder deleted the 215/fix-exception-on-missing-files branch November 22, 2022 22:12

This was referenced Nov 22, 2022

Remove redundant copy from integration test #355

Merged

Output typing map #345

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add error handling for file loading #353

Add error handling for file loading #353

shonfeder commented Nov 21, 2022

shonfeder Nov 21, 2022

bugarela Nov 21, 2022

shonfeder Nov 21, 2022

bugarela Nov 21, 2022

shonfeder Nov 21, 2022

shonfeder Nov 21, 2022

shonfeder commented Nov 21, 2022

bugarela left a comment

bugarela Nov 21, 2022

bugarela commented Nov 21, 2022 •

edited

Loading

shonfeder commented Nov 21, 2022

shonfeder commented Nov 21, 2022

shonfeder commented Nov 22, 2022

shonfeder commented Nov 22, 2022

Add error handling for file loading #353

Add error handling for file loading #353

Conversation

shonfeder commented Nov 21, 2022

shonfeder Nov 21, 2022

Choose a reason for hiding this comment

bugarela Nov 21, 2022

Choose a reason for hiding this comment

shonfeder Nov 21, 2022

Choose a reason for hiding this comment

bugarela Nov 21, 2022

Choose a reason for hiding this comment

shonfeder Nov 21, 2022

Choose a reason for hiding this comment

shonfeder Nov 21, 2022

Choose a reason for hiding this comment

shonfeder commented Nov 21, 2022

bugarela left a comment

Choose a reason for hiding this comment

bugarela Nov 21, 2022

Choose a reason for hiding this comment

bugarela commented Nov 21, 2022 • edited Loading

shonfeder commented Nov 21, 2022

shonfeder commented Nov 21, 2022

shonfeder commented Nov 22, 2022

shonfeder commented Nov 22, 2022

bugarela commented Nov 21, 2022 •

edited

Loading