io7m | single-page | multi-page | epub | Montarre User Manual 0.0.5
6.5. com.io7m.montarre.shell
Previous
Front Matter
Up
Front Matter
Next

# 7. Package Format 1.0 Specification

- 7.1. Overview
- 7.2. Regular Expressions
- 7.3. Dotted Strings
- 7.4. Language
- 7.5. TranslatedText
- 7.6. Hash
  - 7.6.1. Overview
  - 7.6.2. Algorithm
  - 7.6.3. Value
- 7.7. Architecture Name
- 7.8. Operating System Name
- 7.9. Platform
- 7.10. Package
- 7.11. Metadata
  - 7.11.1. Overview
  - 7.11.2. ApplicationKind
  - 7.11.3. Categories
  - 7.11.4. Copying
    - 7.11.4.1. Overview
    - 7.11.4.2. License
    - 7.11.4.3. Copyright
  - 7.11.5. Description
  - 7.11.6. Flatpak
    - 7.11.6.1. Overview
    - 7.11.6.2. Runtimes
    - 7.11.6.3. Permissions
  - 7.11.7. JavaInfo
    - 7.11.7.1. Overview
    - 7.11.7.2. Required JDK Version
    - 7.11.7.3. Main Module
  - 7.11.8. Links
    - 7.11.8.1. Overview
    - 7.11.8.2. Roles
  - 7.11.9. LongDescription
    - 7.11.9.1. Overview
    - 7.11.9.2. Paragraph
    - 7.11.9.3. Feature
  - 7.11.10. Names
    - 7.11.10.1. Overview
    - 7.11.10.2. Package Name
    - 7.11.10.3. Human Name
    - 7.11.10.4. Short Name
  - 7.11.11. Vendor
    - 7.11.11.1. Overview
    - 7.11.11.2. Name
    - 7.11.11.3. ID
  - 7.11.12. Version
    - 7.11.12.1. Overview
    - 7.11.12.2. Number
    - 7.11.12.3. Date
- 7.12. Manifest
  - 7.12.1. Overview
  - 7.12.2. FileName
  - 7.12.3. Modules
  - 7.12.4. PlatformModules
  - 7.12.5. Resources
- 7.13. Serialization
  - 7.13.1. Overview
  - 7.13.2. ZIP
  - 7.13.3. XML
  - 7.13.4. XML Schema
- 7.14. Model Sources

## 7.1. Overview

1
This section specifies the format of version 1.0 montarre packages.
2
This specification is divided into an abstract model and a separate serialization. The purpose of the model is to describe the semantics of montarre packages; the actual meaning of the data within, and to describe properties and invariants that must be true for all valid montarre packages. The serialization section describes the on-disk formats used for distribution.
3
The formal specification described here is written in the Gallina specification language of the Coq theorem prover. The language is a total, pure-functional, dependently-typed language allowing for describing systems in rigorous detail including machine-checked proofs of various chosen properties.
4
The full sources of the entire specification are published at the end of this section.

## 7.2. Regular Expressions

1
The specification makes use of regular expressions to specify the required formats of some string types. The regular expression language used should be assumed to be the Java regular expression language.
2
The specification itself axiomatizes regular expressions using the following definitions:

### 7.2.3. RegularExpressionT

    (** The opaque, abstract type of regular expressions. *)
    Parameter RegularExpressionT : string -> Set.

### 7.2.4. regex

    (** For the sake of specification simplicity, we assume that all
        strings are valid regular expressions. *)
    Parameter regex : forall (s : string), RegularExpressionT s.

### 7.2.5. matches

    (** A proposition that states that a given regular expression
        matches a given string. *)
    Parameter matches : forall (s : string) {e : string},
      RegularExpressionT e -> Prop.

### 7.2.6. matchesDecidable

    (** Whether a string matches a regular expression is decidable. *)
    Parameter matchesDecidable : forall
      (s : string)
      {e : string}
      (r : RegularExpressionT e),
        {matches s r}+{~matches s r}.

## 7.3. Dotted Strings

1
A Lanark dotted string is a string conforming to the regular expression given in the Lanark specification.

### 7.3.2. Dotted String

    Definition lanarkDottedString :=
      forall (s : string),
        matches s (regex "([a-z][a-z0-9_-]{0,63})(\.[a-z][a-z0-9_-]{0,62}){0,15}").

## 7.4. Language

1
A language value is an IETF BCP 47 language tag identifying a language.

### 7.4.2. Language

    Definition LanguageT :=
      string.

3
Example language values include: "en", "yi-Hebr", "gsw-u-sd-chzh".

## 7.5. TranslatedText

1
A translated text value is a record consisting of a piece of text in a specified language, along with a map consisting of translations of that text indexed by language.

### 7.5.2. Translated Text

    Inductive TranslatedTextT := TranslatedText {
      language     : LanguageT;
      text         : string;
      translations : LanguageMaps.t string
    }.

## 7.6. Hash

## 7.6.1. Overview

1
A hash is a record consisting of an algorithm and a value.

### 7.6.1.2. Hash

    Inductive HashT := Hash {
      hashAlgorithm : HashAlgorithmT;
      hashValue     : HashValueT
    }.

## 7.6.2. Algorithm

1
A hash algorithm specifies the name of a cryptographic hash algorithm. The names must be taken from the Java message digest algorithm name specification.

### 7.6.2.2. Algorithm

    Definition HashAlgorithmT :=
      string.

## 7.6.3. Value

1
A hash value is an ASCII, lowercase, hexadecimal text serialization of the binary output of a hash algorithm.

### 7.6.3.2. Value

    Inductive HashValueT :=
      HashValue : forall (s : string),
        matches s (regex "[a-f0-9]{2,256}")
          -> HashValueT.

## 7.7. Architecture Name

1
An architecture name is a unique name for a particular hardware architecture. It represents an attempt to provide a consistent naming convention for hardware types [3].
2
An architecture name is a string conforming to the regular expression [a-z][a-z0-9_-]{0,32}.

### 7.7.3. Architecture Name

    Inductive ArchitectureNameT :=
      ArchitectureName : forall (s : string),
        matches s (regex "[a-z][a-z0-9_-]{0,32}")
          -> ArchitectureNameT.

4
This specification recognizes the following architecture names:

### 7.7.5. Architecture Names

