Email Gateway (Aug 22 2022 at 13:20): Email Gateway (Aug 22 2022 at 13:20):From: Makarius <makarius@sketis.net>
This is a continuation of the thread "bogus simplifier trace messages"
from isabelle-users (Jan-2016).
After the release, I've made the following change:
changeset: 62980:ba9072b303a2
user: wenzelm
date: Thu Apr 14 16:59:47 2016 +0200
files: src/Pure/Tools/simplifier_trace.ML src/Tools/quickcheck.ML
description:
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
That is not suffient, though. Spurious traces remain. The attached
experimental setup (ch-test and Test.thy) helps to find the place where
it happens. To make this work, Pure + HOL need to be build with debugger
information:
isabelle build -c -b -o ML_debugger Pure HOL
This takes approx. 25min on my machine (the exclusion of Complex_Main
helps a lot).
The included trace1 and trace2 show the situation before and after the
following change:
changeset: 63072:413184c7a2a2
user: wenzelm
date: Mon May 09 14:37:47 2016 +0200
files: src/Doc/more_antiquote.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/record.ML src/Pure/Isar/code.ML src/Pure/axclass.ML
src/Tools/Code/code_preproc.ML src/Tools/Code/code_thingol.ML
description:
clarified context, notably for internal use of Simplifier;
The codegen setup has quite a few uses Proof_Context.init_global left:
that seems to be required for a hard reset of the logical context
(fixes, sorts of type variables etc.), but it disrupts the use of
options in the context to control other tools (notably the Simplifier).
Is there a chance to make the code generator fully context-conformant?
Makarius
ch-test
Test.thy
trace1
trace2
Email Gateway (Aug 22 2022 at 13:21):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
changeset: 63072:413184c7a2a2
user: wenzelm
date: Mon May 09 14:37:47 2016 +0200
files: src/Doc/more_antiquote.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/record.ML src/Pure/Isar/code.ML src/Pure/axclass.ML
src/Tools/Code/code_preproc.ML src/Tools/Code/code_thingol.ML
description:
clarified context, notably for internal use of Simplifier;The codegen setup has quite a few uses Proof_Context.init_global left:
that seems to be required for a hard reset of the logical context
(fixes, sorts of type variables etc.), but it disrupts the use of
options in the context to control other tools (notably the Simplifier).Is there a chance to make the code generator fully context-conformant?
indeed I am currently working in that area, to iron out some of these
issues which I have stumbled over from a different perspective also.
The main reasons why significant parts of the code generator
infrastructure are not context-conformant are not of logical nature (the
only example I am aware of is in nbe.ML) but merely technical: there is
still some ancient global-theory background cache. Over the last years
at least the user interfaces have gained more and more proper contexts,
and this will continue hopefully soon. Maybe the days of that cache are
also counted, lets see.
Cheers,
Florian
Makarius
Last updated: Apr 26 2024 at 08:19 UTC