[isabelle-dev] Antiquotation Parsing Time Increased between Isabelle 2017 and 2018

Jackson, Vincent (Data61, Kensington NSW) Vincent.Jackson at data61.csiro.au
Mon Apr 15 03:03:04 CEST 2019

Hello All,

I recently ran into a performance degradation when updating some proofs to Isabelle 2018.
These theory files involve a large number of anti-quotations in ML blocks.

In Isabelle 2017 a file with ~1000 thm antiquotations takes 3 seconds; in Isabelle 2018, 2 minutes and 39 seconds.

I have pinned down the source to this commit:
  d293958f9d use Poly/ML 5.7.1 test version as default;

If anyone knows what changed to cause this, I'd be interested to know.



A bash script to generate a file which exhibits the degradation:
'theory %s\
  imports Main\
begin ML {*\

'    @{thm list_all2_refl}\

echo "session Thy1024 = Main + theories Thy1024" >> ROOT

echo $(
  printf "$template_start" "Thy1024";
  for j in $(seq 0 1024);
    echo "    @{thm list_all2_refl},";
  printf "$template_end") | tr '\\' '\n' > Thy1024.thy


Vincent Jackson
Proof Engineer | Trustworthy Systems
CSIRO | Data61
E  Vincent.Jackson at data61.csiro.au<mailto:Vincent.Jackson at data61.csiro.au>
1466 UNSW Sydney, NSW, Australia
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190415/e7c9408c/attachment.html>

More information about the isabelle-dev mailing list