coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] performance question: replace autorewrite by reflection?

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] performance question: replace autorewrite by reflection?
Date: Wed, 29 Jul 2020 19:13:44 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f174.google.com
Ironport-phdr: 9a23:0tMpahzAnl4ih3PXCy+O+j09IxM/srCxBDY+r6Qd2uoVIJqq85mqBkHD//Il1AaPAdyFrawZwLOH+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhJiTanYL5/LBq6oRjVu8ILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8qFmQwLqhigaLT406G/ZhMxugqxGoxyvoBNwzJLbboyOKPpzfLnQcc8ASGZdQMpcUTFKDIOmb4sICuoMJehUr4v6p1sIrBu+BhejBOfxxTBWnXL20qg63P4gEQHCxgAvA9UOsHHaoN7oM6oSU+e1zK/JzTXAcfxW3Sny55bTfxAupPGDR7Nwcc7LxUYzEAPFi0ydpIr4NDyayuoDqXKU7/Z8Ve2xkW4nrRl8riWvy8kshYTEmJ4Zx0zE+Ch7zos4OdK1RFJ7bNK5HpVcqyWXOop2TM4hXWxkpDo3x6AYtZO5YCUH1Zoqyh7RZfGBboOG4QrjWf6PLTtkgH9pYrGyihao/US9y+DwStO43EtIoydKitXAqHEA2wDO5sWCV/dw+luu1DOA2g3S9u1IPUU5mbfHJ5E8x7M9koYcvlnMEyLzgkr2gqGWe0Aq+ue26unof7DrqYGAOINolg3zNLkllNalDuQiKAcOWnCW+eSi273n+k30WLBKgec3kqndqZzaPNgbqrOgDw9bz4ou6RmyAy2p0NQfmnkHI1ZFdwydg4f1PFHOJej0Dfa5g1uyjDdm3+7KMqHlD5nXLXXOkK3tcat85kJA0gY/0NJS6p1MBrEEOv3zW0vxtNLCDh8+Ngy52+TnCNJ71oMfWmKAHKuZP73MvlKT6eIvJvODZI4RuDrnN/cl4PvugWcjmVABZampwYcXaHegE/t6JEWZeGPgjcsFEWcXpQUzV/fqiV2HUT5LfXm+RaM85jchCIKnF4jPXI6tgKbSlBu8S5ZRfyVNDk2GWSPjcJzBUPMRYgqTJNVgm3oKT+7yZZUm0ETktgj8yrlqKufZ0iIdvJPnktNy4qebwRM18z13AsCQ3kmCSmh1miUDQDpgj/M3mlB01lrWifswuPdfD9EGv6oUADd/DobVyqlBM/63Wg/FeY3XGlOvQ9HjGC1oC9xonINIbEF6FNGvyBvE2njyWu5Hp/mwHJUxt5nk8T30Lsd5xWzB0fB43VYjS8pLc2ahg/wmrlSBN8vyi0yc0p2SW+EExieUrTWMyGOPuAdTVwsiCag=

Using Ltac profiling, it looks like about 40% of time spent in one
project I have is within autorewrite, the remainder primarily doing
proof search. The particular autorewrite hint dbs are not large (10 or
so rules each, one has only 3 rules) and the addition of rules ends
before the hint dbs are used. In such cases, would it be advantageous to
create a reflective procedure to replace use of autorewrite by a
particular hint db? Or is this unlikely to improve performance,
considering that autorewrite is already optimized (presumably)? I do
not beleive that Qeds are significantly time consuming in this project,
so I don't think shrinking the proof terms will have much benefit.

[Coq-Club] performance question: replace autorewrite by reflection?, jonikelee AT gmail.com, 07/30/2020
- Re: [Coq-Club] performance question: replace autorewrite by reflection?, Jason Gross, 07/30/2020
  - Re: [Coq-Club] performance question: replace autorewrite by reflection?, jonikelee AT gmail.com, 07/30/2020
  - Re: [Coq-Club] performance question: replace autorewrite by reflection?, Bas Spitters, 07/31/2020