*To*: Lars Hupel <hupel at in.tum.de>*Subject*: Re: [isabelle] Failing afp-2015 build*From*: Makarius <makarius at sketis.net>*Date*: Wed, 18 Nov 2015 14:39:11 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk, Peter Gammie <peteg42 at gmail.com>*In-reply-to*: <564B2185.30105@in.tum.de>*References*: <f43062eaa295f6327e5913b38d975047-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1UENGV1gNQVZwH1dRXzBeRUEFXV1bSFtS-webmailer1@server05.webmailer.hosteurope.de> <6b7aa3e1e6df1ea8242ffac29182a99a-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1UENGV1gNQVZwH1dRXzBeRUEFXV1fRlxS-webmailer1@server05.webmailer.hosteurope.de> <1447320348.29121.13.camel@lapnipkow10> <alpine.LNX.2.00.1511121435130.31734@lxbroy10.informatik.tu-muenchen.de> <5644A22F.9060709@in.tum.de> <B5A095F6-34EB-4B7C-994C-7EDC161851F5@gmail.com> <564B2185.30105@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 17 Nov 2015, Lars Hupel wrote:

(What is the point of running single-threaded these days?)I only discovered that as part of my investigations into how to reliablybuild the AFP. There are essentially two axes for parallelism: Internalto a session (multi-threaded, e.g. parallel proofs, parallel theories)and between sessions (multi-process, i.e. independent AFP sessions canbe run in parallel).

Gerwin and I suspect that it would be most efficient to exploit thelatter on the cost of the former, since the AFP dependency graph isquite sparse.

Makarius

**References**:**[isabelle] Failing afp-2015 build***From:*Lars Hupel

**Re: [isabelle] Failing afp-2015 build***From:*Lars Hupel

**Re: [isabelle] Failing afp-2015 build***From:*Peter Lammich

**Re: [isabelle] Failing afp-2015 build***From:*Makarius

**Re: [isabelle] Failing afp-2015 build***From:*Lars Hupel

**Re: [isabelle] Failing afp-2015 build***From:*Lars Hupel

- Previous by Date: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Next by Date: Re: [isabelle] Proving termination of a recursive function
- Previous by Thread: Re: [isabelle] Failing afp-2015 build
- Next by Thread: Re: [isabelle] Failing afp-2015 build
- Cl-isabelle-users November 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list