Email Gateway (Aug 18 2022 at 20:27): Email Gateway (Aug 18 2022 at 20:27):From: Mark Wassell <mpwassell@gmail.com>
Hello,
I am using Isabelle/jEdit. I infer from the tutorial that when using
ProofGeneral there is a "Isabelle --> Settings" menu. Is there an
equivalent way of accessing/changing these settings when using jEdit? I am
happy to write lines like
using [[simp_trace=true]]
into my thy file on a temporary basis. I see the 'Tracing' toggle on the
jEdit GUI but assume this is to control general viewing of trace output; I
still need to enable specific tracing.
Is there a list of what possible values for X and Y are possible in lines
like
using [[ X = Y ]]
In particular I would like to enable unification tracing.
Cheers
Mark
Email Gateway (Aug 18 2022 at 20:27):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Mark,
in Isabelle2012 it is not possible to change configuration options via
jEdit menus. Concerning the question where available configuration
options are to be found: The most comprehensive "official" reference
(besides the sources) is the Isabelle Reference Manual (open via
'isabelle doc isar-ref' from a command line). Another alternative is the
command
print_configs
I'm not aware of an option for tracing unification (which does not mean
that such an option does not exist, I just don't know).
cheers
chris
Email Gateway (Aug 18 2022 at 20:27):From: Lukas Bulwahn <bulwahn@in.tum.de>
Hi Mark,
The command print_configs shows all configurations with their current
setting.
The types tell you which values are possible on the right-hand side.
E.g., for bool, values are true or false, for real and int, it could be
some number, for strings you have to look further in the documentation
and references.
For unification, we provide 4 configurations:
unify_search_bound: int = 60
unify_trace_bound: int = 50
unify_trace_simp: bool = false
unify_trace_types: bool = false
Setting those will probably do what you want.
Lukas
Last updated: Apr 27 2024 at 01:05 UTC