Re: [isabelle] make_string

On 25/06/18 11:02, Dominique Unruh wrote:
> You will not get this from @{make_string}, only something similar
> looking but unparseable.
> @{make_string} gives you somewhat human readable output, for debugging
> (which, in case of term is relatively raw, I assume that is because it
> has to work on non-wellformed terms, too).
> So - independent of whether it is production-suitable or it - it does
> not seem to be what you are looking for.

This already summarizes the situation nicely: @{make_string} / @{print}
is for tracing and debugging while doing Isabelle/ML development. The
output is sometimes close to ML notation (e.g. term structure),
sometimes close to regular output (e.g. typ). In some situations there
might be no usable output at all: the exact side-conditions change over
time as the Poly/ML compiler evolves.

Thus it is suitable (and very useful) for adhoc tests, but not suitable
for another program reading the results. Even with perfect output, the
build-in print_depth prevents this. (The print_depth is very important
to avoid bombing the system when printing really big values.)

The default pretty printing with markup conforms to this overall idea of
@{make_string} / @{print} as adhoc diagnostic output. That was the start
of the thread: the <markup> that appears routinely when printing
structured values.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.