| author | wenzelm | 
| Mon, 23 Dec 2019 22:08:20 +0100 | |
| changeset 71341 | dfc52eb97ff4 | 
| parent 71335 | 2afdd24ff707 | 
| child 76153 | bf9f2f4069b9 | 
| permissions | -rw-r--r-- | 
| 69429 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 1 | Notes on maintaining the Isabelle component repository at TUM | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
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 | |
| 69429 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 7 | * ensure that Isabelle/Scala/SSH can connect to the host specified via | 
| 71335 | 8 | system option `isabelle_components_server`; this may require to install | 
| 69429 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 9 | an unencrypted ssh host key as follows: | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 10 | |
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 11 | $ ssh-keyscan -t rsa lxbroy10.informatik.tu-muenchen.de >> ~/.ssh/known_hosts | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 12 | |
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 13 | * local setup (and test) of component directory, e.g. in | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 14 | |
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 15 | screwdriver-3.14/ | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 16 | |
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 17 | * packaging (with associated SHA1 digest), e.g. | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 18 | |
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 19 | $ isabelle build_components screwdriver-3.14 | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 20 | |
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 21 | * publishing, e.g. | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 22 | |
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 23 | $ isabelle build_components -P screwdriver-3.14.tar.gz | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 24 | |
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 25 | * manual editing of Admin/components/main: screwdriver-3.14 | 
| 50332 
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 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 28 | Unique names | 
| 
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 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 31 | 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 | 32 | 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 | 33 | 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 | 34 | like this: | 
| 
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 | screwdriver-3.14 #default packaging/publishing, no index | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 37 | screwdriver-3.14-1 #another refinement of the same | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 38 | screwdriver-3.14-2 #yet another refinement of the same | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 39 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 40 | 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 | 41 | 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 | 42 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 43 | Components are registered in Admin/components/main (or similar) for | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 44 | use of that particular Isabelle repository version, subject to regular | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 45 | Mercurial history. This allows to bisect Isabelle versions with full | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 46 | record of the required components for testing. | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 47 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 48 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 49 | Authentic archives | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 50 | ------------------ | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 51 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 52 | Isabelle components are managed as authentic .tar.gz archives in | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 53 | /home/isabelle/components from where they are made publicly available | 
| 68649 | 54 | on https://isabelle.in.tum.de/components/. | 
| 50332 
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 | 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 | 57 | 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 | 58 | regular components should be world-readable. | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 59 | |
| 71335 | 60 | The file `Admin/components/components.sha1` contains SHA1 identifiers | 
| 50527 | 61 | within the Isabelle repository, for integrity checking of the archives | 
| 69429 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 62 | that are exposed to the public file-system. The command-line tool | 
| 71335 | 63 | `isabelle build_components` maintains these hash-keys automatically. | 
| 50332 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 64 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 65 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 66 | Unpacked copy | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 67 | ------------- | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 68 | |
| 71335 | 69 | A second unpacked copy is provided in `/home/isabelle/contrib/`. This allows | 
| 69429 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 70 | users and administrative services within the TUM network to activate arbitrary | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 71 | snapshots of the repository with all standard components being available, | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 72 | without extra copying or unpacking of the authentic archives. The | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 73 | isabelle_cronjob does this routinely: it will break if the unpacked version is | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 74 | omitted. | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 75 | |
| 71335 | 76 | The command-line tool `isabelle build_components -P` takes care of uploading | 
| 69429 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 77 | the .tar.gz archive and unpacking it, unless it is a special component (e.g. | 
| 
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
 wenzelm parents: 
68649diff
changeset | 78 | for multiplatform application bundling). |