Re: Testing issues for Ada/SPARK support in Babel

[Ihor Radchenko]

Ihor Radchenko  writes:

>> If you don't mind, I attach here the patch in its current state for
>> reviewing purposes.
>
> Sure. See my comments inline.
> ...

It has been two months since the last message in this thread.
Francesc, did you have a chance to look into my comments?

-- 
Ihor Radchenko // yantar92,
Org mode contributor,
Learn more about Org mode at .
Support Org development at ,
or support my work at 

Re: Testing issues for Ada/SPARK support in Babel

[Ihor Radchenko]

Francesc Rocher  writes:

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

Sure. See my comments inline.

> +;; Author: Francesc Rocher
> +;; Maintainer: Francesc Rocher

If you can, please provide a contact email here.

> +
> +(require 'ob)
> +(require 'time-stamp)
> +
> +(org-assert-version)

Need (require 'org-macs) - it is where `org-assert-version' is defined.

> +(defvar org-babel-tangle-lang-exts)
> +(add-to-list 'org-babel-tangle-lang-exts '("ada" . "adb"))

Why not (require 'ob-tangle)?
Or, better (eval-after-load 'ob-tangle ...)

> +(defvar org-babel-temporary-directory)

You don't need it after (require 'ob) - org-babel-temporary-directory is
defined in ob-core, loaded by ob, and is thus available.

> +(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))

What does (with . nil) is supposed to mean?
AFAIK, this does not follow the format we describe in
`org-babel-common-header-args-w-values'.

> +(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.

By convention, Elisp docstrings use double space to separate sentences.
Also, ' should be used with care as they may be interpreted
specially. You may have to protect them with \=' escape or use some
other formatting. Try M-x checkdoc and check out "D.6 Tips for
Documentation Strings" section of Elisp manual.

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

I think `...' is used incorrectly here - it is not a Elisp symbol.

> +  :safe #'stringp)

I very much doubt that setting this variable in buffer-locals is safe -
a file downloaded from internet may set this to something like
"rm -f /home;" and unsuspecting users may evaluate the code...

> +(defcustom org-babel-ada-spark-prove-command "gnatprove"
> 
> +  :safe #'stringp)

Same here.

> +(defcustom org-babel-ada-spark-default-compile-flags
> ...
> +  :safe #'stringp)

And here.

> +(defcustom org-babel-ada-spark-default-prove-flags
> ...
> +  :safe #'stringp)

And here.

> +(defcustom org-babel-ada-spark-default-file-header
> +  (lambda ()

Why not making the value a named function?

> +(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."

It is important to note that PARAMS is modified by side effect.

> +  (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)

Any reason to display a message here? It is not a big deal when running
code interactively, but it may become annoying for users when code
blocks are evaluated in batches. For example during export.

> +  (mapc (lambda (p)
> +  (assq-delete-all (car p) params))
> +(cdr (assq :params template)))
> +  (append params (cdr (assq :params template
> +  params)))

Why not simply (append params ...)? When a plist has (:foo bar :foo
baz), the first value is used.

Also, while your approach works for your current value of
`org-babel-header-args:ada' that does not have any 

Re: Testing issues for Ada/SPARK support in Babel

[Francesc Rocher]

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

> Ihor Radchenko  writes:
>
> > Francesc Rocher  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>
>
From 806da098552f05bd4c3af82ba54bdae8c1ad54f1 Mon Sep 17 00:00:00 2001
From: Francesc Rocher 
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 0..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 pa

Re: Testing issues for Ada/SPARK support in Babel

[Ihor Radchenko]

Ihor Radchenko  writes:

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

[Ihor Radchenko]

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

Testing issues for Ada/SPARK support in Babel

[Francesc Rocher]

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

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

Re: Ada/SPARK support in Babel

[Francesc Rocher]

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

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

[Ihor Radchenko]

Francesc Rocher  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 .
Support Org development at ,
or support my work at 

Re: Ada/SPARK support in Babel

[Bastien Guerry]

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

[Ihor Radchenko]

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

Francesc Rocher  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@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>

Ada/SPARK support in Babel

[Francesc Rocher]

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