[isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS

[Florian Haftmann]

Hi all!

> The following is for my own home directory at TUM:
> 
>   .isabelle/etc/components ->
> /home/wenzelm/isabelle/repos/Admin/contributed_components
>   .isabelle/contrib -> /home/isabelle/contrib
> 
> This achieves the effect of versioned symlinks: the repository says
> which directories to take from the physical file-system.  This assumes
> that the component name-version scheme in the file-system is really
> authentic.  In the past we have occasionally updated components without
> bumping the version, but it might be not that critical after all.

this indeed works nice at TUM, but this requires that every developer
keep up-to-date his/her components on local machines for development,
and, as a prerequsite, to download them to his/her machine.  This first
step already is not clear, or how would you obtain a HOL-Light bundle
without access to TUM NFS!?

So, this is my idea:
a) There is a canonical place at TUM where developers place their
components.
b) This should then also include jedit_build.
c) This place is accessible by HTTP.
d) Developers maintain Admin/contributed_components accordingly.

This burdens each developer to maintain local components accordingly
(even things like the HOL-Light bundle which will rarely affect common
development), but having a common base of components among all
developers (including mira) should be worth the effort, in times where
integration is increasing in importance.

This can be supported by populating Admin/ further, e.g. moving

e) Admin/contributed_components ~> Admin/etc/components

and then including Admin as component in your ~/.isabelle/etc/settings;
the same would be done by mira.

This does not even require a contrib dir in the Isabelle repository.

Common favorites like

  if [[ -z "$ISABELLE_IDENTIFIER" ]]
  then
    ISABELLE_OUTPUT="$ISABELLE_HOME/heaps"
    ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
  fi

then could go to

f) Admin/etc/settings

providing more pre-configuration for developers.

It is good to have a description like
https://isabelle.in.tum.de/community/Working_with_the_repository_version_of_Isabelle
(again):

g) The results of this mail thread should go there.

Awaiting your response,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120530/40f1f83e/attachment.sig>