Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

2018-09-01 Thread Lawrence Paulson
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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

2018-09-01 Thread Makarius
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. >

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

2018-09-01 Thread Manuel Eberl
> 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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

2018-09-01 Thread Makarius
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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

2018-09-01 Thread Lawrence Paulson
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