Merge branch 'release-3.12' into src. Close #44.

Author: ivanperez-keera

home.md

@@ -1,7 +1,7 @@
 ## News
-**Release 3.11 -- 2022-09-07**
+**Release 3.12 -- 2022-11-07**
 
-We are pleased to announce the release of Copilot 3.11, a stream-based DSL for
+We are pleased to announce the release of Copilot 3.12, a stream-based DSL for
 writing and monitoring embedded C programs, with an emphasis on correctness and
 hard realtime requirements. Copilot is typically used as a high-level runtime
 verification framework, and supports temporal logic (LTL, PTLTL and MTL),
@@ -10,21 +10,36 @@ clocks and voting algorithms.
 Among others, Copilot has been used at the Safety Critical Avionics Systems
 Branch of NASA Langley Research Center for monitoring test flights of drones.
 
-This new release introduces a new library copilot-interpreter that exposes the
-functions related to the interpreter backend, pre-existing functions included
-as part of copilot-core are now deprecated. It also fixes multiple bugs,
-removes deprecated elements, hides internal parts of the implementation from
-the public API, and improves the codebase by re-implementing a function without
-the use of unsafeCoerce. This release also continues to use our new software
-engineering process designed to meet the requirements to obtain NASA's Class D
-software classification. Details are available
-[here](https://github.com/Copilot-Language/copilot/milestone/15?closed=1).
-
-Current emphasis is on facilitating the use with other systems, improving the
-codebase in terms of stability and test coverage, removing unnecessary
-dependencies, hiding internal definitions, and formatting the code to meet our
-new coding standards. Users are encouraged to participate by opening issues and
-asking questions via our [github
+The main changes in this release are as follows:
+
+- A new library `copilot-prettyprinter` exposes functions related to the
+  Copilot Core pretty-printing backend. Pre-existing functions included as
+  part of `copilot-core` are now deprecated.
+- The C99 backend now produces an additional header file with struct
+  declarations. This file is used by the C implementation file generated by
+  Copilot to define structs before the declarations of the handlers, avoiding
+  potential forward declarations that the C compiler cannot resolve. Users of
+  Copilot can choose to import the same new type declaration header file before
+  the standard Copilot header file in their hand-written code, or use external
+  definitions that declare compatible structs. Note that, in the former case,
+  the header file that declares the structs must be included *before* the
+  header file that declares the externs, handlers and step function.
+- The custom type equality module in `copilot-core` is now deprecated in favor
+  of the definition of type equality in `base`.
+- `copilot-theorem` now includes support for proofs by bisimulation necessary
+  for future extensions to Copilot.
+- `copilot-core` now complies with the coding rules established as part of the
+  process of compliance with NASA's Class D requirements (NPR 7150.2).
+
+This release also continues to use our new software engineering process
+designed to meet the requirements to obtain NASA's Class D software
+classification. Details are available
+[here](https://github.com/Copilot-Language/copilot/milestone/16?closed=1).
+
+Current emphasis is on improving the codebase in terms of stability and test
+coverage, removing unnecessary dependencies, hiding internal definitions, and
+formatting the code to meet our new coding standards. Users are encouraged to
+participate by opening issues and asking questions via our [github
 repo](https://github.com/copilot-language/copilot).
 
 ## Licence