Name | Description
--- | ---
aarch_64 | 64-bit ARM
arm_32 | 32-bit ARM
loongarch_64 | 64-bit LoongArch
mips_32 | 32-bit MIPS
mips_64 | 64-bit MIPS
mipsle_32 | 32-bit little-endian MIPS
mipsle_64 | 64-bit little-endian MIPS
ppc_32 | 32-bit PowerPC
ppc_64 | 64-bit PowerPC
ppcle_32 | 32-bit little-endian PowerPC
ppcle_64 | 64-bit little-endian PowerPC
riscv_32 | 32-bit RISC-V
riscv_64 | 64-bit RISC-V
s390_64 | 64-bit IBM z/Architecture
sparc_32 | 32-bit SPARC
sparc_64 | 64-bit SPARC
x86_32 | 32-bit x86
x86_64 | 64-bit x86

6
The special name unknown is assigned to unrecognized hardware architectures. The unknown name is not permitted to appear in package declarations.

## 7.8. Operating System Name

1
An operating system name is a unique name for a particular operating system. It represents an attempt to provide a consistent naming convention for operating systems.
2
An operating system name is a string conforming to the regular expression [a-z][a-z0-9_-]{0,32}.

### 7.8.3. Operating System Name

    Inductive OperatingSystemNameT :=
      OperatingSystemName : forall (s : string),
        matches s (regex "[a-z][a-z0-9_-]{0,32}")
          -> OperatingSystemNameT.

4
This specification recognizes the following operating system names:

### 7.8.5. Architecture Names

Name | Description
--- | ---
aix | IBM AIX
freebsd | FreeBSD
hpux | HP-UX
linux | Linux
netbsd | NetBSD
openbsd | OpenBSD
os400 | IBM i
osx | MacOS
solaris | Oracle Solaris
windows | Microsoft Windows

6
The special name unknown is assigned to unrecognized operating systems. The unknown name is not permitted to appear in package declarations.

## 7.9. Platform

1
A platform is a record consisting of an architecture name and operating system name.

### 7.9.2. Platform

    Inductive PlatformT := Platform {
      platformArch : ArchitectureNameT;
      platformOS   : OperatingSystemNameT
    }.

## 7.10. Package

1
A montarre package contains a single package declaration which specifies metadata and a manifest.

## 7.11. Metadata

## 7.11.1. Overview

1
The metadata for the package is a record describing the package itself. It provides important information pertaining to the identity of the package, information pertaining to the runtime environment required to run the package, and information used to produce listings in packaging environments such as Flatpak.

### 7.11.1.2. Metadata

    Inductive MetadataT := Metadata {
      metaApplicationKind  : ApplicationKindT;
      metaCategories       : list CategoryT;
      metaCopying          : CopyingT;
      metaDescription      : DescriptionT;
      metaFlatpak          : FlatpakT;
      metaJavaInfo         : JavaInfoT;
      metaLinks            : list LinkT;
      metaLongDescriptions : LanguageMaps.t LongDescriptionT;
      metaNames            : NamesT;
      metaVendor           : VendorT;
      metaVersion          : VersionT
    }.

## 7.11.2. ApplicationKind

1
The application kind of a package is one of the following values:

### 7.11.2.2. ApplicationKind

Value | Description
--- | ---
CONSOLE | The application is a text-only console application.
GRAPHICAL | The application is a graphical application.

### 7.11.2.3. Application Kind

    Inductive ApplicationKindT :=
      | CONSOLE
      | GRAPHICAL
      .

## 7.11.3. Categories

1
A category is a string conforming to the regular expression [A-Z][A-Za-z0-9_-]{0,128}. A package has zero or more categories.

### 7.11.3.2. Category

    Inductive CategoryT :=
      Category : forall (s : string),
        matches s (regex "[A-Z][A-Za-z0-9_-]{0,128}")
          -> CategoryT.

3
Categories should be taken from the Freedesktop.org category registry.
4
Example category values include: "Building", "Development".

## 7.11.4. Copying

## 7.11.4.1. Overview

1
The copying information for a package is a record consisting of a license and a copyright.

### 7.11.4.1.2. Copying

    Inductive CopyingT := Copying {
      license   : LicenseT;
      copyright : CopyrightT
    }.

## 7.11.4.2. License

1
A license is an SPDX license identifier denoting the license of the package.

### 7.11.4.2.2. License

    Definition LicenseT :=
      string.

3
Example license values include: "ISC", "Apache-2.0", "BSD-3-Clause", "GPL-3.0-or-later".

## 7.11.4.3. Copyright

1
A copyright is a simple copyright string that indicates the current holder of the copyright on the package.

### 7.11.4.3.2. Copyright

    Definition CopyrightT :=
      string.

3
An example copyright value is: "Copyright © 2024 Mark Raynsford <code@io7m.com> https://www.io7m.com".

## 7.11.5. Description

1
A description is a short translated text that provides a summary of the package.

### 7.11.5.2. Description

    Definition DescriptionT :=
      TranslatedTextT.

## 7.11.6. Flatpak

## 7.11.6.1. Overview

1
The Flatpak information for a package provides extra metadata used to produce Flatpaks.

### 7.11.6.1.2. Flatpak

    Inductive FlatpakT := Flatpak {
      flatpakPermissions : list FlatpakPermissionT;
      flatpakRuntimes    : list FlatpakRuntimeT
    }.

## 7.11.6.2. Runtimes

1
A Flatpak runtime consists of a name, a version, and a role.

### 7.11.6.2.2. Flatpak Runtime

    Inductive FlatpakRuntimeT := FlatpakRuntime {
      flatpakRuntimeName    : string;
      flatpakRuntimeVersion : string;
      flatpakRuntimeRole    : FlatpakRuntimeRoleT
    }.

3
Roles may be one of the following values:

### 7.11.6.2.4. Flatpak Roles

Value | Description
--- | ---
SDK | A runtime for building applications.
PLATFORM | A runtime for running applications.

### 7.11.6.2.5. Flatpak Runtime Role

    Inductive FlatpakRuntimeRoleT :=
      | SDK
      | PLATFORM
      .

## 7.11.6.3. Permissions

1
A Flatpak permission denotes that the named permission will be granted to the application when it runs as a Flatpak.

### 7.11.6.3.2. Flatpak Permission

    Definition FlatpakPermissionT :=
      string.

3
Example permission values include: "--share=net", "--socket=x11".

## 7.11.7. JavaInfo

## 7.11.7.1. Overview

1
The java info information for a package is a record consisting of a required JDK version and a main module.

### 7.11.7.1.2. Java Info

    Inductive JavaInfoT := JavaInfo {
      requiredJDKVersion : nat;
      mainModule         : string
    }.

## 7.11.7.2. Required JDK Version

1
The required JDK version specifies the lower bound of the major version of the Java runtime required to use this package.

