I've removed the two rules from continuous_intros as of 1254f3e57fed.
Manuel
On 07/09/2018 14:56, Makarius wrote:
> On 02/09/18 16:00, Manuel Eberl wrote:
>> Okay I did some more experiments and I was now, interestingly enough,
>> completely unable to reproduce the situation where Green
On 02/09/18 16:00, Manuel Eberl wrote:
> Okay I did some more experiments and I was now, interestingly enough,
> completely unable to reproduce the situation where Green /didn't/
> timeout. So I have no idea what was going on there; perhaps I made a
> mistake in testing it. I don't know.
>
> It
This trace doesn’t tell us much because it’s only blast’s internal search.
Looks like every “continuous_on” goal is immediately solved. But after this
search exits, the reconstructed Isabelle proof will fail. Blast will re-enter
but it will only find these unsound proofs, and probably won’t
Okay I did some more experiments and I was now, interestingly enough,
completely unable to reproduce the situation where Green /didn't/
timeout. So I have no idea what was going on there; perhaps I made a
mistake in testing it. I don't know.
It might be wise to remove "continuous_on_discrete"
It’s important to understand that blast knows nothing about type classes. This
isn’t a problem for rules like order_trans, where the type class constraint
would be satisfied in most cases. But it’s fatal for continuous_on_discrete: it
will succeed in all cases, but if the type class constraint
On 01/09/18 14:39, Manuel Eberl wrote:
>> This thread consists of two sub-threads. The hardware / OS question
>> still needs to be sorted out: it might be something with Arch Linux.
>
> I don't really have much of an opportunity to test this on other systems
> atm, but I'll see what I can do.
>
> This thread consists of two sub-threads. The hardware / OS question
> still needs to be sorted out: it might be something with Arch Linux.
I don't really have much of an opportunity to test this on other systems
atm, but I'll see what I can do.
> Apart from that, my reading of blast.ML is that
This thread consists of two sub-threads. The hardware / OS question
still needs to be sorted out: it might be something with Arch Linux.
Apart from that, my reading of blast.ML is that the "continuous_on" rule
is applied in the search independently of its fine-grained type
information. Is that
Surely the main issue that blast somehow behaves differently depending upon
which machine it’s running on?
Larry
> On 31 Aug 2018, at 22:35, Makarius wrote:
>
> On 31/08/18 22:00, Manuel Eberl wrote:
>> That's interesting. I suspected one of the "continuous_on" rules would
>> be the cause. In
On 31/08/18 22:00, Manuel Eberl wrote:
> That's interesting. I suspected one of the "continuous_on" rules would
> be the cause. In any case, I don't know how the unification works
> exactly w.r.t. sorts, but the "continuous_on_discrete" rule does not
> apply to this goal at all due to its
It works on both my work laptop and my private desktop PC.
The work laptop is an Intel i7 something (I cannot recall the exact
model off the top of my head) and the desktop is an AMD Ryzen 1800X.
Both run with an up-to-date Arch Linux.
At least on the desktop, I tried it with both the 32 and 64
On 31/08/18 22:00, Manuel Eberl wrote:
>
> What puzzles me the most is the fact that this behaviour seems to depend
> on the underlying hardware, and it appears to be 100% reproducible on
> machines where it does happen. If this is a race condition, it must be
> one of the strangest one I have
That's interesting. I suspected one of the "continuous_on" rules would
be the cause. In any case, I don't know how the unification works
exactly w.r.t. sorts, but the "continuous_on_discrete" rule does not
apply to this goal at all due to its restrictive type class constraint.
What puzzles me the
On 31/08/18 15:06, Manuel Eberl wrote:
> Update: I pushed another changeset and now everything is green again (if
> you excuse the pun).
>
> I tracked the problem to a diverging invocation of "blast":
>
Update: I pushed another changeset and now everything is green again (if
you excuse the pun).
I tracked the problem to a diverging invocation of "blast":
15 matches
Mail list logo
