[minor] test messages, Sterling menu filtering, fix

[tnelson]

Test Failures

Test failures are now highlighted better in the console. A test that fails because a counterexample exists will print a message like this, and then open Sterling to show the counterexample. In such cases, only that failing test run will be displayed in Sterling's run menu; no other runs will be available.

******************** TEST FAILED *******************
Test myTestName failed. Stopping execution.
Test failed due to finding a counterexample, which will be displayed in Sterling.
*****************************************************

If the test failed due to unsatisfiability or inconsistency (which are the same, from the solver's point of view) a similar message will print but Sterling will not open, since it would only be able to say "UNSATISFIABLE".

Fix: live server on test failure

Fixed an issue where a failed test instance would be loaded without the live server, which could result in trouble loading Sterling. (We had previously changed to the live server for security reasons and compatability with modern browsers.)

Sterling menu and tests

As before, users can pick from a menu of Forge commands, each of which corresponds to an instance iterator. However, we've made some changes to reduce clutter in the menu:

• Tests that have passed, but don't produce an instance in the process (such as assert ... is necessary ..., which passes only if no counterexample is found) will no longer appear in the Sterling menu.
• Tests that have passed, but do produce an instance (such as assert ... is sat) will continue to appear in the Sterling menu. This includes passing examples, so that a user can visually inspect the example instance if needed.

We will be watching feedback on this feature so we can improve the Sterling menu further.

Non-test commands, such as run, will not actually be run until the user has clicked the "Run" button in Sterling with the command selected. (This should be identical behavior to the prior release.)

Terminal Reporting

Unless the verbosity option is set to 0, passing tests will now print a message to the terminal.

Unless the verbosity options is set to 0, Forge will now print a "Solving for next instance." message to the terminal when "Run" or "Next" is clicked in Sterling.

The terminal message about hitting enter to stop Sterling now includes "or click 'Stop' in VSCode" to avoid confusion.

Minor Changes and Workarounds

Java detection

Added the java_exe_location option, which accepts a path to the Java executable that should be used to run the solver. This option isn't well-tested yet, so we suggest providing absolute paths and using it only if needed, e.g., if you have multiple Java installations.

If you are submitting models to an autograder, we suggest using this option only from the terminal via racket <filename.frg> -O java_exe_location <path>. Technically it can be used within a model file via option java_exe_location <path>, but the path given will not likely match the autograder's setup.