From 760589d0f5968a7c64264d925b3aa1ee9068d978 Mon Sep 17 00:00:00 2001
From: Manuel <mgrojo@gmail.com>
Date: Mon, 19 May 2025 14:24:20 +0200
Subject: [PATCH] coap_spark, coap_client 0.9.0 (#1486)

* coap_spark 0.9.0 (via `alr publish`)

* Include coap_client as subdir of the coap_spark repository

* coap_spark: remove unneded dependency for users

* Revert "coap_spark: remove unneded dependency for users"

This reverts commit d8c395bfa65f3e87dce9a2ec623d9f8dcbf15696.

The dependency is needed for SPARKlib, which is not packaged
separately from gnatprove.
---
 index/co/coap_client/coap_client-0.9.0.toml | 24 +++++++
 index/co/coap_spark/coap_spark-0.9.0.toml   | 69 +++++++++++++++++++++
 2 files changed, 93 insertions(+)
 create mode 100644 index/co/coap_client/coap_client-0.9.0.toml
 create mode 100644 index/co/coap_spark/coap_spark-0.9.0.toml

diff --git a/index/co/coap_client/coap_client-0.9.0.toml b/index/co/coap_client/coap_client-0.9.0.toml
new file mode 100644
index 00000000..1f71aa15
--- /dev/null
+++ b/index/co/coap_client/coap_client-0.9.0.toml
@@ -0,0 +1,24 @@
+name = "coap_client"
+description = "Client program for the CoAP-SPARK library"
+version = "0.9.0"
+
+authors = ["Manuel Gomez"]
+maintainers = ["Manuel Gomez <mgrojo@gmail.com>"]
+maintainers-logins = ["mgrojo"]
+licenses = "Apache-2.0 OR GPL-2.0-or-later"
+website = "https://github.com/mgrojo/coap_spark"
+tags = ["coap", "spark", "client", "iot", "protocol"]
+
+executables = ["coap_client"]
+
+[[depends-on]]
+coap_spark = "^0.9.0"
+
+[build-switches]
+"*".Style_Checks = ["-gnatyC"]
+"*".Ada_Version = "Ada2022"
+
+[origin]
+url = "git+https://github.com/mgrojo/coap_spark.git"
+commit = "3dc855f1cf5c730b512c9c782c82973a10f95c81"
+subdir = "client"
\ No newline at end of file
diff --git a/index/co/coap_spark/coap_spark-0.9.0.toml b/index/co/coap_spark/coap_spark-0.9.0.toml
new file mode 100644
index 00000000..e8c3c46a
--- /dev/null
+++ b/index/co/coap_spark/coap_spark-0.9.0.toml
@@ -0,0 +1,69 @@
+name = "coap_spark"
+description = "CoAP implementation formally verified with SPARK/Ada"
+long-description = """
+CoAP-SPARK is a library implementing the Constrained Application Protocol (CoAP)
+as defined in
+[RFC 7252](https://www.rfc-editor.org/rfc/rfc7252), developed in the SPARK 
+language, the formally verified subset of the Ada programming language.
+
+This version implements the client side of the protocol with some limitations:
+- It does not support block-wise transfers.
+- It does not support retransmission of messages.
+- It only supports NoSec and PreSharedKey security modes.
+
+See LICENSING for licensing information.
+"""
+version = "0.9.0"
+
+authors = ["Manuel Gomez"]
+maintainers = ["Manuel Gomez <mgrojo@gmail.com>"]
+maintainers-logins = ["mgrojo"]
+licenses = "Apache-2.0 OR GPL-2.0-or-later"
+website = "https://github.com/mgrojo/coap_spark"
+tags = ["spark", "coap", "iot", "protocol"]
+
+[[depends-on]]
+gnatprove = "^14.1.1"
+
+[build-switches]
+"*".Style_Checks = [
+    "-gnaty3" # Specify indentation level of 3
+    ,"-gnatya" # Check attribute casing
+    ,"-gnatyA" # Use of array index numbers in array attributes
+    ,"-gnatyB" # Check Boolean operators
+    ,"-gnatyb" # Blanks not allowed at statement end
+    ,"-gnatyC" # Check comments (1 space after --)
+    ,"-gnatye" # Check end/exit labels
+    ,"-gnatyf" # No form feeds or vertical tabs
+    ,"-gnatyh" # No horizontal tabs
+    ,"-gnatyi" # Check if-then layout
+    ,"-gnatyI" # check mode IN keywords
+    ,"-gnatyk" # Check keyword casing
+    ,"-gnatyl" # Check layout
+    ,"-gnatyM100" # Check maximum line length
+    ,"-gnatyn" # Check casing of entities in Standard
+    ,"-gnatyO" # Check that overriding subprograms are explicitly marked as such
+    ,"-gnatyp" # Check pragma casing
+    ,"-gnatyr" # Check identifier references casing
+    ,"-gnatyS" # Check no statements after THEN/ELSE
+    ,"-gnatyt" # Check token spacing
+    ,"-gnatyx" # Check extra parentheses
+    ]
+"*".Ada_Version = "Ada2022"
+
+# You might want to use the following to specify the path to the Colibri solver
+# [environment]
+# PATH.append = "/home/mgr/local/gnat-2021/libexec/spark/bin"
+
+[[depends-on]]
+wolfssl = "^5.8.0"
+
+[configuration.values]
+# This is needed only for compatibility with https://github.com/mgrojo/ikea-smartlight
+# You can set it to false, if you meed to disable it.
+wolfssl.STATIC_PSK = true
+
+[origin]
+commit = "81401167ac44c9178de4e130b1bd83228d62a3d2"
+url = "git+https://github.com/mgrojo/coap_spark.git"
+