## 7.11.7.3. Main Module

1
The main module specifies the fully-qualified name of the application's main class.
2
An example main module value is: "com.io7m.montarre.cmdline/com.io7m.montarre.cmdline.MMain".

## 7.11.8. Links

## 7.11.8.1. Overview

1
A link is a target reference to an external website or entity, along with a role describing the relationship between that entity and the package.
2
The target of a link must be a valid RFC 3986 URI.

### 7.11.8.1.3. Link

    Inductive LinkT := Link {
      linkRole   : LinkRoleT;
      linkTarget : string
    }.

## 7.11.8.2. Roles

1
A role is one of the following values:

### 7.11.8.2.2. Role Values

Value | Description
--- | ---
ISSUES | A link to an issue tracker.
HOME_PAGE | A link to a home page.
DONATION | A link to a donation page.
CONTACT | A link to a contact page.
FAQ | A link to an FAQ page.
TRANSLATE | A link to a translation page.
CONTRIBUTE | A link to a contribution page.
SCM | A link to an SCM repository.

### 7.11.8.2.3. Link Role

    Inductive LinkRoleT :=
      | ISSUES
      | HOME_PAGE
      | DONATION
      | CONTACT
      | FAQ
      | TRANSLATE
      | CONTRIBUTE
      | SCM
      .

## 7.11.9. LongDescription

## 7.11.9.1. Overview

1
The long description information for a package is a set of paragraphs and features. A long description has an associated language and there may be at most one long description per language in a given package.

### 7.11.9.1.2. Long Description

    Inductive LongDescriptionT := LongDescription {
      descriptionLanguage : LanguageT;
      descriptions        : list ParagraphT;
      features            : list FeatureT
    }.

## 7.11.9.2. Paragraph

1
A paragraph is a humanly readable description of some aspect of the package for marketing purposes.

### 7.11.9.2.2. Paragraph

    Definition ParagraphT :=
      string.

## 7.11.9.3. Feature

1
A feature is a humanly readable description of one of the features provided by the package for marketing purposes.

### 7.11.9.3.2. Feature

    Definition FeatureT :=
      string.

## 7.11.10. Names

## 7.11.10.1. Overview

1
The names information for a package is a record consisting of a set of different types of names for the package.

### 7.11.10.1.2. Names

    Inductive NamesT := Names {
      namePackage : PackageNameT;
      nameShort   : ShortNameT;
      nameHuman   : HumanNameT
    }.

## 7.11.10.2. Package Name

1
The package name is a unique identifier for the package, specified as a dotted string.

### 7.11.10.2.2. Package Name

    Definition PackageNameT :=
      lanarkDottedString.

3
Example package name values include: "com.io7m.montarre", "com.io7m.lanark".

## 7.11.10.3. Human Name

1
The human name is a friendly, human-readable name for the package.

### 7.11.10.3.2. Human Name

    Definition HumanNameT :=
      string.

3
An example human name value is "Montarre".

## 7.11.10.4. Short Name

1
The short name is a name conforming to the regular expression [a-z][a-z0-9_-]{0,128} [2].

### 7.11.10.4.2. Short Name

    Inductive ShortNameT :=
      ShortName : forall (s : string),
        matches s (regex "[a-z][a-z0-9_-]{0,128}")
          -> ShortNameT.

3
An example short name value is "montarre".

## 7.11.11. Vendor

## 7.11.11.1. Overview

1
The vendor information for a package is a record consisting of a vendor name and a unique vendor ID.

### 7.11.11.1.2. Vendor

    Inductive VendorT := Vendor {
      vendorId   : VendorIDT;
      vendorName : VendorNameT
    }.

## 7.11.11.2. Name

1
The vendor name is the humanly-readable name of the vendor of the package, conforming to the regular expression [a-zA-Z][A-Za-z0-9_-]{0,128} [1].

### 7.11.11.2.2. Vendor Name

    Inductive VendorNameT :=
      VendorName : forall (s : string),
        matches s (regex "[a-zA-Z][A-Za-z0-9_-]{0,128}")
          -> VendorNameT.

## 7.11.11.3. ID

1
The vendor ID is a unique identifier for the vendor of the package, specified as a dotted string.

### 7.11.11.3.2. Vendor ID

    Definition VendorIDT :=
      lanarkDottedString.

3
Example vendor ID values include: "com.io7m", "com.example".

## 7.11.12. Version

## 7.11.12.1. Overview

1
The version information for a package is a record consisting of a version number and a version/release date.

### 7.11.12.1.2. Version

    Inductive VersionT := Version {
      versionNumber : VersionNumberT;
      versionDate   : VersionDateT
    }.

## 7.11.12.2. Number

1
The version number is the semantic version of the package.

### 7.11.12.2.2. Version Number

    Inductive VersionNumberT := VersionNumber {
      major     : nat;
      minor     : nat;
      patch     : nat;
      qualifier : option string
    }.

## 7.11.12.3. Date

1
The version date is an ISO 8601 date string denoting the release date of this version of the package.

### 7.11.12.3.2. Version Date

    Inductive VersionDateT :=
      VersionDate : forall (s : string),
        matches s (regex "[0-9]{4}-[0-9]{2}-[0-9]{2}")
          -> VersionDateT.

3
Example version date values include: "2024-10-13", "2001-01-23".

## 7.12. Manifest

## 7.12.1. Overview

1
A manifest consists of a set of items.

### 7.12.1.2. Manifest

    Inductive ManifestT := Manifest {
      manifestItems : list ItemT
    }.

3
An item is a Module, PlatformModule, or a Resource.

### 7.12.1.4. Item

    Inductive ItemT :=
      | ItemModule         : ModuleT         -> ItemT
      | ItemPlatformModule : PlatformModuleT -> ItemT
      | ItemResource       : ResourceT       -> ItemT
      .

5
Items within a manifest must have unique file names. More formally, for a manifest m, there cannot exist two different items i0 and i1 in m such that i0 and i1 have filenames that are the same.

### 7.12.1.6. Manifest File Names

    Definition manifesItemsFilenamesUnique :=
      forall (m : ManifestT),
        forall (i0 : ItemT),
          In i0 (manifestItems m)
            -> ~(exists i1 : ItemT,
                   (In i1 (manifestItems m))
                /\ (i0 <> i1)
                /\ (fileNamesSame (itemFileName i0) (itemFileName i1))).

7
Each item carries a hash value denoting the cryptographic hash of the contents of the item within the package.

## 7.12.2. FileName

