[isabelle] Performance regression in 2016-1 with character strings.



Hello Isabelle users, developers.

We've noticed a serious performance regression involving characters and 
strings in Isabelle-2016-1.

This can be demonstrated as follows:

lemma "''ab'' ~= ''ba''"
   using [[simp_trace]]
   by simp

In earlier Isabelle versions, it takes a few dozen steps to prove this 
rule. In 2016-1, the characters
are compared by expanding rule Char_eq_Char_iff which requires 
normalising "k mod 256" for
various k, which takes many many steps.

One workaround we tested is to adjust the simpset to ensure that the 
code rules nat_of_char_code
and integer_of_char_simps are used, which solves the problem.

The C typing framework used by the seL4 proofs, Cogent proofs, 
AutoCorres etc, uses strings to
encode field names and type identifiers. The impact of this change is 
big enough to explode the
time to parse seL4 into Isabelle by a factor of 4 or more. There are 
also some other string users
around.

We're sorry we didn't notice how significant the impact was until after 
the release.

For the moment we'll patch around this by adjusting the simpset at our 
end. The Isabelle version
should probably be adjusted as well though.

Cheers,
     Thomas.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.