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

[Jackson, Vincent (Data61, Kensington NSW)]

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.

Thanks,
  Vincent

--

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

template_end=\
'    @{thm list_all2_refl}\
  ]\
*}\
\
end'

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

echo $(
  printf "$template_start" "Thy1024";
  for j in $(seq 0 1024);
  do
    echo "    @{thm list_all2_refl},";
  done;
  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
www.data61.csiro.au<http://www.data61.csiro.au>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190415/e7c9408c/attachment.html>