[isabelle-dev] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken

[Dmitriy Traytel]

Hi all,

thanks for pointing this out, Lars. And thanks for looking at the sources, Jasmin.

The problem seems to only show up when the declaration in question is inside of a class context. Here is a reduced version that does not involve primrec at all.

context linorder begin

context fixes b :: nat begin

definition c where "c = b"

end

end

@Makarius: What is the rationale behind disallowing the definition of c? Or is this not an expected behavior?

Dmitriy

> On 31 May 2018, at 11:17, Blanchette, J.C. <j.c.blanchette at vu.nl> wrote:
> 
> Hi Lars,
> 
> Thanks for the heads-up. Makarius's change e0cd57aeb60c is clearly the immediate source of the problem, but the more profound cause seems to be some nonstandard handling of variables. The "illegal fixed variable" in question, "s1", seems to originate from line 397 in "bnf_fp_n2m.ML":
> 
>      |> Variable.add_fixes (mk_names n "s")
> 
> Dmitriy, since this is your code, could you take a look at it? The line in question seems to have been added as part of an optimization you did in 2016 (see 8053ef5a0174).
> 
> Cheers,
> 
> Jasmin
> 
>> On 31. May 2018, at 10:28, Lars Hupel <hupel at in.tum.de> wrote:
>> 
>> since approximately Isabelle/e0cd57aeb60c (~1 week):
>> 
>> *** Malformed global fact
>> "Misc_N2M.linorder_class.f1_t.n2m_t_ctor_fold_dict"
>> *** Illegal fixed variable: "s1"
>> *** At command "primrec" (line 164 of
>> "~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy")
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>