1
A file name is a unique name assigned to a manifest item. File names are case-insensitive strings that conform to the regular expression ([\p{L}\p{N}_\-.+]+)(/[\p{L}\p{N}_\-.+]+)*

### 7.12.2.2. FileName

    Inductive FileNameT :=
      FileName : forall (s : string),
        matches s (regex "([\p{L}\p{N}_\-.+]+)(/[\p{L}\p{N}_\-.+]+)*")
          -> FileNameT.

3
Intuitively, a filename can be considered to be a non-empty /-separated list of file name segments that each conform to the regular expression [\p{L}\p{N}_\-.+]+. Accordingly, filenames cannot start with slashes, cannot end with trailing slashes, and cannot contain sequences of repeating slashes.
4
The specification axiomatizes the concept of converting a string to uppercase. The uppercase transform of a string should be understood to be a string where every character has been converted to its uppercase equivalent in a neutral locale.

### 7.12.2.5. Uppercase Transform

    (** A function that produces an uppercase version of the given string. *)
    Parameter uppercaseOf : string -> string.

6
A proposition that states that two strings have the same uppercase transform:

### 7.12.2.7. Uppercase Same

    Definition uppercaseSame (s t : string) :=
      uppercaseOf s = uppercaseOf t.

8
Accordingly, as file names are case-insensitive, then two file names are equal if their uppercase transforms are equal:

### 7.12.2.9. File Names Same

    (** A proposition that states that two file names are the same if their
        uppercase transformations are the same. *)
    Definition fileNamesSame (s t : FileNameT) :=
      match s, t with
      | FileName fs _, FileName ft _ => uppercaseSame fs ft
      end.

## 7.12.3. Modules

1
A module represents a platform-neutral jar file that will be placed onto the Java module path regardless of the underlying hardware architecture and operating system on which the application is running.

### 7.12.3.2. Module

    Inductive ModuleT :=
      Module : FileNameT -> HashT -> ModuleT.

## 7.12.4. PlatformModules

1
A platform module represents a platform-specific jar file that will be placed onto the Java module path when the hardware architecture and operating system of the module matches that of the platform upon which the application is running.

### 7.12.4.2. PlatformModule

    Inductive PlatformModuleT :=
      PlatformModule : FileNameT -> HashT -> PlatformT -> PlatformModuleT.

## 7.12.5. Resources

1
A resource is an arbitrary file associated with the package. Resources are typically used to provide icons, BOMs, and screenshots for the package.

### 7.12.5.2. Resource

    Inductive ResourceT :=
      Resource : FileNameT -> HashT -> ResourceRoleT -> CaptionT -> ResourceT.

3
A resource has an associated role that describes the purpose of the resource.

### 7.12.5.4. Resource Role

    Inductive ResourceRoleT :=
      | BOM
      | LICENSE
      | ICO_WINDOWS
      | ICON_16
      | ICON_24
      | ICON_32
      | ICON_48
      | ICON_64
      | ICON_128
      | ICON_256
      | ICON_512
      | ICON_SVG
      | SCREENSHOT
      .

5
A role has one of the following values:

### 7.12.5.6. Resource Role Values

Value | Description
--- | ---
BOM | A bill-of-materials. Recommended to be in CycloneDX format.
LICENSE | A plain text license file.
ICO_WINDOWS | A Windows application icon (".ico").
ICON_16 | A 16x16 application icon.
ICON_24 | A 24x24 application icon.
ICON_32 | A 32x32 application icon.
ICON_48 | A 48x48 application icon.
ICON_64 | A 64x64 application icon.
ICON_128 | A 128x128 application icon.
ICON_256 | A 256x256 application icon.
ICON_512 | A 512x512 application icon.
ICON_SVG | An arbitrarily scaled SVG icon.
SCREENSHOT | A screenshot.

7
A resource has an associated caption that provides a human-readable description of the resource. This is used, for example, to describe the contents of screenshots for use in Flatpak listings.

### 7.12.5.8. Resource Caption

    Definition CaptionT :=
      TranslatedTextT.

## 7.13. Serialization

## 7.13.1. Overview

1
montarre package declarations are serialized to an XML format with a strict XSD schema. The serialized package declaration, and all the package contents, are collected into a ZIP file with some extra restrictions on the entries. Extra restrictions are applied to the ZIP container and the XML data to assist with ensuring that montarre packages are reproducible.

## 7.13.2. ZIP

1
montarre packages are ZIP files with the file extension .mpk. The following restrictions are applied to the entries of the ZIP file:

### 7.13.2.2. ZIP Entry Restrictions

- All entry names in the ZIP file must be valid file names.
- All entry names in the ZIP file must be transformed to uppercase in a neutral locale.
- All entries must be written with creation, modification, and last access dates of 2024-10-14T00:00:00Z.
- All entries, except for the first entry, must be written such that their names appear in ascending alphabetical order.
- The first entry in the file must be META-INF/MONTARRE/PACKAGE.XML.

3
The package declaration is serialized to XML and stored in the META-INF/MONTARRE/PACKAGE.XML entry in the ZIP file.
4
An example valid ZIP listing of a package is as follows:

