Re: Testing issues for Ada/SPARK support in Babel

[Francesc Rocher <francesc.rocher@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 1052 bytes --]

Hi Ihor,

The patch is almost finished: refactored support for Ada and SPARK, tests
and documentation of custom variables.
The only pending thing is to write the changes in the NEWS files and other
minor changes.

If you don't mind, I attach here the patch in its current state for
reviewing purposes.

BR,
-- Francesc Rocher


On Mon, May 13, 2024 at 10:08 AM Ihor Radchenko <yantar92@posteo.net> wrote:

> Ihor Radchenko <yantar92@posteo.net> writes:
>
> > Francesc Rocher <francesc.rocher@gmail.com> writes:
> >
> >> I'm starting from scratch the set of tests for Ada/SPARK support in
> Babel.
> >> I've prepared a file with the first example:
> > ...
>
> It has been a while since the last update in this thread.
> May I know if you need any help to progress on your work?
>
> --
> Ihor Radchenko // yantar92,
> Org mode contributor,
> Learn more about Org mode at <https://orgmode.org/>.
> Support Org development at <https://liberapay.com/org-mode>,
> or support my work at <https://liberapay.com/yantar92>
>

[-- Attachment #1.2: Type: text/html, Size: 2024 bytes --]

[-- Attachment #2: 0001-Initial-support-for-Ada-SPARK.patch --]
[-- Type: text/x-patch, Size: 35271 bytes --]

From 806da098552f05bd4c3af82ba54bdae8c1ad54f1 Mon Sep 17 00:00:00 2001
From: Francesc Rocher <francesc.rocher@gmail.com>
Date: Thu, 21 Mar 2024 08:46:33 +0100
Subject: [PATCH] Initial support for Ada/SPARK

---
 lisp/ob-ada-spark.el                   | 496 +++++++++++++++++++++++++
 testing/examples/ob-ada-spark-test.org | 300 +++++++++++++++
 testing/lisp/test-ob-ada-spark.el      | 240 ++++++++++++
 3 files changed, 1036 insertions(+)
 create mode 100644 lisp/ob-ada-spark.el
 create mode 100644 testing/examples/ob-ada-spark-test.org
 create mode 100644 testing/lisp/test-ob-ada-spark.el

diff --git a/lisp/ob-ada-spark.el b/lisp/ob-ada-spark.el
new file mode 100644
index 000000000..79f40df69
--- /dev/null
+++ b/lisp/ob-ada-spark.el
@@ -0,0 +1,496 @@
+;;; ob-ada-spark.el --- org-babel functions for Ada & SPARK -*- lexical-binding: t; -*-
+
+;; Copyright (C) 2021-2024 Free Software Foundation, Inc.
+
+;; Author: Francesc Rocher
+;; Maintainer: Francesc Rocher
+;; Keywords: literate programming, reproducible research, Ada/SPARK
+;; URL: https://orgmode.org
+
+;; This file is part of GNU Emacs.
+
+;; GNU Emacs is free software: you can redistribute it and/or modify
+;; it under the terms of the GNU General Public License as published by
+;; the Free Software Foundation, either version 3 of the License, or
+;; (at your option) any later version.
+
+;; GNU Emacs is distributed in the hope that it will be useful,
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;; GNU General Public License for more details.
+
+;; You should have received a copy of the GNU General Public License
+;; along with ob-ada-spark. If not, see <https://www.gnu.org/licenses/>.
+
+;;; Commentary:
+
+;; Org-Babel support for evaluating Ada & SPARK code and proving SPARK code.
+
+;;; Requirements:
+
+;; * An Ada compiler (gnatmake)
+;; * A SPARK formal verification tool (gnatprove)
+;; * Emacs ada-mode, optional but strongly recommended, see
+;;   <https://www.nongnu.org/ada-mode/>
+
+;;; Code:
+
+(require 'ob)
+(require 'time-stamp)
+
+(org-assert-version)
+
+(defvar org-babel-tangle-lang-exts)
+(add-to-list 'org-babel-tangle-lang-exts '("ada" . "adb"))
+
+(defvar org-babel-temporary-directory)
+
+(defvar org-babel-default-header-args:ada '((:args . nil)
+                                            (:cflags . nil)
+                                            (:pflags . nil)
+                                            (:prove . nil)
+                                            (:template . nil)
+                                            (:unit . nil)
+                                            (:with . nil))
+  "Ada/SPARK default header arguments.")
+
+(defconst org-babel-header-args:ada '((args . any)
+                                      (cflags . any)
+                                      (pflags . any)
+                                      (prove . ((nil t)))
+                                      (template . :any)
+                                      (unit . :any)
+                                      (with . nil))
+  "Ada/SPARK specific header arguments.")
+
+(defconst ob-ada-spark-template-var-name-format "ob-ada-spark-template:%s"
+  "Format of the name of the template variables.
+All templates must be defined in a variable with a name
+compatible with this format. The template name is only the '%s'
+part. From the source block, templates can be used in the
+':template' header with the template name.
+
+For example, the template defined in the variable
+`ob-ada-spark-template:ada-main' is used in the header of the
+source block with ':template ada-main'.")
+
+(defcustom org-babel-ada-spark-compile-command "gnatmake"
+  "Command used to compile Ada/SPARK code into an executable.
+May be either a command in the path, like gnatmake, or an
+absolute path name.
+
+If using Alire 2.x, install the default native toolchain, with
+`alr install gnat_native', and write here the path to gnatmake or
+append $HOME/.alire/bin to PATH."
+  :group 'org-babel
+  :type 'string
+  :package-version '(Org . "9.7")
+  :safe #'stringp)
+
+(defcustom org-babel-ada-spark-prove-command "gnatprove"
+  "Command used to prove SPARK code.
+May be either a command in the path, like gnatprove, or an
+absolute path name, like /opt/ada/bin/gnatprove.
+
+If using Alire 2.x, install gnatprove, `alr install gnatprove',
+and write here the path to gnatprove or append $HOME/.alire/bin
+to PATH."
+  :group 'org-babel
+  :type 'string
+  :package-version '(Org . "9.7")
+  :safe #'stringp)
+
+(defcustom org-babel-ada-spark-default-compile-flags
+  "-f -we -gnata -gnateF -gnateV -gnatf -gnatVa -gnatwa -gnatX -gnat2022 -gnatW8"
+  "Default compiler flags for Ada and SPARK.
+These flags are used to compile Ada and SPARK code. Any
+additional flags specified in the ':clfags' header is passed
+after the default ones.
+
+Default flags for gnatmake are:
+
+  -f        Force recompilations of non predefined units
+  -we       Treat all warnings as errors
+  -gnata    Assertions enabled. Pragma Assert/Debug to be activated
+  -gnateF   Check overflow on predefined Float types
+  -gnateV   Validity checks on subprogram parameters
+  -gnatf    Full errors. Verbose details, all undefined references
+  -gnatwa   Enable selected warning modes (turn on all info/warnings)
+  -gnatX    Language extensions permitted
+  -gnat2022 Ada 2022 mode
+  -gnatW8   Wide character encoding method (?=h/u/s/e/8/b)
+"
+  :group 'org-babel
+  :type 'string
+  :package-version '(Org . "9.7")
+  :safe #'stringp)
+
+(defcustom org-babel-ada-spark-default-prove-flags
+  "-f --assumptions --level=4 --report=all --verbose"
+  "Default flags for gnatprove.
+These flags are used to prove SPARK code. Any additional flag
+specified in the ':pflags' header is passed after the default
+ones.
+
+The compiler flags are also passed to gnatprove using the
+'-cargs' flag, both the the default flags in
+`org-babel-ada-spark-default-compile-flags' and the flags
+specified in the ':cflags' header, in that order.
+
+Default flags for gnatprove are:
+
+  -f                Force recompilation/analysis of all units
+  --assumptions     Output assumptions information
+  --level=4         Set the level of proof (0 = faster to 4 = more powerful)
+  --report=all      Set the report mode of GNATprove (r=fail*, all,
+                    provers, statistics)
+  --verbose         Output extra verbose information
+"
+  :group 'org-babel
+  :type 'string
+  :package-version '(Org . "9.7")
+  :safe #'stringp)
+
+(defcustom org-babel-ada-spark-default-file-header
+  (lambda ()
+    (format
+     "-----------------------------------------------------------------------------
+--
+--  Source code generated automatically by 'org-babel-tangle' from
+--  file %s
+--  %s
+--
+--  DO NOT EDIT!!
+--
+-----------------------------------------------------------------------------
+
+"
+     (buffer-file-name (current-buffer))
+     (time-stamp-string "%Y-%02m-%02d %02H:%02M:%02S")))
+  "Header written in files generated with `org-babel-tangle'."
+  :group 'org-babel
+  :type 'function
+  :package-version '(Org . "9.7"))
+
+(defvar ob-ada-spark-template:ada-main
+  '((:params . ((:unit . "main") (:cflags . "-gnatW8")))
+    (:body . "with Ada.Text_IO; use Ada.Text_IO;
+%s
+procedure Main is
+%s
+end Main;
+"))
+  "Template for a basic Main procedure written in Ada 2022.
+Makes use of the Ada.Text_IO (with and use clauses). Admits
+additional with'ed packages and a procedure body.
+
+Use this template as a starting point for new Ada templates. All
+templates must include two placeholders, for the with section and
+for the body.
+
+Example of use:
+
+#+begin_src ada :template ada-main :with System.OS_Lib
+   Time : constant String := Current_Time_String;
+begin
+   Put_Line (Time);
+#+end_src
+
+The resulting body is:
+
+with Ada.Text_IO; use Ada.Text_IO;
+with System.OS_Lib; use System.OS_Lib;
+
+procedure Main is
+   Time : constant String := Current_Time_String;
+begin
+   Put_Line (Time);
+end Main;
+")
+
+(defvar ob-ada-spark-template:spark-main
+  '((:params . ((:cflags . "-gnatW8") (:prove . t) (:unit . "main")))
+    (:body . "with Ada.Text_IO; use Ada.Text_IO;
+%s
+procedure Main with Spark_Mode => On is
+%s
+end Main;
+"))
+  "Template for a basic Main procedure written in SPARK.
+Makes use of the Ada.Text_IO (with and use clauses). Admits
+additional with'ed packages and a procedure body.
+
+Use this template as a starting point for new SPARK templates. All
+templates must include two placeholders, for the with section and
+for the body.
+
+Example of use:
+
+#+begin_src ada :template ada-main :with System.OS_Lib
+   Put_Line (Current_Time_String);
+#+end_src
+
+The resulting body is:
+
+with Ada.Text_IO; use Ada.Text_IO;
+with System.OS_Lib; use System.OS_Lib;
+
+procedure Main is
+begin
+   Put_Line (Current_Time_String);
+end Main;
+")
+
+(defun ob-ada-spark-replace-params-from-template (params)
+  "Replace headers in PARAMS with headers defined in the template.
+If a template defines a set of params, replace the values in
+PARAMS with the values defined in the template, overwriting
+parameters already defined in the source code block.
+Return the new list of PARAMS, or the original list if the
+template does not define any header or no template is used."
+  (let* ((template-name (cdr (assq :template params)))
+         (template (eval
+                    (intern-soft
+                     (format ob-ada-spark-template-var-name-format
+                             template-name)))))
+    (if template
+        (progn
+          (message "-- replacing params from template %s" template-name)
+          (mapc (lambda (p)
+                  (assq-delete-all (car p) params))
+                (cdr (assq :params template)))
+          (append params (cdr (assq :params template))))
+      params)))
+
+(defun org-babel-expand-body:ada (body params)
+  "Expand BODY according to PARAMS and return the expanded body.
+Body expansion comprises replacement of template and literal
+variables.
+First, template is filled with the value of ':with' and ':body'
+headers in PARAMS. Second, all literal variables are replaced by
+the values found in the ':var' header of PARAMS."
+  (let* ((template-name (cdr (assq :template params)))
+         (template (eval
+                    (intern-soft
+                     (format ob-ada-spark-template-var-name-format
+                             template-name))))
+         (vars (org-babel--get-vars params))
+         (with (cdr (assq :with params))))
+
+    (if (and template-name (null template))
+        (error
+         "Invalid template name '%s', variable ob-ada-spark-template:%s undefined"
+         template-name template-name))
+
+    ;; Use the body defined in the template, if any. It needs two
+    ;; parameters: the 'with' section (defined in params) and the
+    ;; 'body' section (the contents of source code block)
+    (setq body
+          (if template
+              (progn
+                (message "-- expanding body from template %s" template-name)
+                (format
+                 ;; body's template as format control string
+                 (cdr (assq :body template))
+                 (if (null with) ""
+                   ;; replace :with parameter
+                   (mapconcat
+                    (lambda (w) (format "with %s; use %s;\n" w w))
+                    (split-string with " " t)
+                    ""))
+                 ;; use body in the source code block
+                 body))
+            body))
+
+    ;; expand literal variables in the body, if any
+    (when vars
+      (mapc
+       (lambda (var)
+         (let ((key (car var))
+               (val (cdr var)))
+           (setq body (string-replace (format "%s" key) (format "%s" val) body))))
+       vars))
+    body))
+
+(defun org-babel-execute:ada (body params)
+  "Execute or prove a block of Ada/SPARK code with org-babel.
+BODY contains the Ada/SPARK source code to evaluate. PARAMS is
+the list of source code block parameters.
+
+This function is called by `org-babel-execute-src-block'"
+  (let* ((processed-params (org-babel-process-params params))
+         (all-params
+          (ob-ada-spark-replace-params-from-template processed-params))
+         (full-body (org-babel-expand-body:ada body all-params))
+         (prove (cdr (assq :prove all-params))))
+    (if prove
+        (ob-ada-spark-prove full-body all-params)
+      (ob-ada-spark-execute full-body all-params))))
+
+(defun ob-ada-spark-execute (body params)
+  "Execute or prove a block of Ada/SPARK code with org-babel.
+BODY contains the Ada/SPARK source code to evaluate, already
+expanded when using templates. PARAMS is the list of source code
+block parameters, also expanded with the template parameters.
+
+This function is called by `org-babel-execute:ada'"
+  (let* ((args (cdr (assq :args params)))
+         (cflags (cdr (assq :cflags params)))
+         (unit (cdr (assq :unit params)))
+         (default-directory (org-babel-temp-directory))
+         (tmp-src-file (if unit
+                           (file-name-concat (org-babel-temp-directory)
+                                             (concat unit ".adb"))
+                         (org-babel-temp-file "ada-src-" ".adb")))
+         (tmp-bin-file (if unit
+                           (file-name-concat (org-babel-temp-directory) unit)
+                         (org-babel-temp-file "ada-bin-" org-babel-exeext))))
+
+    ;; write compilation unit
+    (with-temp-file tmp-src-file (insert body))
+
+    ;; clean previous evaluation of the same unit
+    (if (stringp unit)
+        (cl-mapcar
+         (lambda (ext)
+           (let ((file (file-name-concat default-directory
+                                         (concat unit ext))))
+             (if (file-exists-p file) (delete-file file))))
+         '("" ".ali" ".o")))
+
+    ;; compile
+    (setq compile-command
+          (format "%s %s -o %s %s %s"
+                  org-babel-ada-spark-compile-command
+                  (or org-babel-ada-spark-default-compile-flags "")
+                  tmp-bin-file
+                  (or cflags "")
+                  tmp-src-file))
+    (message "-- Ada compile-command: %s" compile-command)
+    (org-babel-eval compile-command "")
+
+    ;; execute
+    (let* ((exec-command (concat tmp-bin-file (if args (concat " " args) "")))
+           (results
+            (org-trim
+             (org-remove-indentation
+              (org-babel-eval exec-command "")))))
+      (org-babel-reassemble-table
+       (org-babel-result-cond (cdr (assq :result-params params))
+         (org-babel-read results)
+         (let ((tmp-file (org-babel-temp-file "ada-")))
+           (with-temp-file tmp-file (insert results))
+           (org-babel-import-elisp-from-file tmp-file)))
+       (org-babel-pick-name
+        (cdr (assq :colname-names params)) (cdr (assq :colnames params)))
+       (org-babel-pick-name
+        (cdr (assq :rowname-names params)) (cdr (assq :rownames params)))))))
+
+(defun ob-ada-spark-prove (body params)
+  "Prove a block of SPARK code with org-babel.
+BODY contains the SPARK source code to prove, already expanded
+when using templates. PARAMS is the list of source code block
+parameters, also expanded with the template parameters.
+
+This function is called by `org-babel-execute:ada'"
+  (let* ((cflags (cdr (assq :cflags params)))
+         (pflags (cdr (assq :pflags params)))
+         (unit (cdr (assq :unit params)))
+         (default-directory (org-babel-temp-directory))
+         (tmp-src-file (if unit (concat unit ".adb") "spark_src.adb"))
+         (tmp-gpr-file (if unit (concat unit ".gpr") "spark_prj.gpr"))
+         (tmp-project (file-name-sans-extension tmp-gpr-file))
+         (prove-command-args
+          (format "-P %s %s %s -u %s -cargs %s %s"
+                  tmp-gpr-file
+                  (or org-babel-ada-spark-default-prove-flags "")
+                  (or pflags "")
+                  tmp-src-file
+                  (or org-babel-ada-spark-default-compile-flags "")
+                  (or cflags ""))))
+
+    ;; write compilation unit
+    (with-temp-file tmp-src-file (insert body))
+
+    ;; create temporary project
+    (with-temp-file tmp-gpr-file
+      (insert (format "project %s is
+  for Source_Dirs use (\"%s\");
+  for Source_Files use (\"%s\");
+  for Main use (\"%s\");
+end %s;
+"
+                      tmp-project
+                      default-directory
+                      tmp-src-file
+                      tmp-src-file
+                      tmp-project)))
+
+    ;; remove gnatprove directory and clean previous evaluation of the
+    ;; same unit
+    (delete-directory
+     (file-name-concat org-babel-temporary-directory "gnatprove") t)
+    (org-babel-eval
+     (format "%s --clean %s"
+             org-babel-ada-spark-prove-command prove-command-args)
+     "")
+
+    ;; invoke gnatprove
+    (let* ((prove-command
+            (format "%s %s"
+                    org-babel-ada-spark-prove-command prove-command-args))
+           (results
+            (org-trim
+             (org-remove-indentation
+              (org-babel-eval prove-command "")))))
+      (message "-- SPARK prove-command: %s" prove-command)
+      (org-babel-reassemble-table
+       (org-babel-result-cond (cdr (assq :result-params params))
+         (org-babel-read results)
+         (let ((tmp-file (org-babel-temp-file "ada-")))
+           (with-temp-file tmp-file (insert results))
+           (org-babel-import-elisp-from-file tmp-file)))
+       (org-babel-pick-name
+        (cdr (assq :colname-names params)) (cdr (assq :colnames params)))
+       (org-babel-pick-name
+        (cdr (assq :rowname-names params)) (cdr (assq :rownames params)))))))
+
+(defun org-babel-prep-session:ada-spark ()
+  "This function does nothing.
+Ada and SPARK are compiled languages with no support for
+sessions."
+  (error "Ada & SPARK are compiled languages -- no support for sessions"))
+
+(defvar ada-skel-initial-string--backup "")
+
+(defun ob-ada-spark-pre-tangle-hook ()
+  "This function is called just before `org-babel-tangle'.
+When using tangle to export Ada/SPARK code to a file, this
+function is used to set the header of the file according to the
+value of the variable `org-babel-ada-spark-default-file-header'."
+  ;; ada-skel-initial-string is defined in ada-mode and is inserted
+  ;; automatically when Emacs sets ada-mode in an empty buffer; switching
+  ;; temporarily its value so the org-babel-ada-spark-default-file-header is
+  ;; inserted
+  (if (boundp 'ada-skel-initial-string)
+      (progn (setq ada-skel-initial-string--backup ada-skel-initial-string)
+             (setq ada-skel-initial-string (funcall org-babel-ada-spark-default-file-header)))))
+
+(defun ob-ada-spark-post-tangle-hook ()
+  "This function is called just after `org-babel-tangle'.
+Once the file has been generated, this function restores the
+value of the header inserted into Ada/SPARK files."
+  ;; if ada-skel-initial-string has not been inserted by ada-mode, then
+  ;; insert the default header
+  (if (boundp 'ada-skel-initial-string)
+      (setq ada-skel-initial-string ada-skel-initial-string--backup)
+    (save-excursion
+      (goto-char (point-min))
+      (insert (funcall org-babel-ada-spark-default-file-header)))))
+
+(add-hook 'org-babel-pre-tangle-hook #'ob-ada-spark-pre-tangle-hook)
+(add-hook 'org-babel-post-tangle-hook #'ob-ada-spark-post-tangle-hook)
+
+(provide 'ob-ada-spark)
+
+;;; ob-ada-spark.el ends here
diff --git a/testing/examples/ob-ada-spark-test.org b/testing/examples/ob-ada-spark-test.org
new file mode 100644
index 000000000..dec1e371c
--- /dev/null
+++ b/testing/examples/ob-ada-spark-test.org
@@ -0,0 +1,300 @@
+#+PROPERTY: results silent scalar
+#+title:A collection of examples for ob-ada-spark tests
+
+* Simple programs
+
+** Hello world
+:PROPERTIES:
+:ID: 778e63c2-2644-4a6f-8e7d-f956fa3d9241
+:END:
+
+#+name: Hello world
+#+begin_src ada :results silent
+   with Ada.Text_IO;
+   procedure Hello_World is
+   begin
+      Ada.Text_IO.Put_Line ("Hello world");
+   end Hello_World;
+#+end_src
+
+** Recursive Fibonacci
+:PROPERTIES:
+:ID: 6281cb40-26cc-423e-88c8-e8f26901ee4a
+:END:
+
+#+name: Recursive Fibonacci
+#+begin_src ada :unit fibonacci :results silent
+   with Ada.Text_IO;
+   procedure Fibonacci is
+      function fib (n : Natural) return Natural is
+        (if n <= 2 then 1 else fib (n-1) + fib (n-2));
+      Fib_15 : Natural;
+   begin
+      Fib_15 := fib (15);
+      Ada.Text_IO.Put_Line (Fib_15'Image);
+   end Fibonacci;
+#+end_src
+
+** Sequential Fibonacci
+:PROPERTIES:
+:ID: 41b4514b-0d46-4011-b5fa-7997aecf75a9
+:END:
+
+#+name Sequential Fibonacci
+#+begin_src ada :unit fibonacci :results silent
+   with Ada.Text_IO; use Ada.Text_IO;
+   procedure Fibonacci is
+      function fib (n : Natural) return Natural is
+      fn1, fn2 : Natural := 1;
+      begin
+         return result : Natural := 1 do
+            for i in reverse 3 .. n loop
+               result := fn1 + fn2;
+               fn2 := fn1;
+               fn1 := result;
+            end loop;
+         end return;
+      end fib;
+      Fib_15 : constant Natural := fib (15);
+   begin
+     Ada.Text_IO.Put_Line (Fib_15'Image);
+   end Fibonacci;
+#+end_src
+
+** UTF8 identifiers
+:PROPERTIES:
+:ID: 06e4dc5b-5566-486b-81af-cb7c547d46f1
+:END:
+
+#+name: UTF8 indetifiers
+#+begin_src ada :unit average :results silent
+   with Ada.Text_IO; use Ada.Text_IO;
+   procedure Average is
+      Σ_numbers : Natural := 0;
+      α, β, Δ_x : Natural := 1;
+      Average   : Float;
+   begin
+      loop
+         Σ_numbers := @ + α;
+         exit when α > 100;
+         α := @ + Δ_x;
+         β := @ + 1;
+         Δ_X := @ * 2;
+      end loop;
+      Average := Float (Σ_numbers) / Float (β);
+      Put_Line ("Average:" & Natural (Average)'Image);
+   end Average;
+#+end_src
+
+* Using templates
+
+** Main template
+:PROPERTIES:
+:ID: a2a64153-a7b6-4c32-84c5-a589f0caac93
+:END:
+
+#+name: Main template
+#+begin_src ada :template ada-main :results silent
+begin
+   Put_Line ("Hello world");
+#+end_src
+
+** Fibonacci
+:PROPERTIES:
+:ID: cbef4ee3-63e3-4295-8b26-e2470e30b1ff
+:END:
+
+#+name: Fibonacci
+#+begin_src ada :template ada-main :results silent
+   --  declaratiions
+   function fib (n : Natural) return Natural is
+      (if n <= 2 then 1 else fib (n-1) + fib (n-2));
+   Fib_15 : Natural;
+
+begin
+   Fib_15 := fib (15);
+   Put_Line (Fib_15'Image);
+#+end_src
+
+** Invalid template name
+:PROPERTIES:
+:ID: 3fb0ac1c-dfed-4d2f-9803-d1dea18eec45
+:END:
+
+#+name: Invalid template
+#+begin_src ada :template foo-bar :results silent
+begin
+   Put_Line ("Hello world");
+#+end_src
+
+* Literate programming
+
+** Hello noweb
+:PROPERTIES:
+:ID: 5386221e-da6f-411f-8dd5-3045e14b2e15
+:END:
+
+#+name: __Say_Hello_Noweb__
+#+begin_src ada
+   Put_Line ("Hello noweb");
+#+end_src
+
+#+header: :noweb yes
+#+name: Hello noweb
+#+begin_src ada :unit hello_world :results silent scalar
+   with Ada.Text_IO; use Ada.Text_IO;
+   procedure Hello_World is
+   begin
+      <<__Say_Hello_Noweb__>>
+   end Hello_World;
+#+end_src
+
+** Constant literals
+:PROPERTIES:
+:ID: 1bc1f537-e31f-4b8e-adb3-bdd474673e17
+:END:
+
+#+name: __Say_Hello__
+#+begin_src ada
+   Put ("Hello");
+#+end_src
+
+#+header: :noweb yes
+#+header: :var __TIMES__=3
+#+name: Constant literals
+#+begin_src ada :template ada-main :results silent scalar
+begin
+   for I in 1 .. __TIMES__ loop
+      Put (I'Image & " ");
+      <<__Say_Hello__>>
+   end loop;
+#+end_src
+
+#+header: :var __MESSAGE__="Hellow world"
+#+name: Constant literals - invalid literal name
+#+begin_src ada :template ada-main :results silent scalar
+   Put_Line ("Message: " &  __MSG__);
+#+end_src
+
+** Evaluated literals
+:PROPERTIES:
+:ID: 7cc220c1-a917-4af4-a497-7e247f1c15ae
+:END:
+
+#+header: :var __SUM__=(+ 1 1 3 5 8 13 34 55 89 144)
+#+name: Variable evaluation
+#+begin_src ada :template ada-main :results silent scalar
+begin
+   Put_Line ("SUM is __SUM__");
+#+end_src
+
+* User-Defined templates
+
+For the test, the template =ob-ada-spark-template:test= is defined in
+the file =test-ob-ada-spark.el=.
+
+** Test
+:PROPERTIES:
+:ID: 70feb9e8-19f1-402b-b1d0-4c8ccdf2cfe4
+:END:
+
+#+name: Test
+#+begin_src ada :template test
+   Write_Answer (42);
+#+end_src
+
+** Using and evaluated literals
+:PROPERTIES:
+:ID: 2a05b182-07bf-4ba5-9cca-128919cb837e
+:END:
+
+#+header: :var __Answer__=(* 21 2)
+#+name: Using evaluated literals
+#+begin_src ada :template test
+   Write_Answer (__Answer__);
+#+end_src
+
+** Using noweb and evaluated literals
+:PROPERTIES:
+:ID: 69e852b1-a278-4051-8719-917cfb59c582
+:END:
+
+#+name: __Write_Answer__
+#+begin_src ada :template test
+   Write_Answer (__Answer__);
+#+end_src
+
+#+header: :noweb yes
+#+header: :var __Answer__=(* 21 2)
+#+name: Using noweb and evaluated literals
+#+begin_src ada :template test
+   <<__Write_Answer__>>
+#+end_src
+
+* Proving SPARK code
+
+** Increment
+
+#+name: __Increment__
+#+begin_src ada
+   subtype Nat16 is Natural range 0 .. 2**16;
+   Number : Nat16 := Nat16'Last - 1;
+
+   procedure Increment (X : in out Nat16) with
+      Global  => null,
+      Depends => (X => X),
+      Pre     => (X < Nat16'Last),
+      Post    => (X = X'Old + 1)
+   is
+   begin
+      X := X + 1;
+   end Increment;
+
+begin
+   Increment (Number);
+   Put_Line ("Last Nat16 is" & Number'Image);
+#+end_src
+
+** Stone
+:PROPERTIES:
+:ID: fd628dbb-aacc-4931-aab5-5816f7c85b46
+:END:
+
+#+name: Stone
+#+header: :noweb yes
+#+begin_src ada :template spark-main :pflags --mode=stone :results scalar
+   <<__Increment__>>
+#+end_src
+
+** Bronze
+:PROPERTIES:
+:ID: 79b4ca15-8127-467d-b239-dd190cb45f2d
+:END:
+
+#+name: Bronze
+#+header: :noweb yes
+#+begin_src ada :template spark-main :pflags --mode=bronze :results scalar
+   <<__Increment__>>
+#+end_src
+
+** Silver
+:PROPERTIES:
+:ID: 4529e47f-835a-4410-883a-b3fab0026553
+:END:
+
+#+name: Silver
+#+header: :noweb yes
+#+begin_src ada :template spark-main :pflags --mode=silver :results scalar
+   <<__Increment__>>
+#+end_src
+
+** Gold
+:PROPERTIES:
+:ID: 371d0f89-4281-48b4-a70b-d0b51d515423
+:END:
+
+#+name: Gold
+#+header: :noweb yes
+#+begin_src ada :template spark-main :pflags --mode=gold :results scalar
+   <<__Increment__>>
+#+end_src
diff --git a/testing/lisp/test-ob-ada-spark.el b/testing/lisp/test-ob-ada-spark.el
new file mode 100644
index 000000000..21ab66026
--- /dev/null
+++ b/testing/lisp/test-ob-ada-spark.el
@@ -0,0 +1,240 @@
+;;; test-ob-ada-spark.el --- tests for ob-ada-spark.el  -*- lexical-binding: t; -*-
+
+;; Copyright (c) 2024 Free Software Foundation, Inc.
+;; Authors: Francesc Rocher
+;; Maintainer: Francesc Rocher <francesc.rocher@gmail.com>
+
+;; This file is part of GNU Emacs.
+
+;; This program is free software; you can redistribute it and/or modify
+;; it under the terms of the GNU General Public License as published by
+;; the Free Software Foundation, either version 3 of the License, or
+;; (at your option) any later version.
+
+;; This program is distributed in the hope that it will be useful,
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;; GNU General Public License for more details.
+
+;; You should have received a copy of the GNU General Public License
+;; along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+;;; Code:
+(require 'ob-core)
+(require 'ob-ada-spark)
+
+(org-test-for-executable "gnatmake")
+(org-test-for-executable "gnatprove")
+
+(unless (featurep 'ob-ada-spark)
+  (signal 'missing-test-dependency "Support for Ada and SPARK code blocks"))
+
+;; Simple programs
+
+(ert-deftest ob-ada-spark/simple/hello-world ()
+  "Simple program: Hello world"
+  (org-test-at-id
+   "778e63c2-2644-4a6f-8e7d-f956fa3d9241"
+   (org-babel-next-src-block)
+   (should (equal "Hello world" (org-babel-execute-src-block)))))
+
+(ert-deftest ob-ada-spark/simple/recursive-fibonacci ()
+  "Simple program: Recursive Fibonacci"
+  (org-test-at-id
+   "6281cb40-26cc-423e-88c8-e8f26901ee4a"
+   (org-babel-next-src-block)
+   (should (= 610 (org-babel-execute-src-block)))))
+
+(ert-deftest ob-ada-spark/simple/sequential-fibonacci ()
+  "Simple program: Sequential Fibonacci"
+  (org-test-at-id
+   "41b4514b-0d46-4011-b5fa-7997aecf75a9"
+   (org-babel-next-src-block)
+   (should (= 610 (org-babel-execute-src-block)))))
+
+(ert-deftest ob-ada-spark/simple/utf8-identifiers ()
+  "Simple program: UTF-8 indentifiers"
+  (org-test-at-id
+   "06e4dc5b-5566-486b-81af-cb7c547d46f1"
+   (org-babel-next-src-block)
+   (should (equal "Average: 32" (org-babel-execute-src-block)))))
+
+(ert-deftest ob-ada-spark/simple/utf8-identifiers-error ()
+  "Simple program: UTF-8 indentifiers"
+  (org-test-at-id
+   "06e4dc5b-5566-486b-81af-cb7c547d46f1"
+   (org-babel-next-src-block 2)
+   (when (should (buffer-live-p (get-buffer org-babel-error-buffer-name)))
+     (kill-buffer org-babel-error-buffer-name))
+   :type 'error))
+
+;; Using templates
+
+(ert-deftest ob-ada-spark/using-templates/main-template ()
+  "Using templates: Main template"
+  (org-test-at-id
+   "a2a64153-a7b6-4c32-84c5-a589f0caac93"
+   (org-babel-next-src-block)
+   (should (equal "Hello world" (org-babel-execute-src-block)))))
+
+(ert-deftest ob-ada-spark/using-templates/fibonacci ()
+  "Using templates: Fibonacci"
+  (org-test-at-id
+   "cbef4ee3-63e3-4295-8b26-e2470e30b1ff"
+   (org-babel-next-src-block)
+   (should (= 610 (org-babel-execute-src-block)))))
+
+(ert-deftest ob-ada-spark/using-templates/invlaid-template-name ()
+  "Using templates: Invalid template name"
+  (org-test-at-id
+   "3fb0ac1c-dfed-4d2f-9803-d1dea18eec45"
+   (org-babel-next-src-block)
+   (when (should (buffer-live-p (get-buffer org-babel-error-buffer-name)))
+     (kill-buffer org-babel-error-buffer-name))
+   :type 'error))
+
+;; Literate programming
+
+(ert-deftest ob-ada-spark/literate-programming/hello-noweb ()
+  "Literate programming: Hello noweb"
+  (org-test-at-id
+   "5386221e-da6f-411f-8dd5-3045e14b2e15"
+   (org-babel-next-src-block 2)
+   (should (equal "Hello noweb" (org-babel-execute-src-block)))))
+
+(ert-deftest ob-ada-spark/literate-programming/constant-literals ()
+  "Literate programming: Constant literals"
+  (org-test-at-id
+   "1bc1f537-e31f-4b8e-adb3-bdd474673e17"
+   (org-babel-next-src-block 2)
+   (should (equal "1 Hello 2 Hello 3 Hello"
+                  (org-babel-execute-src-block)))))
+
+(ert-deftest ob-ada-spark/literate-programming/constant-literals-invalid-literal-name ()
+  "Literate programming: Constant literals - Invalid literal name"
+  (org-test-at-id
+   "1bc1f537-e31f-4b8e-adb3-bdd474673e17"
+   (org-babel-next-src-block 3)
+   (when (should (buffer-live-p (get-buffer org-babel-error-buffer-name)))
+     (kill-buffer org-babel-error-buffer-name))
+   :type 'error))
+
+(ert-deftest ob-ada-spark/using-templates/evaluated-literals ()
+  "Using templates: Evaluated literals"
+  (org-test-at-id
+   "7cc220c1-a917-4af4-a497-7e247f1c15ae"
+   (org-babel-next-src-block)
+   (should (equal "SUM is 353" (org-babel-execute-src-block)))))
+
+;; User-defined templates
+
+(setq ob-ada-spark-template:test
+      '((:params . ((:unit . "main") (:results silent)))
+        (:body . "
+with Ada.Text_IO; use Ada.Text_IO;
+%s
+procedure Main is
+   procedure Write_Answer (N : Natural) is
+   begin
+      Put_Line (\"Answer:\" & N'Image);
+   end Write_Answer;
+begin
+   %s
+end Main;
+")))
+
+(ert-deftest ob-ada-spark/user-defined-template/test ()
+  "Users-defined templates: Test"
+  (org-test-at-id
+   "70feb9e8-19f1-402b-b1d0-4c8ccdf2cfe4"
+   (org-babel-next-src-block)
+   (should (equal "Answer: 42" (org-babel-execute-src-block)))))
+
+(ert-deftest ob-ada-spark/user-defined-template/using-evaluated-literals ()
+  "Users-defined templates: Using evaluated literals"
+  (org-test-at-id
+   "2a05b182-07bf-4ba5-9cca-128919cb837e"
+   (org-babel-next-src-block)
+   (should (equal "Answer: 42" (org-babel-execute-src-block)))))
+
+(ert-deftest ob-ada-spark/user-defined-template/using-noweb-and-evaluated-literals ()
+  "Users-defined templates: Using noweb and evaluated literals"
+  (org-test-at-id
+   "69e852b1-a278-4051-8719-917cfb59c582"
+   (org-babel-next-src-block 2)
+   (should (equal "Answer: 42" (org-babel-execute-src-block)))))
+
+;; Proving SPARK Code
+
+(ert-deftest ob-ada-spark/proving-spark-code/stone ()
+  "Proving SPARK code: Stone"
+  (org-test-at-id
+      "fd628dbb-aacc-4931-aab5-5816f7c85b46"
+   (org-babel-next-src-block)
+   (org-babel-execute-src-block)
+   (should (search-forward "#+begin_example" nil t))
+   (forward-line 1)
+   (let ((report-begin (point-at-bol))
+         (report-end 0))
+     (should (search-forward "#+end_example" nil t))
+     (forward-line -1)
+     (setq report-end (point-at-eol))
+     (should
+      (string-match
+       "Phase 1 of 2: generation of Global contracts ...
+\\(.\\|\n\\)+
+Phase 2 of 2: full checking of SPARK legality rules ..."
+       (buffer-substring-no-properties report-begin report-end))))))
+
+(ert-deftest ob-ada-spark/proving-spark-code/bronze ()
+  "Proving SPARK code: Bronze"
+  (org-test-at-id
+      "79b4ca15-8127-467d-b239-dd190cb45f2d"
+    (org-babel-next-src-block)
+    (org-babel-execute-src-block)
+    (should (search-forward "#+begin_example" nil t))
+    (forward-line 1)
+    (let ((report-begin (point-at-bol))
+          (report-end 0))
+      (should (search-forward "#+end_example" nil t))
+      (forward-line -1)
+      (setq report-end (point-at-eol))
+      (should
+       (string-match
+        "Phase 1 of 2: generation of Global contracts ...
+\\(.\\|\n\\)+
+Phase 2 of 2: analysis of data and information flow ...
+\\(.\\|\n\\)+
+main.adb:8:07: info: data dependencies proved
+main.adb:9:07: info: flow dependencies proved"
+        (buffer-substring-no-properties report-begin report-end))))))
+
+(ert-deftest ob-ada-spark/proving-spark-code/silver ()
+  "Proving SPARK code: Silver"
+  (org-test-at-id
+      "4529e47f-835a-4410-883a-b3fab0026553"
+    (org-babel-next-src-block)
+    (org-babel-execute-src-block)
+    (should (search-forward "#+begin_example" nil t))
+    (forward-line 1)
+    (let ((report-begin (point-at-bol))
+          (report-end 0))
+      (should (search-forward "#+end_example" nil t))
+      (forward-line -1)
+      (setq report-end (point-at-eol))
+      (should
+       (string-match
+        "Phase 1 of 2: generation of Global contracts ...
+\\(.\\|\n\\)+
+Phase 2 of 2: flow analysis and proof ...
+\\(.\\|\n\\)+
+main.adb:8:07: info: data dependencies proved
+main.adb:9:07: info: flow dependencies proved
+main.adb:11:18: info: postcondition proved
+main.adb:14:14: info: range check proved
+main.adb:18:04: info: precondition proved
+main.adb:19:30: info: range check proved"
+        (buffer-substring-no-properties report-begin report-end))))))
+
+(provide 'test-ob-ada-spark)
+;;; test-ob-ada-spark.el ends here
-- 
2.43.0