author  wenzelm 
Mon, 03 Dec 2012 20:43:40 +0100  
changeset 50332  2c7479865e07 
permissions  rwrr 
50332
2c7479865e07
some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff
changeset

1 
Some notes on the Isabelle component repository at TUM 
2c7479865e07
some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff
changeset

2 
====================================================== 
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 
2c7479865e07
some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff
changeset

10 
$ run Admin/component_repository/checksum u 
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 

2c7479865e07
some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff
changeset

47 
The file Admin/component_repository/contains SHA1 identifiers within 
2c7479865e07
some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff
changeset

48 
the Isabelle repository, for integrity checking of the archives that 
2c7479865e07
some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff
changeset

49 
are exposed to the public filesystem. The script 
2c7479865e07
some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff
changeset

50 
Admin/component_repository/checksum helps to update these hashkeys 
2c7479865e07
some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff
changeset

51 
wrt. the information within the Isabelle repository. 
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. 