Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] debug parts of Pure

view this post on Zulip Email Gateway (Aug 22 2022 at 14:49):

From: Walther Neuper <wneuper@ist.tugraz.at>
We want to understand details of AST translations.

After having studied §8.5. »Syntax transformations« in isar-ref und §3
»Concrete syntax and type-checking« in implementation we still had
questions. So we studied respective code (ast.ML, syntax_phases.ML, etc)
and got stuck again.

Would it be possible to re-compile respective code of Pure, such that we
can investigate it »Step«wise in the debugger ?

Walther

PS: »ML_file_debug "syntax_phases.ML"« etc seems impossible in the very
specific bootstrapping process. In the mail archive we did not find more
than the outdated »Toplevel.debug«.

Last updated: Nov 21 2024 at 12:39 UTC