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.
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and