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 [email protected]<mailto:[email protected]>
1466 UNSW Sydney, NSW, Australia
www.data61.csiro.au<http://www.data61.csiro.au>
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
