Tree [0b0f24] default Isabelle2012 / metadata /

Read Only access

File Date Author Commit
 README 2010-12-01 [817b5c] merged sitegen update from release branch
 entry.tpl 2010-07-02 kleing kleing [7cfccc] merged
 index.tpl 2012-05-11 [dcfc5e] merged
 metadata 2012-05-18 Christian Sternagel Christian Sternagel [a9160e] same abstract on website as in document
 release-dates 2011-10-10 kleing kleing [d31f0a] merged from release branch
 releases 2012-05-11 [dcfc5e] merged
 topics 2012-01-08 nipkow nipkow [81ac55] rearranged topics
 topics.tpl 2012-03-15 nipkow nipkow [35faf8] get rid of The in front of AFP

Read Me

Metadata format

We're using a simple INI-like format for configuration

  * File 'metadata'

    Master storage for entry metadata. Format:

    title = <title>
    author = <author1> [<<url1>>], <author2> ...
    date = <YYYY>-<MM>-<HH>
    topic = <topic>/<subtopic>/..., <topic2>/...
    base = <base-theory>
    abstract = <text>


    title = Formalizing the Logic-Automaton Connection
    author = Stefan Berghofer <>, Markus Reiter
    date = 2009-12-03
    topic = Computer Science/Automata, Logic
    base = HOL
    abstract = This abstract has
      multiple lines ...

    The section name (<short-name> in this terminology) must correspond to
    the folder name in 'thys' directory. This short name is used as entry
    identifier during the whole process.

    The key 'base' can be omitted. In this case, the script assumes 'HOL'.
    If the entry uses e. g. HOLCF, you have to specify that explicitly as
    this information is used to generate the links.

    Currently, only three levels of topics and subtopics are allowed, but
    you may specify as many topics as you wish. If multiple topics are
    specified, the entry will appear under each of them. Note that the
    short name must be the same as their name in the 'thys' folder. The topic
    must also appear in the 'topics' file (see below).

    For each author, you may provide an URI (either a web page or a mail
    address, the latter prepended with 'mailto:') in standard <protocol:uri>

    The section header and the keys must not contain leading whitespaces. When
    continuing a value on a second line, this and the following lines must be
    preceded by a whitespace. The date is the submission date of the entry.

    If you've chosen multiple topics, you can comma-separate them. The key
    'base' can be omitted if you simply use HOL (which is the default).
    If you want to have some additional text fields like 'Note' or 'Change
    history' below the 'Abstract' column, you can use the 'extra' facility:
     extra-<key> = <heading>: <text>
    where <key> denotes an identifier (most cases 0, 1, ...) unique for each
    entry. The particular <key> has no impact on output and is solely used for
    disambiguating multiple extra fields.
     extra-0 = Warning: Untested... 
     extra-1 = History: [2010-01-01] new year

    There is another special treatment at the moment: Some entries have a
    custom format, e. g. InformationFlowSlicing, which contains multiple
    proofs, or Valuation which doesn't contain a proof document. For these
    entries, no entry file should be generated, but they should be listed on
    index and topics page. These entries have another pair 'ignore = entry' in
    the metadata file which simply means 'don't generate template 'entry.tpl'
    for this entry'.

    For entries with a license other than BSD, you can add a line

	license = LGPL

    Only BSD and LGPL are supported.

  * File 'release-dates'
    To list the older releases, a mapping between date and Isabelle version
    is necessary.
    <isabelle-version> = <release-date>
    2003 = 2003-05-13
    2004 = 2004-04-19
    So, all tarballs between 2003-05-13 (inclusive) and 2004-04-19 (exclusive)
    will be treated as older release for 'Isabelle 2003'.
  * File 'releases'
    Contains a list of all released tarballs. The youngest release is always
    ignored, so don't forget to add new releases when a new Isabelle version
    has been added to the 'release-dates' file.

  * File 'topics'

    Each topic and its subtopics must go into there. The format looks like that
    (where '_' denotes exactly one space character):


    Only three levels of indentation are supported currently.

Metadata directory

The metadata file resides in this folder, additionally to the HTML template
files. Currently, the script supports generation of '*.shtml' files, if a
corresponding '*.tpl' file is located in the metadata folder. Each '*.tpl'
file should contain a line



which will be replaced by the output of a so-called generator function. The
appropriate function is inferred from the filename of the template and the
corresponding configuration in the script. Some generators (at the moment,
only for 'entry.tpl') require a parameter which denotes which subpart of the
page should be rendered. For available parameters, consult the comments in
the script.

In most cases, you don't have to change these generator lines.


When invoking without arguments, the following help is displayed:

  Usage: [--no-warn] [--debug] [--check=THYS_DIR | --dest=DEST_DIR] metadata-dir

The script requires one parameter to pass specifying the metadata folder.
Secondly, you must specify at least one action (--check or --dest)
(examples assume that you are in the root of the repository):


    If you specify the 'thys' folder, the script will perform a check whether
    the entries in the metadata file corresponds to the folders in the

      admin/ --check=thys metadata

    You might want to specify --no-warn when using --check if you're only
    interested in checking the rough structure of the metadata file.


    If you specify a destination folder, the script will look for templates in
    the metadata folder and generate a corresponding file in the destination

      admin/ --dest=/tmp/web metadata

You may wish to supply both --check and --dest.

The other parameters are optional. Provide --help to get an explanation.

    Disable warnings. The script will occasionally complain about 
    various things:
      * missing keys in metadata file
      * release of unknown entry
      * release matches no known Isabelle version 
        (i.e. release is 'too early')
      * unknown topic is used in metadata
    Enables debug output. Each generator will print its representation of 
    the data.