Ada/SPARK support in Babel

Ada/SPARK support in Babel

[Francesc Rocher]

[-- Attachment #1: Type: text/plain, Size: 945 bytes --]

Hi all,

I've started developing Babel support for Ada and SPARK languages.
I would like to include them in the main org-mode repository, as an
additional ("officially") supported language by org-mode.

Temporary development can be found at
https://github.com/rocher/ob-ada-spark/

For a new language to be included in the main org-mode repository, it
is required that the language:

  1. is supported by Emacs
  2. has a large user-base

IMMO both requirements are satisfied:

  1. ada-mode supports Ada (and, partially, SPARK)
  2. Ada appears in position 32 in the TIOBE rank of programming
     languages popularity (https://www.tiobe.com/tiobe-index/), above
     other languages supported by Babel like Julia, Clojure, Haskell,
     Scheme, awk, Forth, Ocaml or sed. (SPARK appears in the next 100)

Do you think that Ada/SPARK support should be included in the main
org-mode repository? Or in the org-contrib one?

BR,
-- Francesc Rocher

[-- Attachment #2: Type: text/html, Size: 1350 bytes --]

Re: Ada/SPARK support in Babel

[Ihor Radchenko]

[ I am going through some old threads without reply. ]

Francesc Rocher <francesc.rocher@gmail.com> writes:

> I've started developing Babel support for Ada and SPARK languages.
> I would like to include them in the main org-mode repository, as an
> additional ("officially") supported language by org-mode.
> ...
> For a new language to be included in the main org-mode repository, it 
> is required that the language:
>
>   1. is supported by Emacs
>   2. has a large user-base

> IMMO both requirements are satisfied:
>
>   1. ada-mode supports Ada (and, partially, SPARK)
>   2. Ada appears in position 32 in the TIOBE rank of programming
>      languages popularity (https://www.tiobe.com/tiobe-index/), above
>      other languages supported by Babel like Julia, Clojure, Haskell,
>      Scheme, awk, Forth, Ocaml or sed. (SPARK appears in the next 100)

From Bastien
https://list.orgmode.org/orgmode/87bl9rq29m.fsf@gnu.org/

    I suggest a criterium for keeping ob*.el files in Org could be that
    the extension is known by Emacs _or_ that the supported language is
    well-established.

Ada appears to fit in.

> Do you think that Ada/SPARK support should be included in the main
> org-mode repository? Or in the org-contrib one?

org-mode or ELPA. org-contrib is deprecated now.

I am, however, concerned that https://github.com/rocher/ob-ada-spark/
did not show much interest (just a single issue). Also, no replies on
this list from users.

It appears that we have not many Org mode users who need Ada support.

But I also know that Ada is certainly well-established and active -
https://www.adaic.org/events/.

My initial assessment is that we might include babel support for Ada if
it is accompanied by good set of tests, so that we do not need to worry
too much about things breaking even if there is no ob-ada maintainer.

... and let's see if the original author is still interested to continue
with his request.

-- 
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>

Re: Ada/SPARK support in Babel

[Bastien Guerry]

Ihor Radchenko <yantar92@posteo.net> writes:

> My initial assessment is that we might include babel support for Ada if
> it is accompanied by good set of tests, so that we do not need to worry
> too much about things breaking even if there is no ob-ada maintainer.
>
> ... and let's see if the original author is still interested to continue
> with his request.

FWIW +1

-- 
 Bastien Guerry

Re: Ada/SPARK support in Babel

[Francesc Rocher]

[-- Attachment #1: Type: text/plain, Size: 1063 bytes --]

Hi all,

At the moment, ob-ada-spark is available at MELPA,
https://melpa.org/#/ob-ada-spark.
For what I've seen, it seems enough for the Ada community: 187 downloads
since it was published
back in 2022 (possibly that's not relevant; possibly if it was available in
org-mode some people would
be interested in Ada).

If you still want to include it into the mainstream org-mode repository,
then I'll be more than happy
to contribute. If so, let me know what are the next steps and what kind of
test do you expect.

BR,
-- Francesc Rocher


On Sat, Feb 24, 2024 at 2:58 PM Bastien Guerry <bzg@gnu.org> wrote:

> Ihor Radchenko <yantar92@posteo.net> writes:
>
> > My initial assessment is that we might include babel support for Ada if
> > it is accompanied by good set of tests, so that we do not need to worry
> > too much about things breaking even if there is no ob-ada maintainer.
> >
> > ... and let's see if the original author is still interested to continue
> > with his request.
>
> FWIW +1
>
> --
>  Bastien Guerry
>

[-- Attachment #2: Type: text/html, Size: 1769 bytes --]

Re: Ada/SPARK support in Babel

[Ihor Radchenko]

Francesc Rocher <francesc.rocher@gmail.com> writes:

> If you still want to include it into the mainstream org-mode repository,
> then I'll be more than happy
> to contribute. If so, let me know what are the next steps and what kind of
> test do you expect.

Yes, we are interested to have Ada support in Org mode repository.

Here is what you need to do:

1. Check our contributor instructions at
   https://orgmode.org/worg/org-contribute.html#first-patch
   In particular, pay attention to the ChangeLog entry format.
   You also need FSF copyright assignment.
   Don't worry to make mistakes - we will guide you through once you
   submit patches.

2. https://github.com/rocher/ob-ada-spark/blob/main/ob-ada-spark.el
   should go to lisp/ directory of Org repository.
   Make sure to update the file header, updating the licence and stating
   that it is now a part of Emacs.

3. You need to get rid of any external library dependencies (f.el)

4. https://github.com/rocher/ob-ada-spark/blob/main/ob-doc-Ada-SPARK.org
   should go to
   https://orgmode.org/worg/org-contrib/babel/languages/index.html
   You will need to make a patch against https://git.sr.ht/~bzg/worg
   Also, make sure to follow
   https://orgmode.org/worg/org-contrib/babel/languages/ob-doc-template.org

5. You need to add tests to testing/lisp in Org repository.
   You may use
   https://git.savannah.gnu.org/cgit/emacs/org-mode.git/tree/testing/lisp/test-ob-java.el
   as a reference.

6. It will be best if you continue maintaining ob-ada within Org mode
   repository. If you are willing to, we will also give you write access
   to the Org mode repository on savannah. We will provide instructions
   later, when we reach this stage.
   Note that we use Org mailing list to track bugs and discuss the
   development. You do not have to be subscribed, we can forward
   relevant email threads to your email inbox.

If you have any questions, feel free to ask us.

-- 
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>

Testing issues for Ada/SPARK support in Babel

[Francesc Rocher]

[-- Attachment #1: Type: text/plain, Size: 4144 bytes --]

Hi all,

I'm starting from scratch the set of tests for Ada/SPARK support in Babel.
I've prepared a file with the first example:

---8<--- testing/examples/ob-ada-spark-test-org ---8<---
* Simple tests
:PROPERTIES:
:ID:       778e63c2-2644-4a6f-8e7d-f956fa3d9241
:END:
#+name: hello-world
#+begin_src ada :unit hello_world :results silent
   with Ada.Text_IO;
   procedure Hello_World is
   begin
      Ada.Text_IO.Put_Line ("Hello world");
   end Hello_World;
#+end_src
---8<------8<------8<------8<------8<------8<---

Then in the file testing/test-ob-ada-spark.el I've defined the following
test:

(ert-deftest ob-ada-spark/hello-world ()
  "Test simple Hello world."
  (org-test-at-id "778e63c2-2644-4a6f-8e7d-f956fa3d9241"
    (org-babel-next-src-block)
    (should (equal "Hello world\n" (org-babel-execute-src-block)))))

When I execute the test form within Emacs with:

(add-to-list ' load-path (concat (file-name-directory (buffer-file-name))))
(require 'org-test)
(ert 'ob-ada-spark/hello-world)

it works fine, but when I run the test from the command line with

$ make BTEST_RE='ob-ada-spark.*' test-dirty

it fails because (org-babel-execute-src-block) returns nil:

Test ob-ada-spark/hello-world condition:
    (wrong-type-argument stringp nil)
   FAILED  1/1  ob-ada-spark/hello-world (0.002933 sec) at
../lisp/test-ob-ada-spark.el:40

Everything is in place, "make compile" issues no warning and required
programs are in PATH. I've tested other languages, e.g.

$ make BTEST_RE='ob-fortran.*' test-dirty
$ make BTEST_RE='ob-java/.*' test-dirty

and everything works fine .

Any idea?? How can I debug test execution from the command line?

BR,
-- Francesc Rocher


On Sun, Feb 25, 2024 at 11:36 AM Ihor Radchenko <yantar92@posteo.net> wrote:

> Francesc Rocher <francesc.rocher@gmail.com> writes:
>
> > If you still want to include it into the mainstream org-mode repository,
> > then I'll be more than happy
> > to contribute. If so, let me know what are the next steps and what kind
> of
> > test do you expect.
>
> Yes, we are interested to have Ada support in Org mode repository.
>
> Here is what you need to do:
>
> 1. Check our contributor instructions at
>    https://orgmode.org/worg/org-contribute.html#first-patch
>    In particular, pay attention to the ChangeLog entry format.
>    You also need FSF copyright assignment.
>    Don't worry to make mistakes - we will guide you through once you
>    submit patches.
>
> 2. https://github.com/rocher/ob-ada-spark/blob/main/ob-ada-spark.el
>    should go to lisp/ directory of Org repository.
>    Make sure to update the file header, updating the licence and stating
>    that it is now a part of Emacs.
>
> 3. You need to get rid of any external library dependencies (f.el)
>
> 4. https://github.com/rocher/ob-ada-spark/blob/main/ob-doc-Ada-SPARK.org
>    should go to
>    https://orgmode.org/worg/org-contrib/babel/languages/index.html
>    You will need to make a patch against https://git.sr.ht/~bzg/worg
>    Also, make sure to follow
>
> https://orgmode.org/worg/org-contrib/babel/languages/ob-doc-template.org
>
> 5. You need to add tests to testing/lisp in Org repository.
>    You may use
>
> https://git.savannah.gnu.org/cgit/emacs/org-mode.git/tree/testing/lisp/test-ob-java.el
>    as a reference.
>
> 6. It will be best if you continue maintaining ob-ada within Org mode
>    repository. If you are willing to, we will also give you write access
>    to the Org mode repository on savannah. We will provide instructions
>    later, when we reach this stage.
>    Note that we use Org mailing list to track bugs and discuss the
>    development. You do not have to be subscribed, we can forward
>    relevant email threads to your email inbox.
>
> If you have any questions, feel free to ask us.
>
> --
> 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 #2: Type: text/html, Size: 6426 bytes --]

Re: Testing issues for Ada/SPARK support in Babel

[Ihor Radchenko]

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:
>
> ---8<--- testing/examples/ob-ada-spark-test-org ---8<---
> ...
> Then in the file testing/test-ob-ada-spark.el I've defined the following
> test:
>
> (ert-deftest ob-ada-spark/hello-world ()
>   "Test simple Hello world."
>   (org-test-at-id "778e63c2-2644-4a6f-8e7d-f956fa3d9241"

I recommend using `org-test-with-temp-text' when the tested Org snippet
is short. Otherwise, it is harder to read the test.

> $ make BTEST_RE='ob-ada-spark.*' test-dirty
>
> it fails because (org-babel-execute-src-block) returns nil:
>
> Test ob-ada-spark/hello-world condition:
>     (wrong-type-argument stringp nil)

Is the file name exactly "ob-ada-spark-test-org"? Without .org extension?
If yes, IDs inside that file may not be indexed properly.

-- 
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>

Re: Testing issues for Ada/SPARK support in Babel

[Ihor Radchenko]

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>

Re: Testing issues for Ada/SPARK support in Babel

[Francesc Rocher]

[-- 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