Re: [isabelle-dev] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken
Hi Makarius, > On 1 Jun 2018, at 23:32, Makarius wrote: > > On 01/06/18 10:35, Dmitriy Traytel wrote: >> 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 > > This is ultimately a problem of the class target in conjunction with the > unnamed local context. See now > > changeset: 68351:bcdc4c21ab1d > tag: tip > user:wenzelm > date:Fri Jun 01 22:01:43 2018 +0200 > files: src/Pure/Isar/class.ML > description: > varify frees, notably dangling_params (see also e0cd57aeb60c); Happy to see that this was not a problem in our codebase. >> @Makarius: What is the rationale behind disallowing the definition of c? > > The changeset explains it as follows: > > changeset: 68239:e0cd57aeb60c > user:wenzelm > date:Sun May 20 22:37:00 2018 +0200 > files: src/Pure/global_theory.ML > description: > more checks for global facts: disallow undeclared frees (as in > Export_Theory.export_fact); > > > At first I did not want to expose odd mixtures of free vs. schematic > variables to the world out there, and for global items we have a clear > understanding that fixed vs. schematic can always be flipped via > Logic.varify_global/unvarify_global and related operations. > > Moreover, the check was meant to tighten existing tools and local theory > targets, as we have seen here. In the process, I had to give up the full > rigour, though: a3bd410db5b2 allows mixed variable indexes. > > > Looking even more closely at global facts, there might be further > problems that are still undetected. In the next round I will experiment > with Thm.plain_prop_of to see if we can disallow hyps, shyps, tpairs. Thanks for the explanation. The context handling in the BNF packages has quite improved over the years thanks to the additional checks you introduce every now and then. Do not hesitate to tell us should you encounter further problems. Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken
On 01/06/18 10:35, Dmitriy Traytel wrote: > 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 This is ultimately a problem of the class target in conjunction with the unnamed local context. See now changeset: 68351:bcdc4c21ab1d tag: tip user:wenzelm date:Fri Jun 01 22:01:43 2018 +0200 files: src/Pure/Isar/class.ML description: varify frees, notably dangling_params (see also e0cd57aeb60c); > @Makarius: What is the rationale behind disallowing the definition of c? The changeset explains it as follows: changeset: 68239:e0cd57aeb60c user:wenzelm date:Sun May 20 22:37:00 2018 +0200 files: src/Pure/global_theory.ML description: more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact); At first I did not want to expose odd mixtures of free vs. schematic variables to the world out there, and for global items we have a clear understanding that fixed vs. schematic can always be flipped via Logic.varify_global/unvarify_global and related operations. Moreover, the check was meant to tighten existing tools and local theory targets, as we have seen here. In the process, I had to give up the full rigour, though: a3bd410db5b2 allows mixed variable indexes. Looking even more closely at global facts, there might be further problems that are still undetected. In the next round I will experiment with Thm.plain_prop_of to see if we can disallow hyps, shyps, tpairs. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken
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. 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 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-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken
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 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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
