Email Gateway (Aug 08 2020 at 15:53): Email Gateway (Aug 08 2020 at 15:53):From: Mario Carneiro <di.gama@gmail.com>
(I'm posting this to isabelle-dev since it's a very internal technical
question that probably won't be of interest to end users.)
So I've managed to successfully modify the kernel to support better proof
traces, with ~0 performance impact, but while processing HOL I hit an error
in Extraction.thy that am having trouble debugging.
The line that fails is:
lemmas [extraction_expand] = meta_spec
which gives an error "add_expand_thm: unnamed theorem". I believe this
means that add_expand_thm is being passed the wrong theorem, or a variant
on the theorem, that hasn't been explicitly tagged with the name. However,
as near as I can tell, this lemmas directive does the same thing as
ML "Extraction.add_expand_thm false @{thm meta_spec} @{theory}"
and this has no errors. How can I more precisely unfold the meaning of the
lemmas command here to get ML code that has exactly the same behavior, so
that I can inline functions until I've isolated the source of the
problematic theorem?
Also, is there any way for me to do "printf debugging" in isabelle/ML? The
focus on pure functional programming makes debugging especially difficult,
but I'm sure I'm just missing the idioms for doing so (understandably, I
can't find any examples of debugging in the source).
Email Gateway (Aug 08 2020 at 16:00):From: Manuel Eberl <eberlm@in.tum.de>
On 08/08/2020 17:52, Mario Carneiro wrote:
So I've managed to successfully modify the kernel to support better
proof traces, with ~0 performance impact, but while processing HOL I hit
an error in Extraction.thy that am having trouble debugging.
Oof, I can't help you with your actual question, but my advice would be
to just ignore Extraction for now (i.e. just remove it from HOL). It's
not really used much and I don't think anyone except Stefan Berghofer
understands the code in detail. For an experiment such as the one that
you are doing, I think it is safe to ignore whatever problems arise from
Extraction for now.
Also, is there any way for me to do "printf debugging" in isabelle/ML?
The focus on pure functional programming makes debugging especially
difficult, but I'm sure I'm just missing the idioms for doing so
(understandably, I can't find any examples of debugging in the source).
There are a few functions ("writeln", "Pretty.writeln", "print_tac" for
tactics) but the easiest one in most circumstances is the @{print}
antiquotation which takes just about anything (integers, lists, types,
terms, theorems) and just prints it. For instance:
let
val _ = @{print} my_term
in
<actual code>
end
I sometimes turn terms into cterms before printing them like this
because then they are printed more nicely.
Very interesting thing that you're trying here, and I must commend you
for your bravery to delve this deep into the internals of Isabelle all
by yourself!
I recall you saying earlier this year that you might try to do this, but
I didn't expect you to actually go through with it. You must /really/
want some of our precious Isabelle/HOL theorems very badly. ;)
Manuel
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 08 2020 at 16:28):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
On 08.08.20 17:52, Mario Carneiro wrote:> ....
Also, is there any way for me to do "printf debugging" in isabelle/ML?
The focus on pure functional programming makes debugging especially
difficult, but I'm sure I'm just missing the idioms for doing so
(understandably, I can't find any examples of debugging in the source).
The ML-cookbook has a section (2.2) about debugging that might help you:
https://nms.kcl.ac.uk/christian.urban/Cookbook/
Some combinators (like "tap") might also speed up your development (see
section 2.3).
Currently I'm in the first stage, which involves modifying primarily
thm.ML and proofterm.ML to support "proof traces" instead of "proof
terms".
Do you mind giving more details about what you mean by "proof traces" in
this context?
Best wishes,
Kevin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 08 2020 at 20:48):From: Makarius <makarius@sketis.net>
This means you are interfering with the ongoing Isabelle development process
(i.e. everything around repository versions, including administrative problems).
Whatever you do with official Isabelle releases outside of the Isabelle
development process belongs to the isabelle-users mailing list. We don't have
a separate "kernel hacking mailing list" (and don't need that).
My own priority in answering threads is as follows (high to low):
1. isabelle-dev
2. isabelle-users
3. isabelle-dev material that does not belong here
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 08 2020 at 20:53):From: Makarius <makarius@sketis.net>
Standard disclaimer: the cookbook is somewhat outdated and non-standard.
People who have learned special "tricks" over there might have to unlearn them
later: there is a 50/50 chance that they are conceptually wrong, or just old.
Answer to the original question: see the "implementation" manual section "0.2.4
Printing ML values" (with examples).
(These questions belong to the isabelle-users mailing list, where more people
can benefit from the answers as well.)
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 08 2020 at 20:55):From: Makarius <makarius@sketis.net>
I find this all very interesting, but it does not belong the the
administrative isabelle-dev mailing list.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Jul 15 2022 at 23:21 UTC