Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.



On Fri, 13 Dec 2013, Lawrence Paulson wrote:

I need to stress a basic fact: Flex-Flex constraints invariably involve function variables. This means that the proof involved an inference rule containing a function variable, such as imageI. It is worth attempting to identify which rule is to blame (the variable name may be a clue) and to supply a suitably instantiated instance of the rule to blast.

Larry

On 13 Dec 2013, at 12:24, Makarius <makarius at sketis.net> wrote:

On Wed, 11 Dec 2013, Makarius wrote:

Anyway, after heating my office with more CPU power (running Isabelle + AFP + IsaFoR a few times), I have the impression that there is nothing to see on this thread, and we can just move on. This means we can probably remove the extra clean-up step from blast in coming Isabelle versions.

Further explanations when the current build has terminated ...

There were various delays, failures, non-termination, but mostly due to other reasons. We have again a situation where AFP feels very "heavy" (even on 8 cores), and the many repository clones and branches sometimes cause confusion what needs to be tested.

Just for the record: there *is* something wrong with this experiment on AFP Collections and/or JinjaThreads, but I don't know yet what really happens. Total existence failure of the test environment ...

We should close this thread on isabelle-users for now, since David has his workaround already to get L4.verified running.

Further software archeology on isabelle-dev at some later point -- I am on travel next week.


	Makarius




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