### 7.13.2.5. Example ZIP Listing

    Length      Date    Time    Name
    ---------  ---------- -----   ----
         9147  2024-10-14 00:00   META-INF/MONTARRE/PACKAGE.XML
        15052  2024-10-14 00:00   LIB/COM.IO7M.ANETHUM.API-1.1.1.JAR
        42944  2024-10-14 00:00   LIB/COM.IO7M.BLACKTHORNE.CORE-2.0.2.JAR
         5166  2024-10-14 00:00   LIB/COM.IO7M.BLACKTHORNE.JXE-2.0.2.JAR
        38355  2024-10-14 00:00   LIB/COM.IO7M.JAFFIRM.CORE-4.0.1.JAR
         5569  2024-10-14 00:00   LIB/COM.IO7M.JCIP-2.0.1.JAR
        21462  2024-10-14 00:00   LIB/COM.IO7M.JDOWNLOAD.CORE-1.0.0.JAR
        12841  2024-10-14 00:00   LIB/COM.IO7M.JLEXING.CORE-3.2.0.JAR
        10227  2024-10-14 00:00   LIB/COM.IO7M.JMULTICLOSE.CORE-1.1.3.JAR
         4505  2024-10-14 00:00   LIB/COM.IO7M.JUNREACHABLE.CORE-4.0.2.JAR
        21622  2024-10-14 00:00   LIB/COM.IO7M.JXE.CORE-2.0.0.JAR
         6730  2024-10-14 00:00   LIB/COM.IO7M.JXTRAND.API-2.1.0.JAR
         9797  2024-10-14 00:00   LIB/COM.IO7M.JXTRAND.VANILLA-2.1.0.JAR
        10609  2024-10-14 00:00   LIB/COM.IO7M.LANARK.CORE-1.2.0.JAR
       131113  2024-10-14 00:00   LIB/COM.IO7M.MONTARRE.API-0.0.1-SNAPSHOT.JAR
        48154  2024-10-14 00:00   LIB/COM.IO7M.MONTARRE.CMDLINE-0.0.1-SNAPSHOT.JAR
        35065  2024-10-14 00:00   LIB/COM.IO7M.MONTARRE.IO-0.0.1-SNAPSHOT.JAR
       175186  2024-10-14 00:00   LIB/COM.IO7M.MONTARRE.NATIVEPACK-0.0.1-SNAPSHOT.JAR
         7016  2024-10-14 00:00   LIB/COM.IO7M.MONTARRE.SCHEMA-0.0.1-SNAPSHOT.JAR
        55257  2024-10-14 00:00   LIB/COM.IO7M.MONTARRE.XML-0.0.1-SNAPSHOT.JAR
       109688  2024-10-14 00:00   LIB/COM.IO7M.QUARREL.CORE-1.6.1.JAR
         5985  2024-10-14 00:00   LIB/COM.IO7M.QUARREL.EXT.LOGBACK-1.6.1.JAR
         9077  2024-10-14 00:00   LIB/COM.IO7M.SELTZER.API-1.1.0.JAR
         9750  2024-10-14 00:00   LIB/COM.IO7M.STREAMTIME.CORE-1.0.0.JAR
        11838  2024-10-14 00:00   LIB/COM.IO7M.VERONA.CORE-1.0.1.JAR
       372687  2024-10-14 00:00   LIB/COMMONS-CODEC-1.17.1.JAR
      1087319  2024-10-14 00:00   LIB/COMMONS-COMPRESS-1.27.1.JAR
       515978  2024-10-14 00:00   LIB/COMMONS-IO-2.17.0.JAR
       673587  2024-10-14 00:00   LIB/COMMONS-LANG3-3.17.0.JAR
       304513  2024-10-14 00:00   LIB/LOGBACK-CLASSIC-1.5.8.JAR
       619394  2024-10-14 00:00   LIB/LOGBACK-CORE-1.5.8.JAR
        69435  2024-10-14 00:00   LIB/SLF4J-API-2.0.16.JAR
       262317  2024-10-14 00:00   META/BOM.XML
       102134  2024-10-14 00:00   META/ICON.ICO
        41273  2024-10-14 00:00   META/ICON128.PNG
          544  2024-10-14 00:00   META/ICON16.PNG
          732  2024-10-14 00:00   META/ICON24.PNG
         1973  2024-10-14 00:00   META/ICON32.PNG
         5461  2024-10-14 00:00   META/ICON48.PNG
        10050  2024-10-14 00:00   META/ICON64.PNG
          768  2024-10-14 00:00   META/LICENSE.TXT
        16002  2024-10-14 00:00   META/SCREENSHOT.PNG
    ---------                     -------
      4896322                     42 files

## 7.13.3. XML

1
Package declarations must be serialized according to the included schema with the following restrictions:

### 7.13.3.2. ZIP Entry Restrictions

- XML must be serialized indented to four spaces.
- The character content of elements must be serialized using a function equivalent to XSLT's normalize-space() function.
- After indenting, XML must be canonicalized using the Exclusive XML Canonicalization Version 1.0 algorithm.

## 7.13.4. XML Schema

1
The package declaration schema is as follows:

