Workflow for defining new interactive test cases

1. Manually figure out what the command is supposed to output under success and failure situations.

   To do so, first construct an example file to test the command on, e.g. t/interactive/commands/load-success.bel with the contents

   LF tm : type =
       | c : tm
       | lam : (tm -> tm) -> tm
       | app : tm -> tm -> tm
   ;
   
   rec id : tm -> tm = fn x => x;
   

   Next, start the interactive mode, bin/beluga -I -emacs. Try the commands you're interested in, e.g. %:load t/interactive/commands/load.bel and note what the output is.

2. Write the request-response clauses in the test case file.

   In this case, append to t/interactive/commands/load-success.bel the following contents:

   %:load input.bel
   - The file input.bel has been successfully loaded;
   

   The Replay test harness renames input files to input.bel so make sure to use that file name to obtain the test input. (Recall that the test input is the part of the test file that precedes the very first interactive command.)

3. Try the test case with the harness.

   Run bin/replay t/interactive/commands/load-success.bel. It should show the request-response clauses, and exit with code 0 if it succeeds. If there is a mismatch in the expected and actual response from Beluga, Replay will show this.

If the test passes in isolation, try running the full test suite with ./TEST. Finally, add and commit the new test case.