author  wenzelm 
Tue, 16 Jan 2018 09:58:17 +0100  
changeset 67445  4311845b0412 
parent 50529  b2aa899b3f2d 
child 68649  f849fc1cb65e 
permissions  rwrr 
50529  1 
Some notes on maintaining the Isabelle component repository at TUM 
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/screwdriver3.14.tar.gz 
2c7479865e07
some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff
changeset

8 
$ install /home/isabelle/contrib/screwdriver3.14/ 
2c7479865e07
some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff
changeset

9 
$ edit Admin/components/main: screwdriver3.14 
50528  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 reused. If some component needs to be 
2c7479865e07
some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff
changeset

20 
repackaged, 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 
screwdriver3.14 #default packaging/publishing, no index 
2c7479865e07
some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff
changeset

24 
screwdriver3.141 #another refinement of the same 
2c7479865e07
some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff
changeset

25 
screwdriver3.142 #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 worldreadable. 
2c7479865e07
some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff
changeset

46 

50527  47 
The file Admin/components/components.sha1 contains SHA1 identifiers 
48 
within the Isabelle repository, for integrity checking of the archives 

50528  49 
that are exposed to the public filesystem. The components_checksum 
50 
tool helps to update these hashkeys wrt. the information within the 

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. 