Re: [isabelle] Packaging for distros? (Ubuntu/Debian/Fedora?)

On Sun, Nov 28, 2010 at 05:04:53PM +0100, Makarius wrote:
> On Sun, 28 Nov 2010, Ian Lynagh wrote:
>> * It's a lot easier to "apt-get install isabelle" than it is to find
>>  where to download it, download it, work out how to install it (even if
>>  that does turn out to be "just untar it"), add it to my path, etc
> So which version of Isabelle is the "isabelle" package?

One that works.

> You do need to be able to use several Isabelle versions at the same
> time in parallel.

Oh no I don't.

Now a power user's needs might not be served by the version in their
distro. They might need to use a recent development version, for
example. But new users have much simpler needs.

In fact, I started using coq trunk several months before downloading
Isabelle too, having started using the packaged version and then finding
I wanted some recent new features and bug fixes.

Something else I should have mentioned: I am reluctant to start writing
proofs with Isabelle that I ultimately want to share, because I know
that the people I want to share them with are much less likely to be
bother if the barrier to getting started is higher than "apt-get install
isabelle; isabelle myProof".

>> * I can be sure that packaged software is actually going to work on my
>>  machine
> This is simply not the case.

s/sure/more confident/

> Many Debian packages are broken, like the  
> jEdit one I mentioned.  Once I wanted to give Axiom a quick try, and its  
> Debian/Ubuntu package was really bad, so I did a quick compile from  
> sources again at it just worked out of the box.

I've never tried either of those, but broadly speaking my machine is the
same as the package maintainers, and it presumably works for the
maintainer, so it's likely to work for me.

I'm far more likely to have problems with a binary compiled on some
version of RedHat, when I try to use it on some version of Debian.
Or trying to compile some software on Linux when the maintainer uses

>> * Packaged software is more likely to "fit in" with the rest of the
>>  system, e.g. docs where I expect them
> Isabelle expects its documentation in a certain place, but not where  
> Debian has it.

Then an Isabelle package might move the docs to where they should be on
Debian systems, and update Isabelle accordingly. Perhaps adding a
configure flag so the location is configurable.

Or alternatively, it might put a symlink from one place to the other.

Or it might be as simple as a README (in the normal place) explaining
how to find the documentation. It depends what fits the package best.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.