[isabelle-dev] Notes and updates on Isabelle/ML

[Jasmin Christian Blanchette]

Am 01.07.2014 um 19:45 schrieb Makarius <makarius at sketis.net>:

>  * src/HOL/Tools/ATP/atp_problem_generate.ML
> 
>    Two occurrences that are not immediately clear.  Looks like plain
>    structural equality could do the job.

Right. This looks like very minor optimizations. I'm taking them out (pushed to testboard already).

>  * src/HOL/Tools/BNF/bnf_def.ML
> 
>    fun maybe_restore lthy_old lthy =
>      lthy |> not (pointer_eq (lthy_old, lthy)) ? Local_Theory.restore;
> 
>    This looks odd.  The normal idiom is to maintain an option value, to
>    say when a value remains explicitly unchanged (NONE).  If this is too
>    awkward here,

It is a bit awkward indeed.

> one could try comparing the background theories via
>    Theory.eq_thy instead (which is strictly speaking just another
>    approximation, but a deterministic one).  One could also try to
>    express the idea behind the uses of maybe_restore differently.

I'll try something like this first.

>  * Metis has various optimizations using the "portable" alias
>    pointerEqual. Hard to say if there are potential problems coming from
>    it.  A quick experiment with an always false predicate (which is a
>    correct approximation) makes metis very slow, but in most situations
>    it still terminates.  (Shall we forward this to Joe Hurd?  For the
>    Isabelle release, Metis is better left alone, though.)

From looking at the code, it looks to me like he's using "pointerEqual" only as an overapproximation for equality, to speed up some data structure operations. These uses do not worry me at all, and your experiments just confirm what the code already strongly suggests.

Jasmin