[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''"
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
We're sorry we didn't notice how significant the impact was until after
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and