Nubo: a repository for Dedukti developments

This repository centralises metadata concerning Dedukti developments. These metadata ought to be structured enough so that developments may be processed by programs. We call expression any string understood by Dedukti: it can be the declaration of a type Nat in Dedukti, a set of declarations and definitions, a collection of definitions, declarations and theorems. We call module a Dedukti file containing proofs. The file nat.dk containing

Nat: Type.
z: Nat
s: Nat -> Nat

is a module containing expressions. We call library a set of modules which are related by topic or dependency.

Blueprint

We call blueprint a file that holds metadata about a library.

A blueprint is a BSD flavoured Makefile defining the following variables:

• LIB_NAME: name of the library. This is not the library name

• LIB_VERSION: version of the library.

• LIB_FLAVOUR: denotes some options used in the generation of the library. This field is optional.

• LIB_DEPENDS: a list of library paths on which the library depends.

• LIB_ORIGIN: URL to the original files of the library, as distributed by the authors.

• ENCODING: a list of library path that specifies the encoding of the logic the library is expressed into. It must be a (possibly empty) subset of LIB_DEPENDS. This field serves interoperability purposes.

• SYNTAX: concrete syntax the library is written in. See the syntax specification.

• TOOLING: a list of tools used to translate proofs. A tool is specified by a string <name>:<version> where <name> is the name of the tool, and <version> is its version used. The format of the version may depend on the source of the tool. If the tool is stored on git, a commit hash, or tag, or branch name may be provided. Tools are referenced in TOOLS.

• MAIN: a list of modules standing for entry points to the library. The entry points are explicitly checked whereas other modules are usually checked as dependencies.

• FLAGS: flags that may be passed to the checker.

Note: These variables not only serve informative purposes, they can be used to fulfill miscellaneous tasks using targets defined in infrastructure/mk/nubo.library.mk. More information on these targets are given in How to use this repository.

Library name

Each library has a name which consists of 3 parts

stem-version[-flavour]

The stem part identifies the library and refers to the variable LIB_NAME of the blueprint. It may contain dashes.

The version part starts at the first digit that follows a - and goes up to the following -. It refers to the variable LIB_VERSION of the blueprint.

The remaining flavour part refers to the variable LIB_FLAVOUR of the blueprint. It is optional.

The version part must start with a digit, whereas the flavour must not start with a digit.

All packages must have a version number. Normally, the version number directly matches the original library version number, or release date. In case there are substantial changes in the translated library, a patch level marker should be appended (e.g. p0, p1, &c.).

Version comparison is done using a lexicographic alphabetic order.

This section is based on the manual page packages-specs(7) of OpenBSD

Library path

Each location in the library tree is uniquely identified by a libpath.

Every libpath conforms to the pattern cat/stem/[flavour,]version where stem, version and flavour are defined in the name specification. The cat (for category) part refers to the first directory at the root of the library tree. The flavour, part is optional.

Such a libpath locates uniquely a library in the library tree.

For instance, libraries/arith_fermat/sttfa,1.0 is the location of the library arith_fermat version 1.0 in its sttfa flavour, its blueprint is libraries/arith_fermat/sttfa,1.0/Makefile.

As an example, the overall structure of the library tree may look like this,

nubo/
+- encodings/
|  +- libA/
|  |  +- 1.0/
|  |  |  +- Makefile
|  |  +- flavA,1.0/
|  |  |  +- Makefile
|  |  +- flavA,1.1/
|  |  |  +- Makefile
|  |  +- flavB,1.0/
|  |     +- Makefile
|  +- libB/
|     +- ...
+- arithmetic/
   +- ...

Note: in the previous example, each Makefile is a blueprint.

Syntax specifier

Expressions are written in a concrete syntax that can be identified by a syntax specifier which conforms to the pattern

stem [options]

The stem part is a string without spaces that identifies a grammar.

The options part is a (possibly empty) space-separated list of strings preceded by a - or a +. An option identifies one or more syntax extensions that are added to the grammar stem if the option is preceded by + or removed from the grammar if the option is preceded by -.

The possible stems and options are referenced in the file SYNTAXES. The SYNTAXES file follows the record jar format where records contain the following fields:

