What are the drawbacks of using the development version of Isabelle?

Question

This question is related to my last question.

In the answer to my question there is the statement that "it is in general not a good idea to use the repository version for your work".

So then my question is: what are the most significant drawbacks of using the development version from the mecurial repository?

I also stated the resons why I decided to use the development version:

My experience is that Isabelle2013-2 is simply completely unusable. I get very frustrated, this is not fun. It is slow and crashed too often. With the dev version typing feels again normal, not slightly delayed. Sledgehammer is greatly improved again, it finds proofs faster and the metis proofs are faster too that it generates. I don't mind being part of the development process. Wither other theorem provers like Agda, users are advised to use the development version too.

NOTE: Researchers in Munich explicitly told me that using the development version is a valuable alternative if the last stable version is older. Now it depends what older means, but three months old can be considered "old". For this reason, I would like to know the specific drawbacks (the most important aspects only) regarding Isabelle.

For instance, I think that a false lemma cannot be proven correct even in the development version, but would to like to know if it were the case. (In general, as a CS researcher I know the drawbacks are of using a development version of a software tool.)

Answer 1

In any way, you should have the same confidence in the development version than in the stable as long as the kernel and the logic's axioms have not been changed -- which is highly likely.

However, the tools -- including the definitional packages like function or datatypes, the proof methods like simp or auto and the framework components like locales and classes -- could have been modified such that they could fail more often, be slower or do things differently.

If such problems appear, there is a high probability that they would get corrected soon, but you would then have to update your repository, possibly update all your work, sometimes non trivially, while not being assured that other problems have not appeared and that the modications will remain until the next stable version.

Chances are that everything go well in the development version, but there can be sometimes problems or big reforms that could force you to change all your theories which is sometimes not an option. It can also be more difficult to get help, as you have seen in your last question.

Answer 2

There is a general misunderstanding here what a proper software release actually is, compared to ongoing changes in the development repository.

You will surely figure this out yourself, now that we are a few months past the latest release and many new things coming it at a high rate, until it will stabilize and converge again for the next release in summer 2014.