Release Notes¶
1.5.0-beta.7 (25/04/2025)¶
Improvements:
- Functions on ports marked with
@noSideEffects
will now be marked asconst
in the generated C++ code whenlanguage.standard
is set to2024
. @ignoreWarning(.Unused)
can now be used on encapsulating components to suppress warnings about unconnected provided ports if this is expected.- Literal expressions are now bounds checked inside struct literals.
- C++: Added a
@mapToConstructor
attribute that can be used to indicate a function maps onto a constructor in C++. - C#: External components now have a virtual
Dispose
method that can be overridden to add custom dispose logic. - C++: The runtime header has now been split into a header and source file. This can be disabled by setting
generator.cpp.headerOnlyRuntime
tofalse
. This is enabled whenlanguage.standard
is set to2024
, and should result in faster compilation times when used. - The Popili Java API is now available as a Maven-compatible artifact.
- Log replay:
- Line numbers are now displaying counterexamples from log files.
- Add an option to suppress the error that is normally raised when no events match a monitor.
- Adds support for using the
VerifiedVector
type as a parameter type when replaying logs. - Adds an option to specify the maximum counterexample length, and improves the counterexample presentation so that it is clearer when the limit has been reached.
- VSCode:
- Improves the code completion behaviour to avoid problems where the editor would automatically select completion items in an unhelpful way.
- Text layout has been greatly improved in the counterexample diagrams.
- Improved the highlighting of functions that implement operators, such as
equals
. - Counterexamples now reopen when VSCode relaunches, providing the remote verification is being used.
- Improves the behaviour when a new project is created in VSCode by ensuring that the new project does not have any errors.
- The language identifier for Coco has been changed to
coco
to match other languages. - Improve the presentation of instance variables in the debugger.
- Improves the behaviour of verification whilst modifications are being made to the model: now the verification is not cancelled instantly, in case the change is actually semantics-preserving
Bug fixes:
- Frontend (command-line, VSCode and Eclipse):
- Code completion now respects
setAllow
filters on monitors. - Improve code completion behaviour when typing
:
in the editor. - Fixes a misleading error message when the
.clang-format
file contains an error. - Fixes obfuscation of type casts, such as
e as T
when generating support bundles. - Fixes a crash when incorrectly instantiating generic types with modules.
- Fixes a case where some side-effects inside arguments marked with
@noSideEffects
would not be rejected. - Fixes an issue with the code completion on signals which was suggesting a parameter called
returnValue
. - Fixes a crash when raising coco-tidy diagnostics on modules that have invalid names.
- If
Unreachable
is specified inlanguage.disabledWarnings
then this now correctly affects the verification. - Improves the behaviour of
popili
when executed on a Coco package that has no files. - Fixes several issues that could cause the junit output to be nondeterministic.
- Fixes a crash when exporting models that use state-machine inheritance via the EMF interface.
- Fixes a crash when creating encapsulating components that connect ports that do not have state machines.
- Code completion now respects
- Generators:
- All:
- Improved the handling of defaults on external types so that all generators are consistent with how they apply attributes related to initialisation.
- Fixes unused variables in the generated code for encapsulating components.
- Fixes a crash when generating code on models that use the
@implicitCast
attributes. - Fixes a crash when using
await
on components that have multiple required ports of the same type.
- C:
- Fixes several issues that could cause includes to be missing from the generated code. This would most commonly
affect uses of the
Log
trait.
- Fixes several issues that could cause includes to be missing from the generated code. This would most commonly
affect uses of the
- C++:
- Fixes a TODO that was incorrectly left in the C++ runtime header.
- Fixes an issue with the generated code when
generator.cpp.componentStyle
is set toHideImplementation
that would cause the code to not be compilable. - Fixes several bugs that could cause includes to be missing from the generated code. This would most commonly
affect uses of the
Log
trait.
- C#:
- Fixes a case where the
C#
profile was too strict and raised errors about name clashes that were not actually errors.
- Fixes a case where the
- All:
- Licensing:
- When acquiring licenses using external account credentials the proxy will no longer be used.
- Replay:
- Fixes replaying logs from stdin against multiple monitors.
- Fixes a crash when displaying counterexamples for certain logs.
- Fixes a crash when displaying some counterexamples from specific monitors.
- Verification:
- Fixes a crash when displaying some complex
@eventually
counterexamples.
- Fixes a crash when displaying some complex
- VSCode:
- Fixes a case where the verification statistics table would load with zeros.
- Fixes an issue that caused the verification statistics table to stop updating when files were modified in a semantics-preserving manner.
- Fixes a case where stale statistics would be shown in the verification statistics table.
- Fixes a rare crash on startup.
- Fixes the generation of code on workspaces that contain packages with
generator.cpp.generateCode
set tofalse
. - Fixes a bug that would cause counterexamples to be mis formatted when they exceeded a certain length.
- Fix crash when modifying Coco tidy settings.
- Fixes an issue that would prevent verification from being executed if cancellation was performed at certain points during the verification.
- Fixes a case where the plugin would incorrectly warn about a mismatch in the running version.
1.5.0-beta.6 (01/02/2025)¶
Bug fixes:
- Fixes an issue where the C# profile would incorrectly report that an external type’s name clashed with its parent.
- Fixes an issue that mean running code completion inside a monitor would not always respect any
setAllow
filters.
1.5.0-beta.5 (31/01/2025)¶
Bug fixes:
- Fixes an issue where the VSCode plugin would warn about the plugin version being out-of-date incorrectly.
1.5.0-beta.4 (29/01/2025)¶
New features:
There is a new Coco language standard available, called
2024
. This differs from1.2
as follows:Format strings now use the
Display
trait instead of theLog
trait by default. For example:$"Hello {name}"
would convert
name
to a String by invoking theDisplay
trait instead of theLog
trait.When value logging is enabled (as added in Popili 1.4), the generated code now logs signal sends. This can be disabled by setting the
generator.cpp.logSendSignals
option tofalse
.
Going forward, Coco language standards will use year-based versions instead of semantic versions to help disambiguate tool versions from language versions.
Improvements:
- VSCode: the various diagrams can now be saved in bitmap formats, in addition to SVGs.
- VSCode: diagrams can now be copied directly to the clipboard.
- VSCode: prompts to restart if
tool.selectedVersion
is modified. - VSCode: it is now possible to navigate from entries in the verification statistics table to the corresponding declaration, or to open other views such as the counterexample debugger.
- C: add support for the
Signal
datatype. - C#: add support for
generator.csharp.fileHeader
to allow a static file header to be prepended to a file. tool.selectedVersion
can now omit the patch version.
Bug fixes:
- Coco:
- Fixes an issue that caused
@derive(Default)
on generic enums to require all of its generic parameters to be defaultable, even if only a subset of them were required in the first enum case. - Fixes an issue where ports that have
@unbounded
transitions that write to variables that are read by non-unbounded transitions would not be rejected.
- Fixes an issue that caused
- Language Server:
- Fixes a crash when constructing invalid models that use the mixed runtime.
- VSCode:
- Fixes various issues that would result in diagrams opening over the top of editors.
- Fixes an issue that caused the architecture diagram to be blurry.
- Fixes an issue where panning one of the diagrams would also cause a click to be registered, leaving to editors opening unexpectedly.
- C#:
- Fixes an issued that prevented the generated code from compiling when multi-dimensional arrays of ports were used.
- Fixes an issue that would cause code generation to fail with filesystem errors.
- Fixes an issue where the generated code would contain errors relating to non-file-local types.
- Fixes a crash when generating code for Coco models that include and
unused()
handler with parameterised states. - Fixes an issue where the generated code incorrectly used
ref
in some cases. - Fixes a crash when generating code for Coco models that defaulted arrays of reference types.
- Fixes an issue that prevented the generated code from compiling when using multi-step port inheritance.
- Fixes an issue where
Result<T, E>
could not be defaulted whenT
is defaultable.
1.5.0-beta.3 (18/12/2024)¶
New features:
popili
now supports external authentication providers, enabling easier integration into CI environments that provide secure credentials, such as Github Actions or other cloud providers who use OIDC. Contact support@cocotec.io to set this up for your organisation.- Coco now has full support for 8, 16 and 32 bit signed and unsigned integers;
Base.coco
now containsInt8
,UInt8
etc.
Improvements:
popili replay
now permits multiple log files to be replayed at once.- VSCode: improves the initial placement of the counterexample diagram.
- VSCode: it is now possible to set the preferred verification backend directly within the VSCode preferences.
- VSCode: improves the opening of diagrams to more consistently not open the diagrams over the top of editors.
Bug fixes:
- Fixes a case where types declared inside monitors would cause code generation to crash.
- Fixes a crash when running code completion on types inside structs.
- Fixes a crash when generating C# for Coco code where an external member function was mapped to a non-member function.
- Fixes a case where the generated C# would not compile because the auto-generated Timer enum would contain duplicated values.
- Fixes a case where the format specifiers in format strings would be broken by the auto-formatter.
- Fixes a case where you could not pass an immutable reference to a struct field.
- Fixes a crash when running code completion on component constructors.
- VSCode: fixes a case where the keyboard arrows would not scroll the counterexample diagram.
- VSCode: fixes a case where the counterexample diagram would still be visible even if a non-Coco debug session was active.
1.5.0-beta.2 (26/11/2024)¶
Improvements:
- Types that are not defaultable in C++ code can now be used as the types of state machine variables.
- Improves verification cache hit rate when only comments are changed.
- Added a generate command to the
popili
command-line tool that will generate code for the language set ingenerator.defaultLanguage
. This is a language-neutral variant of thegenerate-cpp
subcommand. - Improves the fixits for unused parameters to suggest replacing the name with
_
. - Coco tidy is now able to enforce naming standards on transition names and labels.
- Improves the behaviour of the state diagram and architecture diagrams when a license is lost.
- Coco will now auto-generate warning supressions for unused parameters in C when it has to generate a name in order to comply with the C standard.
Bug fixes:
- Fixes the verification progress counters in VSCode, so that they correctly sum to 100%.
- Fixes several crashes that could occur when running Verification via VSCode in certain cases.
- Fixes an error reported in the VSCode plugin when restoring the state diagram after relaunching.
- Improves the behaviour of the VSCode plugin when launching the simulator or a counterexample whilst also debugging a non-Coco system.
- Fixes an issue with the VSCode plugin that would mean that the counterexample was not scrolled to the end on startup.
- Fixes a case where the language server would produce stale diagnostics in rare cases when modifications were made to
the files in one of the folders listed under
sources
ortestSources
, or if the folders were deleted. - Fixes a crash in the language server that could occur whilst editing Coco.toml files.
- Fixes a crash in the language server following a user verification error, such as loosing connection to the verification servers.
- Fixes a crash in the language server whilst typechecking invalid monitors that used arrays.
- Fixes a crash in the language server whilst running code completion on nested function calls.
- Fixes an issue that would mean the diagram pause status was not correctly updated when the diagram was restored.
- Fixes an internal error when verifying models that used function pointers stored in state parameters that included non-verified parameters.
- Fixes a crash in the language server when launching the simulator and stepping at a granular level.
- Fixes a crash when typechecking components that have incorrectly typed private variables.
1.5.0-beta.1 (08/11/2024)¶
New features:
The Coco Platform is now known as Popili, and all of our tools have been updated to reflect this. This includes the command-line tool, which is now invoked as
popili
instead ofcoco
. If you are using the automatic downloader added in 1.4, then no changes are required: this will transparently use the correct name based on the version. The Eclipse and VSCode plugins will auto-update to the new names as part of the usual update processes with no user intervention required.The Popili VSCode plugin has been significantly enhanced and it is now able to be used as a full development environment for Coco. The plugin currently includes:
- Support for running the verification and debugging counterexamples:
- Popili for VSCode includes a verification tree that shows all Coco models in your package in a similar way to Eclipse, but using the native VSCode controls and UI paradigms.
- Behavioural counterexamples are presented as a sequence diagram but are integrated with VSCode’s native debugger.
- Reachability counterexamples are presented via a separate interface and show as inline annotations on the editor showing which lines are reachable or unreachable. (More views will follow.)
- Verification statistics are also available as a table, which allows for a quick overview of which models are taking the longest to verify.
- The verification has been deeply integrated into VSCode, and statistics and verification results are now shown as contextual information in the editor (e.g. in tooltips) in relevant places.
- The simulator. This uses the same debugger and sequence diagram viewer as the counterexamples. Compared to Eclipse, the VSCode simulator is significantly easier to drive purely via the keyboard.
- Support for generating code, either via a dedicated command in VSCode’s command palette, or via a button on the assertions tree (like Eclipse).
- Support for helping users get started, including:
- A welcome page that integrates with VSCode’s welcome pages, helping new users get a license and open their first Coco project with Popili.
- A command to install the Coco examples.
- A command to create a new project in a given folder.
- A command to create a support bundle when users run into problems.
- Vastly improved licensing support:
- The login process will no longer happen on its own; instead you can click login at the point you want to start authenticating.
- The license status is clearly shown in the Popili status icon in the icon bar, and various options are provided to login.
- Popili for VSCode now supports offline licenses.
- Support for floating licenses has been improved, as users are now able to choose when to activate Popili and thus attempt to acquire the floating license.
- Improved integration between VSCode and Popili features:
- The architecture and state diagrams now automatically restore when VSCode is re-opened, and also update promptly after edits are completed, rather than just on save.
- Improved support for VSCode’s remote feature, where the language server runs on a remote connection.
- The counterexample diagrams are themed using VSCode’s native themes.
- The architecture and state diagrams now use controls that are natively styled by VSCode.
More features will follow.
- Support for running the verification and debugging counterexamples:
The Coco language now incorporates a
Display
trait that is intended to allow users to define methods for converting types into human-readable strings (unlikeLog
, which is intended for both human and machine-readable representations). For example:Display can be used in format strings by using the
d
format specifier:{e:d}
means print the value of expressione
using theDisplay trait.
Improvements:
Language:
Coco now includes specific syntax for ranges.
0..5
is equivalent torange(0, 5)
(i.e. up-to but not including5
), whilst0..=5
is equivalent toclosedRange(0, 5)
(i.e. up-to and including5
).Type aliases can be declared inside external types and structs.
type(e)
can now be used as a type to extract the type of an expressione
.Transitions that are marked as illegal must now use
_
as their parameter name.The builtin Coco
Base
module is no longer treated like an unqualified import, allowing users to define their own types that override the types inBase
. This will help ensure that as Coco’s standard library is enlarged, user code will not break even if it uses the same names.Formatter
now contains overloads ofwriteInt
for non-verified types.The
Vector2
vectors types now have aSize
member type. For example when combined with thetype
operator, this allows the following code to be written:var x : Vector2.BoundedVector<NonVerified<Int>, 5>; var pos : type(x).Size = x.size();
The
Duration
-construction functions, includingseconds
etc can now be used at the module-level as part of constants.
Tooling:
- VSCode now displays the Device Code more prominently during the login process.
- Deprecated or unused declarations now have more distinct styling when using VSCode.
- A warning is now generated when if
tooling.selectedVersion
is set to an unsupported version of Popili. - Code completion hints on encapsulating components have been improved, particularly when using external implementation components.
- Models that contain stack overflows due to, for instance, unbounded recursion, are now caught by the verification and helpful counterexamples are now produced.
- The layout of keywords in the documentation has now been improved.
- The log replay now allows parameters or return values that are not used by the monitor to be omitted from the logs.
Code Generation:
- Whether the generated C++ mocks are header-only or not can be controlled via the
generator.cpp.headerOnlyMocks
setting. This defaults to true, but can be set to false in which case a .cc file will be generated as well. Testing
now containsNiceMock
which will map to GMock’s :icpp:`testing::NiceMock` class in the generated code.
- Whether the generated C++ mocks are header-only or not can be controlled via the
Bug fixes:
- Fixes a case where the code completion documentation was incorrect for generic types.
- Fixes a case where code completion items involving
.
would be auto-selected in VScode, leading to confusing code completion behaviour. - Fixes an issue with running the language server on Windows where it would not reload files when they change on disk under some circumstances.
- Fixes several crashes with the language server whilst editing Coco.toml files.
- Fixes a case where diagnostics would not be updated inside the editor if a file was modified outside of the editor (e.g. via git).
- Fixes several issues that meant that working with Coco workspaces that contained invalid Coco packages would give misleading diagnostics.
- Fixes several issues creating support bundles, including incorrect Coco being printed, and also cases where the TOML files were not correctly synthesised making the resulting bundle malformed.
- Fixes an issue that prevented referring to trait instance functions without qualification even within the trait instance declaration.
- Fixes several issues that caused the generated C++ code to contain unused variables under some configurations.
- Fixes an issue with the simulator that meant it would not report errors raised during initialisation.
- Fixes an issue that meant creating a support bundle in Eclipse would corrupt the names displayed in the assertions tree.
1.4.7 (25/11/2024)¶
- Fixes an issue with the generated C and C++ code where the
generator.cpp.fileHeader
setting would not be respected for runtime files under some conditions.
1.4.6 (15/11/2024)¶
- Fixes an issue with the generated code that meant that characters would not be escaped correctly when logging strings. This affects all languages.
- Fixes an issue that would cause escaped null characters in string literals (i.e.