• type: either stem or option,
• key: the string that may be used in the syntax specifier,
• description: a short description of the grammar or the syntax extension introduced by the record.

Tooling

The file TOOLS gathers information on the tools that may be used to translate proofs or to operate on translated proofs. It follows the record jar format.

A record must at least contain the fields name and homepage. Any other field is optional.

• name: a unique name that identifies the tool.
• homepage: URL of the homepage of the tool from where it can be downloaded.

Packaged libraries

Libraries are packaged into gzipped tarballs with the extension .tgz for distribution. Each library identified by a library name specification: libname is packaged as libname.tgz. Such an archive must contain

• the modules that make up the library (.dk files),

• a (POSIX) Makefile dependency list named .depend listing the dependencies between the modules.

Modules are expected to be in the same directory as the dependency file.

For instance, the archive of arith_fermat-1.0-sttfa is available at ${PKG_PATH}/arith_fermat-1.0-sttfa.tgz (see the documentation of makefiles for a description of ${PKG_PATH}).

How to use this repository

The library tree can be used to install, check or package libraries using make.

Caution: BSD make must be used, Linux users must invoke bmake rather than make.

Caution: the variable NUBOROOT must contain the path of the local clone of this repository for most of these commands to work.

The available targets are

• download: download and extracts the source files of the library,
• check: check the library. By defaults it uses Dedukti to check the library. It can be invoked as make check=CHECKER where CHECKER is the name of a known checker. Currently available are dedukti and kontroli.
• package: create a library package from the downloaded files.
• lint: performs sanity checks on a package.
• makesum: computes the checksum of the library package and replace it in the blueprint.
• list: list available libraries.
• clean: clean content. By default, clean the blueprint directory. It can be invoked as make clean='[work build]'.
  • work: clean the blueprint directory (remove archives and uncompressed library).
  • build: clean typechecked files.

These commands must be called in the same directory as the blueprint. For example, to download arith_fermat-1.0-sttfa,

cd libraries/arith_fermat/sttfa,1.0
make download

The following parameters can be set to alter the user interface:

• ECHO_MSG: handle progress messages with the command given as parameter.
• PROGRESS_METER: set to No to disable the library download progress bar.

To check the same library without output (where true refers to the shell function that returns 0, and does not mean that messages are activated),

cd libraries/arith_fermat/sttfa,1.0
make ECHO_MSG=true PROGRESS_METER=No check

Contributing to Nubo

If you have translated a library in Dedukti (and it typechecks), or you designed an encoding; you may submit it to Nubo.

Contribution checklist:

1. Fetch a copy of the Nubo proof tree. Let root be the path to the proof tree.
2. Pick a category for your ports. Either an already existing one at root/<cat> or create a new one. Let cat be the chosen category.
3. Create the directory structure: let name be the name of your library, ver its version. Create the directory tree root/cat/name/ver/. If there are different version of the same library, flavours may be specified. In that case, the directory tree is root/cat/name/ver,flavour/.
4. Copy the template blueprint from root/infrastructure/templates/Makefile to the created directory, and fill all variables noted # REQUIRED.
5. Copy your modules into a directory named name-ver or name-ver-flav alongside the new blueprint. There must not be any subdirectory in the directory containing the modules.
6. In the former directory, create a .depend file such that for each module m that depends on modules m1, m2, ... there is a target m.dko which depends on m.dk and mi.dko.
7. Make the library package with make package.
8. Add the checksum of the package with make makesum. The original blueprint is saved as Makefile.bak.
9. Run basic verifications with make lint.
10. Assert it typechecks running make check.
11. Incorporate your new library: email your blueprint to [email protected] with its category and the package or an URL where it can be retrieved. If you cloned Nubo using git, add a one-line entry for the new library in its parent directory's makefile, e.g. for libraries/arith_fermat/, add it to libraries/Makefile, commit and email a patch (see git-format-patch(1)) or create a pull request.

Steps 2 to 4 can be automated using make new at root. Step 6 can be automated using dkdep.

Notes

It is the user's responsability to install softwares and tools in their appropriate version.

Upcoming

• Add a maintainer for each library

• Use another format than Makefile to have easily parsable meta data. Or add target to generate json from makefile.