v5.0.0

This update contains a BREAKING CHANGE: certain built-in helpers, such as sequences, are not automatically imported. Instead, use open util/<library name>. For the moment, libraries include util/temporal and util/sequences. This change avoids cluttering a model's namespace as we add more helpers, and makes Forge more extensible: new helpers can be written in Racket and added as new library modules.

Another breaking change is the upgrade to use the new CnD-powered Sterling visualizer. Existing custom-visualization functionality should continue to work, but the new visualizer also gives a constraint-based means of controlling layouts.

Other updates include improved type-checking and refactoring to pay down design debt.

Forge 4.2.1

This release corresponds to Forge's state as of June, 2025. It added:

• improved checking for predicate use, detecting mis-used predicate names.
• fixes for the crypto domain language, which could produce type errors under Forge's new predicate typechecking
• fix to allow sigs that extend Int
• improved detection of cyclic references between predicates and functions
• allow optional names in assert statements

Forge 4.1

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.

Forge v4.0

Forge 4.0 Release Notes

Forge 4.0 contains a number of new features and fixes from the previous version (3.7). There are breaking changes; please read the first 2 paragraphs carefully.

Anyone using the Forge VSCode extension should make sure to update that extension alongside updating Forge. We recommend enabling automatic updates for the extension.

Major Change: Sterling Run Menu

Sterling will now show a menu of available commands to execute, rather than commands being executed in sequence at the command prompt. Run Forge as normal (either via the Play button in the VSCode extension or via `racket in the command prompt) and Sterling will immediately load. Select a command from the drop-down and click "Run" to start the solver process and view instances for that command.

Breaking Change: #lang forge/froglet

For consistency, the Froglet language can now only be accessed via #lang forge/froglet. Forge had previously supported #lang froglet and #lang froglet/bsl (for "Beginner Student Language"). The new language name both avoids ambiguity and the need to install a separate Racket package.

Attempting to use #lang forge/bsl in Forge 4.0 will produce an error message.

Breaking Change: is checked vs. is theorem

The syntax of a test expect test that expects the predicate body to be valid has changed. Previously, one would write {<property>} is theorem, but this was inaccurate: Forge performs bounded verification of <property>, and so will now enforce the use of is checked so as not to connote completeness.

Sterling Fixes

Giving a filename to the run_sterling option will now properly pre-load the contents of that file into the script view window.

Theming will now persist between instances for the same command. Previously, theming was cleared for every new instance.

New Syntax

This release adds new assertion forms for consistency checking:

• assert <constraint> is consistent with <pred name> for <bounds>; and
• assert <constraint> is inconsistent with <pred name> for <bounds>.
  Moreover, the assert ... is necessary for ... and assert ... is sufficient for ... commands now support an arbitrary constraint block on the left hand side. Previously only a predicate name was allowed.

We strongly encourage the use of these new constructs rather than the old-style test expect {... is sat } and ... is unsat forms where possible.

For internal use, test expect now supports the is forge_error <?substr> expectation, which passes only if the run generates an error in Forge. Optionally, a substring may be provided that is matched against any error thrown.

Domain-Specific Model Fixes

The #lang forge/domains/crypto visualizer now properly displays the plaintext and key for encrypted terms if those terms have unexpected atom names.

The #lang forge/domains/crypto examples now include the missing Needham-Schroeder protocol as well as the fixed version of the protocol.

Initial Release for Spring 2024

This is the initial release for Spring semester of 2024.

Please keep Forge updated!