### 7.13.4.2. XML Schema

    <?xml version="1.0" encoding="UTF-8" ?>

    <xsd:schema xmlns:xsd="http://www.w3.org/2001/XMLSchema"
                targetNamespace="urn:com.io7m.montarre.package:1"
                xmlns:mp="urn:com.io7m.montarre.package:1">

      <xsd:simpleType name="ApplicationKindType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            The type of application. Many packaging systems and some operating systems distinguish between "console" and
            "graphical" applications.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:enumeration value="CONSOLE"/>
          <xsd:enumeration value="GRAPHICAL"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="VersionType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            An arbitrary version number.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string"/>
      </xsd:simpleType>

      <xsd:simpleType name="CategoryNameType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A category name.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="[A-Z][A-Za-z0-9_-]{0,128}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="VendorIDType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A vendor ID; A Lanark dotted name.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="([a-z][a-z0-9_-]{0,63})(\.[a-z][a-z0-9_-]{0,62}){0,15}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="PackageNameType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A package name; A Lanark dotted name.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="([a-z][a-z0-9_-]{0,63})(\.[a-z][a-z0-9_-]{0,62}){0,15}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="ShortNameType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A short package name. Used for systems such as Debian packages.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="[a-z][a-z0-9_-]{0,128}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="HashAlgorithmNameType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A hash algorithm name. See " Java Security Standard Algorithm Names".
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="[A-Z][A-Z0-9_-]{0,128}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="HashValueType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A hex-encoded hash value.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="[a-f0-9]{2,256}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="OSNameType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            An operating system name.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="[a-z][a-z0-9_-]{0,32}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="ArchitectureNameType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A hardware architecture name.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="[a-z][a-z0-9_-]{0,32}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="VendorNameType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A vendor name. Must be a filesystem-safe name as these names can be used as directories in Windows installers.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="[a-zA-Z][A-Za-z0-9_-]{0,128}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="FlatpakPermissionType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A flatpak permission.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="--[a-z\-]+(=[a-zA-Z0-9\\._\-/:~]+)?"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:element name="Version">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            Version information.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:complexType>
          <xsd:attribute name="Number"
                         type="xsd:string"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The version number. Typically in semantic version form ("2.0.0", "1.0.0-SNAPSHOT", etc).
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Date"
                         type="xsd:date"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The date the version was set.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Vendor">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A vendor.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:complexType>
          <xsd:attribute name="ID"
                         type="mp:VendorIDType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The unique vendor ID.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Name"
                         type="mp:VendorNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The vendor name.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Category">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A category applied to an application.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:complexType>
          <xsd:attribute name="Name"
                         type="mp:CategoryNameType"
                         use="required"/>
        </xsd:complexType>
      </xsd:element>

      <xsd:simpleType name="LinkRole">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            The role of a link.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:enumeration value="ISSUES"/>
          <xsd:enumeration value="HOME_PAGE"/>
          <xsd:enumeration value="DONATION"/>
          <xsd:enumeration value="CONTACT"/>
          <xsd:enumeration value="FAQ"/>
          <xsd:enumeration value="TRANSLATE"/>
          <xsd:enumeration value="CONTRIBUTE"/>
          <xsd:enumeration value="SCM"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:element name="Link">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A link.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:complexType>
          <xsd:attribute name="Role"
                         type="mp:LinkRole"
                         use="required"/>
          <xsd:attribute name="Target"
                         type="xsd:anyURI"
                         use="required"/>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Copying">
        <xsd:complexType>
          <xsd:attribute name="License"
                         type="xsd:string"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                An SPDX license identifier such as "ISC".
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Copyright"
                         type="xsd:string"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                A copyright string such as "Copyright © 2024 Mark Raynsford &lt;code@io7m.com> https://www.io7m.com".
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="JavaInfo">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            Information relative to the Java runtime.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:complexType>
          <xsd:attribute name="RequiredJDKVersion"
                         type="xsd:unsignedLong"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The required JDK version.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="MainModule"
                         type="xsd:string"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The main application module. This should be in a fully-qualified module form such as
                "com.io7m.montarre.cmdline/com.io7m.montarre.cmdline.MMain".
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Names">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            Package name information.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:complexType>
          <xsd:attribute name="Name"
                         type="mp:PackageNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The package name.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="ShortName"
                         type="mp:ShortNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The package short name. The short name is used when exporting to some native package systems such as Debian
                packages.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="HumanName"
                         type="xsd:string"
                         use="optional">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The optional human-readable application name. This will default to the package name if not specified.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:simpleType name="FlatpakRuntimeRole">
        <xsd:restriction base="xsd:string">
          <xsd:enumeration value="PLATFORM"/>
          <xsd:enumeration value="SDK"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:element name="FlatpakPermission">
        <xsd:complexType>
          <xsd:attribute name="Value"
                         use="required"
                         type="mp:FlatpakPermissionType">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                A flatpak permission such as "--share=network", "--share=ipc", etc.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="FlatpakRuntime">
        <xsd:complexType>
          <xsd:attribute name="Name"
                         use="required"
                         type="xsd:string">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                A flatpak runtime such as "org.freedesktop.Platform".
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Version"
                         use="required"
                         type="xsd:string">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                A flatpak runtime version such as "24.08".
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Role"
                         use="required"
                         type="mp:FlatpakRuntimeRole">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                A runtime role such as "PLATFORM" or "SDK".
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Flatpak">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            Metadata specific to Flatpak packages.
          </xsd:documentation>
        </xsd:annotation>

        <xsd:complexType>
          <xsd:sequence>
            <xsd:sequence minOccurs="0"
                          maxOccurs="unbounded">
              <xsd:element ref="mp:FlatpakPermission"/>
            </xsd:sequence>
            <xsd:sequence minOccurs="0"
                          maxOccurs="unbounded">
              <xsd:element ref="mp:FlatpakRuntime"/>
            </xsd:sequence>
          </xsd:sequence>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Text">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A text element in a specific language.
          </xsd:documentation>
        </xsd:annotation>

        <xsd:complexType mixed="true">
          <xsd:attribute name="Language"
                         use="required"
                         type="xsd:NMTOKEN"/>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Description">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A humanly-readable package description.
          </xsd:documentation>
        </xsd:annotation>

        <xsd:complexType>
          <xsd:sequence minOccurs="0"
                        maxOccurs="1">
            <xsd:element ref="mp:Text"/>
          </xsd:sequence>
        </xsd:complexType>

        <xsd:unique name="DescriptionTextLanguageUnique">
          <xsd:selector xpath="mp:Text"/>
          <xsd:field xpath="@Language"/>
        </xsd:unique>
      </xsd:element>

      <xsd:element name="Feature">
        <xsd:complexType mixed="true"/>
      </xsd:element>

      <xsd:element name="Paragraph">
        <xsd:complexType mixed="true"/>
      </xsd:element>

      <xsd:element name="LongDescription">
        <xsd:complexType>
          <xsd:sequence>
            <xsd:sequence minOccurs="1"
                          maxOccurs="unbounded">
              <xsd:element ref="mp:Paragraph"/>
            </xsd:sequence>
            <xsd:sequence minOccurs="0"
                          maxOccurs="unbounded">
              <xsd:element ref="mp:Feature"/>
            </xsd:sequence>
          </xsd:sequence>

          <xsd:attribute name="Language"
                         use="required"
                         type="xsd:NMTOKEN"/>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Caption">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A humanly-readable resource caption.
          </xsd:documentation>
        </xsd:annotation>

        <xsd:complexType>
          <xsd:sequence minOccurs="1"
                        maxOccurs="unbounded">
            <xsd:element ref="mp:Text"/>
          </xsd:sequence>
        </xsd:complexType>

        <xsd:unique name="CaptionTextLanguageUnique">
          <xsd:selector xpath="mp:Text"/>
          <xsd:field xpath="@Language"/>
        </xsd:unique>
      </xsd:element>

      <xsd:element name="Metadata">
        <xsd:complexType>
          <xsd:sequence>
            <xsd:sequence minOccurs="0"
                          maxOccurs="unbounded">
              <xsd:element ref="mp:Category"/>
            </xsd:sequence>
            <xsd:element ref="mp:Copying"/>
            <xsd:element ref="mp:Description"/>
            <xsd:sequence>
              <xsd:element ref="mp:Flatpak"
                           minOccurs="0"
                           maxOccurs="1"/>
            </xsd:sequence>
            <xsd:element ref="mp:JavaInfo"/>
            <xsd:sequence minOccurs="0"
                          maxOccurs="unbounded">
              <xsd:element ref="mp:Link"/>
            </xsd:sequence>
            <xsd:sequence minOccurs="0"
                          maxOccurs="1">
              <xsd:element ref="mp:LongDescription"/>
            </xsd:sequence>
            <xsd:element ref="mp:Names"/>
            <xsd:element ref="mp:Vendor"/>
            <xsd:element ref="mp:Version"/>
          </xsd:sequence>

          <xsd:attribute name="ApplicationKind"
                         type="mp:ApplicationKindType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The kind of the application.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="PlatformDependentModule">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A module that is only used when running on a specific platform.
          </xsd:documentation>
        </xsd:annotation>

        <xsd:complexType>
          <xsd:attribute name="File"
                         type="xsd:string"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file name within the package.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="HashAlgorithm"
                         type="mp:HashAlgorithmNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file hash algorithm name.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="HashValue"
                         type="mp:HashValueType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file hash value.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="OperatingSystem"
                         type="mp:OSNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The operating system on which this module is used.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Architecture"
                         type="mp:ArchitectureNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The hardware architecture on which this module is used.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Module">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A module that is used on all platforms.
          </xsd:documentation>
        </xsd:annotation>

        <xsd:complexType>
          <xsd:attribute name="File"
                         type="xsd:string"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file name within the package.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="HashAlgorithm"
                         type="mp:HashAlgorithmNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file hash algorithm name.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="HashValue"
                         type="mp:HashValueType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file hash value.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:simpleType name="ResourceRole">
        <xsd:restriction base="xsd:string">
          <xsd:enumeration value="BOM"/>
          <xsd:enumeration value="ICON_128"/>
          <xsd:enumeration value="ICON_16"/>
          <xsd:enumeration value="ICON_24"/>
          <xsd:enumeration value="ICON_256"/>
          <xsd:enumeration value="ICON_32"/>
          <xsd:enumeration value="ICON_48"/>
          <xsd:enumeration value="ICON_64"/>
          <xsd:enumeration value="ICO_WINDOWS"/>
          <xsd:enumeration value="LICENSE"/>
          <xsd:enumeration value="SCREENSHOT"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:element name="Resource">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A metadata resource.
          </xsd:documentation>
        </xsd:annotation>

        <xsd:complexType>
          <xsd:sequence>
            <xsd:element ref="mp:Caption" minOccurs="0" maxOccurs="1"/>
          </xsd:sequence>

          <xsd:attribute name="File"
                         type="xsd:string"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file name within the package.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="HashAlgorithm"
                         type="mp:HashAlgorithmNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file hash algorithm name.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="HashValue"
                         type="mp:HashValueType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file hash value.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Role"
                         type="mp:ResourceRole"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The role of the resource.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:group name="ManifestItemGroup">
        <xsd:choice>
          <xsd:element ref="mp:Module"/>
          <xsd:element ref="mp:PlatformDependentModule"/>
          <xsd:element ref="mp:Resource"/>
        </xsd:choice>
      </xsd:group>

      <xsd:element name="Manifest">
        <xsd:complexType>
          <xsd:sequence minOccurs="0"
                        maxOccurs="unbounded">
            <xsd:group ref="mp:ManifestItemGroup"/>
          </xsd:sequence>
        </xsd:complexType>

        <xsd:key name="ManifestItemUnique">
          <xsd:selector xpath="mp:Module|mp:PlatformDependentModule|mp:BOM"/>
          <xsd:field xpath="@File"/>
        </xsd:key>
      </xsd:element>

      <xsd:element name="Package">
        <xsd:complexType>
          <xsd:sequence>
            <xsd:element ref="mp:Metadata"/>
            <xsd:element ref="mp:Manifest"/>
          </xsd:sequence>
        </xsd:complexType>
      </xsd:element>

    </xsd:schema>

