Admin/components/README
author blanchet
Mon, 19 May 2014 23:43:53 +0200
changeset 57005 33f3d2ea803d
parent 50529 b2aa899b3f2d
child 68649 f849fc1cb65e
permissions -rw-r--r--
store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50529
b2aa899b3f2d clarified README;
wenzelm
parents: 50528
diff changeset
     1
Some notes on maintaining the Isabelle component repository at TUM
b2aa899b3f2d clarified README;
wenzelm
parents: 50528
diff changeset
     2
==================================================================
50332
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
     3
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
     4
Quick reference
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
     5
---------------
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
     6
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
     7
  $ install /home/isabelle/components/screwdriver-3.14.tar.gz
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
     8
  $ install /home/isabelle/contrib/screwdriver-3.14/
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
     9
  $ edit Admin/components/main: screwdriver-3.14
50528
c29af5ffe98a more formal components_checksum tool;
wenzelm
parents: 50527
diff changeset
    10
  $ isabelle components_checksum -u
50332
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    11
  $ hg diff
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    12
  $ hg commit
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    13
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    14
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    15
Unique names
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    16
------------
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    17
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    18
Component names are globally unique over time and space: names of
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    19
published components are never re-used.  If some component needs to be
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    20
re-packaged, extra indices may be added to the official version number
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    21
like this:
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    22
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    23
  screwdriver-3.14    #default packaging/publishing, no index
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    24
  screwdriver-3.14-1  #another refinement of the same
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    25
  screwdriver-3.14-2  #yet another refinement of the same
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    26
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    27
There is no standard format for the structure of component names: they
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    28
are compared for equality only, without any guess at an ordering.
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    29
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    30
Components are registered in Admin/components/main (or similar) for
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    31
use of that particular Isabelle repository version, subject to regular
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    32
Mercurial history.  This allows to bisect Isabelle versions with full
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    33
record of the required components for testing.
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    34
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    35
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    36
Authentic archives
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    37
------------------
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    38
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    39
Isabelle components are managed as authentic .tar.gz archives in
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    40
/home/isabelle/components from where they are made publicly available
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    41
on http://isabelle.in.tum.de/components/.
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    42
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    43
Visibility on the HTTP server depends on local Unix file permission:
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    44
nonfree components should omit "read" mode for the Unix group/other;
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    45
regular components should be world-readable.
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    46
50527
2f9b5b0e388d just one Admin/components/ directory;
wenzelm
parents: 50332
diff changeset
    47
The file Admin/components/components.sha1 contains SHA1 identifiers
2f9b5b0e388d just one Admin/components/ directory;
wenzelm
parents: 50332
diff changeset
    48
within the Isabelle repository, for integrity checking of the archives
50528
c29af5ffe98a more formal components_checksum tool;
wenzelm
parents: 50527
diff changeset
    49
that are exposed to the public file-system.  The components_checksum
c29af5ffe98a more formal components_checksum tool;
wenzelm
parents: 50527
diff changeset
    50
tool helps to update these hash-keys wrt. the information within the
c29af5ffe98a more formal components_checksum tool;
wenzelm
parents: 50527
diff changeset
    51
Isabelle repository.
50332
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    52
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    53
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    54
Unpacked copy
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    55
-------------
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    56
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    57
A second unpacked copy is provided in /home/isabelle/contrib/.  This
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    58
allows users within the TUM network to activate arbitrary snapshots of
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    59
the repository with all standard components being available, without
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    60
extra copying or unpacking of the authentic archives.  Testing
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    61
services like "isatest" and "mira" do this routinely, and will break
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    62
accordingly if this is omitted.