*To*: "He, Shuhan" <13061136 at buaa.edu.cn>*Subject*: Re: [isabelle] Datatype definition can be slow*From*: Dmitriy Traytel <traytel at di.ku.dk>*Date*: Tue, 13 Apr 2021 11:43:53 +0000*Accept-language*: en-US, da-DK*Arc-authentication-results*: i=1; mx.microsoft.com 1; spf=pass (sender ip is 192.38.125.140) smtp.rcpttodomain=buaa.edu.cn smtp.mailfrom=di.ku.dk; dmarc=pass (p=none sp=none pct=100) action=none header.from=di.ku.dk; dkim=none (message not signed); arc=none*Arc-message-signature*: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=PvvBNqQ/Nq/1uKP+DezEy/4D+O4j0OrM8J/ZsKZiE+E=; b=cBXnbxEjcxXHD9X3qGyIBdTpdv9t7jpB2nk2qaPntP1rL9R+tRJVS5nk/NAkkrVbOvrrP9B0hNBlidV3InSFcLKbcftZgw7g3mxk1lKvjvEDH0G7/WSKyOCwMmyXNeoJD2L1PScMuPLX0qg9WJ/nLv6x6d6V+1s+xnqeD9Ydk5iPwH9b/wybJAgBfTq0J4vrXlg+Fnk+/HH89snvAf4dp1YumQG4Tm8F5RxaIpu79XFi9kj2kBC8C2lb2jTkMBe2EzM33NZp8qXU8NTDDaZszsz5snTSGPymLSBlzDZQGq5IoabW8pvLmhrsHEdEWe0LbXt9g8dONFl3752gSHKdiw==*Arc-seal*: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=Djj8iJRZ6T+EAOhfNEMWkONEAFlZzEAtEAgMow5AP+0RBMtGyjwtSsmwU5B8J9XPtOxk05YGXdnmsc6Da5BlVWvZjVRRoo8Q0S/g6IEM+PrdPsYRXquNtoKBu+RQ5wrsjG88rdNjz5cVHt803O+khNFTGHGZrIzOtVtb3CaJL5BBuBv99rshPtcOs/ounPQtMISusMhwOfVp+bIbEzZwWwRx4WSgUwB2n2I1AhdbqOTMfUNHwMF1dD4luPatOm08KyNdAKV8PSUSKG804QDYZTlwTAOfl16UbTsbG4M+7T+hWHhm9RUggx+TaF/nnJ+BKwp8+1o3Gt9d/Dqkmdi7jw==*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <a0701ab.2b705.178c68638b8.Coremail.13061136@buaa.edu.cn>*References*: <a0701ab.2b705.178c68638b8.Coremail.13061136@buaa.edu.cn>*Thread-index*: AQHXME6USuEHxbShiUWe2GMCfoKBq6qyMmqA*Thread-topic*: [isabelle] Datatype definition can be slow

Hi Shuhan, There are a couple of knobs one can turn. For example, a definition like datatype t = A00 | A01 | A02 | A03 | A04 | A05 | A06 | A07 | A08 | A09 | A10 | A11 | A12 | A13 | A14 | A15 | A16 | A17 | A18 | A19 | A20 | A21 | A22 | A23 | A24 | A25 | A26 | A27 | A28 | A29 | A30 | A31 | A32 | A33 | A34 | A35 | A36 | A37 | A38 | A39 | A40 | A41 | A42 | A43 | A44 | A45 | A46 | A47 | A48 | A49 takes something like 30 seconds on my machine. In contrast, datatype (plugins only: ) t = A00 | A01 | A02 | A03 | A04 | A05 | A06 | A07 | A08 | A09 | A10 | A11 | A12 | A13 | A14 | A15 | A16 | A17 | A18 | A19 | A20 | A21 | A22 | A23 | A24 | A25 | A26 | A27 | A28 | A29 | A30 | A31 | A32 | A33 | A34 | A35 | A36 | A37 | A38 | A39 | A40 | A41 | A42 | A43 | A44 | A45 | A46 | A47 | A48 | A49 takes only something like 3 seconds. So the actual datatype constructions (including the simplification theorems which are indeed quadratic in the number of constructors) is reasonably fast. The plugins (e.g., size function, code generation setup, transfer theorems, etc.) that were disabled in the second definition provide many useful things too, but have their cost for large datatypes. It depends on the actual application which plugins are actually needed. It would help to see your specific example and your requirements (what do you want to do with the type?) to provide further hints. Dmitriy > On 12 Apr 2021, at 16:39, He, Shuhan <13061136 at buaa.edu.cn> wrote: > > Hello fellow researchers, > > I'm working on a translator from an ML-like language to HOL, and I'm having a > difficulty with translation of inductive datatype definitions. > > Datatype definition in Isabelle can be quite slow (at least compared to HOL4) > when the number of constructors goes up (say a few dozen), and time consumption > seems to be super-linear in the number of constructors. This has a significant > impact on usability since some programs in the source language have very large > datatypes, and it's not always feasible to modify the source programs to make > them friendlier to Isabelle. Is the poor performance caused by inherent > limitation of the theoretical foundation of the datatype definition package, or > suboptimality of implementation of the package? Also, does the package provide > a "quick mode" that skips the slow part of the definition process, while > retaining the essential theorems about the datatype being defined? > > I once tried to poke into the implementation of the 'datatype' command to find > out what's slowing the thing down, but finally got lost in its sheer > complexity. The only potential culprit I found is the simplification theorems, > the number of which is quadratic in the number of constructors. > > It would be nice to have a datatype definition package without the > aforementioned drawback, but given the size and complexity of current > implementation, improving it seems extremely difficult. > > Your thoughts are greatly appreciated.

**Follow-Ups**:**Re: [isabelle] Datatype definition can be slow***From:*Manuel Eberl

**Re: [isabelle] Datatype definition can be slow***From:*He, Shuhan

**References**:**[isabelle] Datatype definition can be slow***From:*He, Shuhan

- Previous by Date: [isabelle] 7th International Workshop on Proof eXchange for Theorem Proving (PxTP) - Second CFP
- Next by Date: Re: [isabelle] Datatype definition can be slow
- Previous by Thread: [isabelle] Datatype definition can be slow
- Next by Thread: Re: [isabelle] Datatype definition can be slow
- Cl-isabelle-users April 2021 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