## 7.14. Model Sources

1
The full sources of the specification model are provided here.

### 7.14.2. Montarre/Package.v

    Require Import Coq.Unicode.Utf8_core.
    Require Import Coq.Strings.String.
    Require Import Coq.Strings.Ascii.
    Require Import Coq.FSets.FMapInterface.
    Require Import Coq.FSets.FMapWeakList.
    Require Import Coq.FSets.FMapFacts.
    Require Import Coq.Structures.Equalities.

    (** A mini decidable type module to instantiate maps. *)
    Module StringMiniDec : MiniDecidableType
      with Definition t := string.

      Definition t        := string.
      Definition eq       := @Logic.eq t.
      Definition eq_refl  := @Logic.eq_refl t.
      Definition eq_sym   := @Logic.eq_sym t.
      Definition eq_trans := @Logic.eq_trans t.

      Theorem eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
      Proof. apply string_dec. Qed.
    End StringMiniDec.

    (** A usual decidable type module to instantiate maps. *)
    Module StringDec <: UsualDecidableType
      with Definition t := string
      with Definition eq := @Logic.eq string
    := Make_UDT StringMiniDec.

    (** A Maps module with string keys. *)
    Module StringMaps : FMapInterface.WS
      with Definition E.t  := string
      with Definition E.eq := @Logic.eq string
    := FMapWeakList.Make StringDec.

    (** The opaque, abstract type of regular expressions. *)
    Parameter RegularExpressionT : string -> Set.

    (** For the sake of specification simplicity, we assume that all
        strings are valid regular expressions. *)
    Parameter regex : forall (s : string), RegularExpressionT s.

    (** A proposition that states that a given regular expression
        matches a given string. *)
    Parameter matches : forall (s : string) {e : string},
      RegularExpressionT e -> Prop.

    (** Whether a string matches a regular expression is decidable. *)
    Parameter matchesDecidable : forall
      (s : string)
      {e : string}
      (r : RegularExpressionT e),
        {matches s r}+{~matches s r}.

    Definition lanarkDottedString :=
      forall (s : string),
        matches s (regex "([a-z][a-z0-9_-]{0,63})(\.[a-z][a-z0-9_-]{0,62}){0,15}").

    Inductive ApplicationKindT :=
      | CONSOLE
      | GRAPHICAL
      .

    Inductive CategoryT :=
      Category : forall (s : string),
        matches s (regex "[A-Z][A-Za-z0-9_-]{0,128}")
          -> CategoryT.

    Definition LicenseT :=
      string.

    Definition CopyrightT :=
      string.

    Inductive CopyingT := Copying {
      license   : LicenseT;
      copyright : CopyrightT
    }.

    Definition LanguageT :=
      string.

    (** A Maps module with language keys. *)
    Module LanguageMaps : FMapInterface.WS
      with Definition E.t  := LanguageT
      with Definition E.eq := @Logic.eq LanguageT
    := FMapWeakList.Make StringDec.

    Inductive TranslatedTextT := TranslatedText {
      language     : LanguageT;
      text         : string;
      translations : LanguageMaps.t string
    }.

    Definition DescriptionT :=
      TranslatedTextT.

    Inductive JavaInfoT := JavaInfo {
      requiredJDKVersion : nat;
      mainModule         : string
    }.

    Inductive LinkRoleT :=
      | ISSUES
      | HOME_PAGE
      | DONATION
      | CONTACT
      | FAQ
      | TRANSLATE
      | CONTRIBUTE
      | SCM
      .

    Inductive LinkT := Link {
      linkRole   : LinkRoleT;
      linkTarget : string
    }.

    Inductive VendorNameT :=
      VendorName : forall (s : string),
        matches s (regex "[a-zA-Z][A-Za-z0-9_-]{0,128}")
          -> VendorNameT.

    Definition VendorIDT :=
      lanarkDottedString.

    Inductive VendorT := Vendor {
      vendorId   : VendorIDT;
      vendorName : VendorNameT
    }.

    Inductive VersionNumberT := VersionNumber {
      major     : nat;
      minor     : nat;
      patch     : nat;
      qualifier : option string
    }.

    Inductive VersionDateT :=
      VersionDate : forall (s : string),
        matches s (regex "[0-9]{4}-[0-9]{2}-[0-9]{2}")
          -> VersionDateT.

    Inductive VersionT := Version {
      versionNumber : VersionNumberT;
      versionDate   : VersionDateT
    }.

    Definition ParagraphT :=
      string.

    Definition FeatureT :=
      string.

    Inductive LongDescriptionT := LongDescription {
      descriptionLanguage : LanguageT;
      descriptions        : list ParagraphT;
      features            : list FeatureT
    }.

    Inductive FlatpakRuntimeRoleT :=
      | SDK
      | PLATFORM
      .

    Definition FlatpakPermissionT :=
      string.

    Inductive FlatpakRuntimeT := FlatpakRuntime {
      flatpakRuntimeName    : string;
      flatpakRuntimeVersion : string;
      flatpakRuntimeRole    : FlatpakRuntimeRoleT
    }.

    Inductive FlatpakT := Flatpak {
      flatpakPermissions : list FlatpakPermissionT;
      flatpakRuntimes    : list FlatpakRuntimeT
    }.

    Definition PackageNameT :=
      lanarkDottedString.

    Inductive ShortNameT :=
      ShortName : forall (s : string),
        matches s (regex "[a-z][a-z0-9_-]{0,128}")
          -> ShortNameT.

    Definition HumanNameT :=
      string.

    Inductive NamesT := Names {
      namePackage : PackageNameT;
      nameShort   : ShortNameT;
      nameHuman   : HumanNameT
    }.

    Inductive MetadataT := Metadata {
      metaApplicationKind  : ApplicationKindT;
      metaCategories       : list CategoryT;
      metaCopying          : CopyingT;
      metaDescription      : DescriptionT;
      metaFlatpak          : FlatpakT;
      metaJavaInfo         : JavaInfoT;
      metaLinks            : list LinkT;
      metaLongDescriptions : LanguageMaps.t LongDescriptionT;
      metaNames            : NamesT;
      metaVendor           : VendorT;
      metaVersion          : VersionT
    }.

    Definition HashAlgorithmT :=
      string.

    Inductive HashValueT :=
      HashValue : forall (s : string),
        matches s (regex "[a-f0-9]{2,256}")
          -> HashValueT.

    Inductive HashT := Hash {
      hashAlgorithm : HashAlgorithmT;
      hashValue     : HashValueT
    }.

    Inductive ArchitectureNameT :=
      ArchitectureName : forall (s : string),
        matches s (regex "[a-z][a-z0-9_-]{0,32}")
          -> ArchitectureNameT.

    Inductive OperatingSystemNameT :=
      OperatingSystemName : forall (s : string),
        matches s (regex "[a-z][a-z0-9_-]{0,32}")
          -> OperatingSystemNameT.

    Inductive PlatformT := Platform {
      platformArch : ArchitectureNameT;
      platformOS   : OperatingSystemNameT
    }.

    (** A function that produces an uppercase version of the given string. *)
    Parameter uppercaseOf : string -> string.

    Definition uppercaseSame (s t : string) :=
      uppercaseOf s = uppercaseOf t.

    Inductive FileNameT :=
      FileName : forall (s : string),
        matches s (regex "([\p{L}\p{N}_\-.+]+)(/[\p{L}\p{N}_\-.+]+)*")
          -> FileNameT.

    (** A proposition that states that two file names are the same if their
        uppercase transformations are the same. *)
    Definition fileNamesSame (s t : FileNameT) :=
      match s, t with
      | FileName fs _, FileName ft _ => uppercaseSame fs ft
      end.

    Inductive ResourceRoleT :=
      | BOM
      | LICENSE
      | ICO_WINDOWS
      | ICON_16
      | ICON_24
      | ICON_32
      | ICON_48
      | ICON_64
      | ICON_128
      | ICON_256
      | ICON_512
      | ICON_SVG
      | SCREENSHOT
      .

    Definition CaptionT :=
      TranslatedTextT.

    Inductive ModuleT :=
      Module : FileNameT -> HashT -> ModuleT.

    Inductive PlatformModuleT :=
      PlatformModule : FileNameT -> HashT -> PlatformT -> PlatformModuleT.

    Inductive ResourceT :=
      Resource : FileNameT -> HashT -> ResourceRoleT -> CaptionT -> ResourceT.

    Inductive ItemT :=
      | ItemModule         : ModuleT         -> ItemT
      | ItemPlatformModule : PlatformModuleT -> ItemT
      | ItemResource       : ResourceT       -> ItemT
      .

    Definition itemFileName (i : ItemT) : FileNameT :=
      match i with
      | ItemModule         (Module f _)           => f
      | ItemPlatformModule (PlatformModule f _ _) => f
      | ItemResource       (Resource f _ _ _)     => f
      end.

    Definition itemHash (i : ItemT) : HashT :=
      match i with
      | ItemModule         (Module _ h)           => h
      | ItemPlatformModule (PlatformModule _ h _) => h
      | ItemResource       (Resource _ h _ _)     => h
      end.

    Inductive ManifestT := Manifest {
      manifestItems : list ItemT
    }.

    Definition manifesItemsFilenamesUnique :=
      forall (m : ManifestT),
        forall (i0 : ItemT),
          In i0 (manifestItems m)
            -> ~(exists i1 : ItemT,
                   (In i1 (manifestItems m))
                /\ (i0 <> i1)
                /\ (fileNamesSame (itemFileName i0) (itemFileName i1))).

## Footnotes

1 | Vendor names are used in some native packaging systems as installation directories and are therefore required to be filesystem-safe. References to this footnote: 1
2 | Short names are used in some native packaging systems as executable names and are therefore required to be filesystem-safe. References to this footnote: 1
3 | Many hardware architectures have different names referring to the same thing. For example, 64-bit x86 hardware is often referred to as amd64, x64, x86_64, etc. References to this footnote: 1

6.5. com.io7m.montarre.shell
Previous
Front Matter
Up
Front Matter
Next
io7m | single-page | multi-page | epub | Montarre User Manual 0.0.5