<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<pre>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.
</pre>
<pre>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 <a class="moz-txt-link-abbreviated" href="mailto:Vincent.Jackson@data61.csiro.au">Vincent.Jackson@data61.csiro.au</a>
1466 UNSW Sydney, NSW, Australia
<a class="moz-txt-link-abbreviated" href="http://www.data61.csiro.au">www.data61.csiro.au</a></pre>
</body>
</html>