Minimal Ada kernel for Jupyter

Introduction

This Package contains a Jupyter kernel for the Ada language. The Jupyter C kernel was used as a starting point for this implementation.

License & Copyright

This Package is available "as is" under MIT License. The copyright of the Jupyter C kernel --- used as a starting point for this implementation --- is held by Brendan Rius. Unless stated otherwise, the copyright of the Ada kernel for Jupyter is held by Gustavo A. Hoffmann.

Supported Platforms

This Package has been tested on the following compilers / platforms:

• Linux / Python 3.6
• Windows / Python 3.6

Features

• Support for Ada language in Jupyter notebooks
• Support for running compiler and linker (GNAT) in the background
• Support for specifying multiple source-code files in the same notebook

Known Issues and Limitations

Platforms

• This Package has not been tested on the Mac platform.

Features

• Syntax highlighting requires manual installation.

Documentation

• Extensive documentation and tutorials are missing.

Installation

Details about the installation can be found on this document.

Usage

Please refer to the Jupyter documentation for details on how to create and use notebooks.

Entering and running Ada code

In order to use the Ada kernel, the first step is to select "Ada" from the list of kernels supported by the Jupyter installation. As soon as the kernel has started, you may enter Ada code by specifying the filename in the comments:

--% src_file: main.adb

with Ada.Text_IO;

procedure Main is
begin
    Ada.Text_IO.Put_Line("Hello World");
end Main;

The filename is required for creating the source-code file for the GNAT compiler. Click on 'Run' on the toolbar to compile the code.

In order to build and run the binary based on the procedure Main, you can replace src_file by run_file:

--% run_file: main.adb

with Ada.Text_IO;

procedure Main is
begin
    Ada.Text_IO.Put_Line("Hello World");
end Main;

Alternatively, you may build a file that has been created in another cell by using the build mode:

--% mode: build
--% src_file: main.adb

In the next cell, you can run the file by using run:

--% run: main

Again, if you want to build and run the file in the same cell, you may simply replace src_file by run_file:

--% mode: build
--% run_file: main.adb

Specifiying build options

It is possible to pass compilation options to the compiler using cflags:

--% src_file: main.adb
--% cflags: -g

with Ada.Text_IO;

procedure Main is
begin
    Ada.Text_IO.Put_Line("Hello World");
end Main;

Also, it is possible to specify build options using make_flags:

--% src_file: main.adb
--% make_flags: -a

with Ada.Text_IO;

procedure Main is
begin
    Ada.Text_IO.Put_Line("Hello World");
end Main;

Using GPRbuild project files

In addition to the simple compilation / build described in the previous section, you may also use project files:

--% prj_file: default.gpr

project Default is
    for Source_Dirs use (".");
    for Object_Dir use ".";
    for Main use ("main.adb");
end Default;

Running the cell will automatically build the project. It is also possible to build the project in a separate cell using the build mode:

--% mode: build
--% prj_file: default.gpr

Also, in case multiple main files are used, it is possible to specify which file contains the main application by using src_file:

--% mode: build
--% prj_file: default.gpr
--% src_file: main.adb

If we replace src_file by run_file, the application will run automatically after the build process:

--% mode: build
--% prj_file: default.gpr
--% run_file: main.adb

Proving SPARK code

It is possible to prove SPARK code by calling GNATprove (when available). This is achieved by using the prove mode:

--% mode: prove
--% prj_file: default.gpr

It is possible to prove just a specific file using src_file:

--% mode: prove
--% prj_file: default.gpr
--% src_file: main.adb

In addition, GNATprove options may be specified by using prove_flags:

--% mode: prove
--% prj_file: default.gpr
--% prove_flags: --report=all --output-header --verbose

Output formats

By default, the standard output of the binary will be displayed as raw (plain) text. However, this mode can be explicitly specified:

--% run_file: main.adb
--% output: raw

with Ada.Text_IO;

procedure Main is
begin
    Ada.Text_IO.Put_Line("Hello World");
end Main;

The standard output can also be displayed in HTML format:

--% run_file: main.adb
--% output: text/html

with Ada.Text_IO;

procedure Main is
begin
    Ada.Text_IO.Put_Line("<b>Hello World</b>");
end Main;

The standard output can also be displayed in Markdown format:

--% run_file: main.adb
--% output: text/markdown

with Ada.Text_IO;

procedure Main is
begin
    Ada.Text_IO.Put_Line("# Hello World");
end Main;

Finally, the format to be used can also be specified directly in the Ada application. In this case, the output must use the JSON representation required by display_data, which is used by IPython. Details about this can be found in the IPython documentation.

Interfacing with C/C++

In addition to Ada code, it is possible to interface with C code. For example, we may create a cell containing C code by using src_file:

//% src_file: test.c

#include <stdio.h>

void test()
{
    int a = 0;
    printf("Hi from C\n");
}

In the next cell, we may write an Ada procedure that makes use of the test function from the C code:

--% src_file: main.adb

with Ada.Text_IO;

procedure Main is
   procedure test with
     Import,
     Convention => C;
begin
   test;
end Main;

In order to build this code, we need to make use of a project file that explicitly mentions C in the list of supported languages:

--% prj_file: default.gpr

project Default is
    for Source_Dirs use (".");
    for Object_Dir use ".";
    for Languages use ("ada", "c");
    for Main use ("main.adb");
end Default;

Example of notebook

This Package contains an example of a notebook:

The HTML output notebook contains examples of HTML and Markdown output. It also contains an example that makes use of the internal JSON representation.