Merge branch 'develop-update-docs' into develop. Close #220.

**Description**

Some of the documentation of Ogma, such as the READMEs of the cocospec
and smv language processing modules, still contains references to the
way that Ogma was designed in older version. As Ogma has evolved over
time and requirements have changed, these references are no longer
applicable.

**Type**

- Management: Adjust documentation to match new requirements.

**Additional context**

None.

**Requester**

- Ivan Perez.

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

The documentation no longer contains references to tools based on the
design of the initial versions of Ogma.

**Solution implemented**

Remove references to old design of Ogma from documentation.

Remove references to old design of Ogma from hlint files.

**Further notes**

None.

Author: ivanperez-keera

ogma-core/.hlint.yaml

@@ -3,8 +3,3 @@
 
 # Ignore in automatically generated files.
 - ignore: {within: [Paths_ogma_core]}
-
-# We use data instead of newtype for uniformity.
-- ignore: { name: Use newtype instead of data
-          , within: [ Command.FRETReqsDB2Copilot ]
-          }

ogma-core/CHANGELOG.md

@@ -1,8 +1,9 @@
 # Revision history for ogma-core
 
-## [1.X.Y] - 2025-01-26
+## [1.X.Y] - 2025-01-27
 
 * Import liftIO from Control.Monad.IO.Class (#215).
+* Remove references to old design of Ogma from hlint files (#220).
 
 ## [1.6.0] - 2025-01-21
 

ogma-language-cocospec/CHANGELOG.md

@@ -1,5 +1,9 @@
 # Revision history for ogma-language-cocospec
 
+## [1.X.Y] - 2025-01-27
+
+* Remove references to old design of Ogma from documentation (#220).
+
 ## [1.6.0] - 2025-01-21
 
 * Version bump 1.6.0 (#208).

ogma-language-cocospec/ogma-language-cocospec.cabal

@@ -53,8 +53,7 @@ description:         Ogma is a tool to facilitate the integration of safe runtim
                      <https://github.com/Copilot-Language/copilot Copilot>, a high-level runtime
                      verification framework that generates hard real-time C99 code.
                      .
-                     This library contains a frontend to read CoCoSpec Boolean expressions, used by
-                     the tool FRET to capture requirement specifications.
+                     This library contains a frontend to read CoCoSpec Boolean expressions.
 
 -- Ogma packages should be uncurated so that only the official maintainers make
 -- changes.

ogma-language-smv/CHANGELOG.md

@@ -1,5 +1,9 @@
 # Revision history for ogma-language-smv
 
+## [1.X.Y] - 2025-01-27
+
+* Remove references to old design of Ogma from documentation (#220).
+
 ## [1.6.0] - 2025-01-21
 
 * Version bump 1.6.0 (#208).

ogma-language-smv/grammar/SMV.cf

@@ -28,11 +28,9 @@
 -- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS
 -- AGREEMENT.
 
--- This is a simplified grammar of SMV temporal logic expressions, extended
--- with the tags that FRET uses around names.
---
--- The format of FRET files itself uses JSON, so this grammar applies
--- only to specific fields in those files.
+-- This is a simplified grammar of SMV temporal logic expressions. This grammar
+-- allows for the presence of tags around some expressions, which some tools
+-- that produce SMV include in expressions.
 
 entrypoints BoolSpec;
 

ogma-language-smv/ogma-language-smv.cabal

@@ -53,8 +53,7 @@ description:         Ogma is a tool to facilitate the integration of safe runtim
                      <https://github.com/Copilot-Language/copilot Copilot>, a high-level runtime
                      verification framework that generates hard real-time C99 code.
                      .
-                     This library contains a frontend to read SMV Boolean expressions, used by
-                     the tool FRET to capture requirement specifications.
+                     This library contains a frontend to read SMV Boolean expressions.
 
 -- Ogma packages should be uncurated so that only the official maintainers make
 -- changes.