Keep multiple versions parallel-installable in Debian?

[Achim D. Brucker]

Hi,

On Sat, Aug 16, 2008 at 07:50:43PM +0200, Lionel Elie Mamane wrote:
> Hi,
> 
> Do you think that for theorem provers, and for Isabelle in particular,
> we want to allow our users to have multiple versions installed in
> parallel? E.g. Isabelle2008 _and_ Isabelle2009? Sounds like a
> non-trivial amount of users would benefit from it. What do you think?

I think, it mainly depends on the user group we are targeting
at. Just a brief explanation for those under us that are not using 
theorem prover on a regular basis. Isabelle can be used in two ways:

1) it can be used for formalizing mathematical (i.e., logical)
   theories and proving properties over them in an high-level
   way. That means, writing theory files in the Isar language. 
   This is probably the usage most people have in mind when 
   thinking of an interactive theorem prover. 
2) it  can be used as a programming framework for developing 
   new logical tools, e.g., domain-specific interactive theorem
   provers like HOL-OCL or even test tools like HOL-TestGen. 
   This involves writing new functions in SML (but also writing
   Isar theories). 

I would assume, that most users are using Isabelle in the first My
Isabelle "career" started with Isabelle 98 and my experience is, that
porting "pure" theories is relatively easy and all necessary changes
are documented (i.e., see the NEWS file of the Isabelle distribution)
and sometimes even tool support is provided.  Thus, my assumption is
that the first class of users will usually switch to the latest
Isabelle version in a timely manner.

On the other hand, porting projects that are based on Isabelle as a
programming framework is more painful (e.g., the changes on the
programming API are usually not documented) and, therefore, takes a
lot of time. Personally, I currently use Isabelle 2008 and Isabelle
2005 on a regular basis and one project still uses Isabelle 2003...

As maintaining several Isabelle version (at least for a clearly
defined transitional period) shouldn't be to much work, I am in favor
(but I wouldn't fight for it) of preparing our package for multiple
versions of Isabelle. Of course, we should also provide an "empty"
isabelle package that always depends on the latest version of
Isabelle.

> That would entail renaming the package to isabelle-2008, and change
> the paths so that they don't conflict between versions. The same for
> Poly/ML, because old versions of Isabelle will require old versions of
> Poly/ML. We would also then, I suppose, add an isabelle package that
> would install symlinks in /usr/bin/ like:
> isabelle -> isabelle-2008

One could also port the old Isabelle version to the new SML system. At
least in the last 8 years this was quite easy (for both Poly/ML and
SML/NJ). Currently, I have Isabelle 2008 and 2005 running based on
Poly/ML 5.2.

Just as a side remark: On the long term, supporting several Isabelle
versions could also requiring supporting several versions of its user
interface (i.e., Proof General and whatever comes after it). The
current Proof General can be used with all Isabelle 200x versions. But
in the long term (could be already for Isabelle 2009) Proof General
will be replaced by something else and I think it is unlikely that
this successor will work with the older Isabelle releases.

The only point that I see against supporting old versions of Isabelle
is upstream: Usually, the Isabelle developers do not support old
versions longer then a few weeks after releasing a new one (even bugs
are often only fixed in the CVS version and not ported back to the
last stable release). Therefore, we should ensure that a user just
installing "isabelle" will get the latest version
available. Installing old versions should, somehow, not be encouraged
by us.


Achim