Stream: Coq users

Topic: Exporting proof term


view this post on Zulip spaceloop (Nov 25 2022 at 18:54):

Is there an easy way to "export" a gallina proof term that was generated by ltac, so that it can be reused as a definition? Using the term printed by Coq Print does not seem to print valid syntax.

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 02:23):

Print foo is usually valid syntax, unless somebody adds bad printing only notation

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 02:25):

If that happens, you can disable notations as a workaround (the way depends on the IDE), but you should probably fix those notations.

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 02:25):

It might also be a bug? Hard to say

view this post on Zulip Yann Leray (Nov 26 2022 at 03:05):

I know you can also have issues with implicit arguments which cannot [always|completely] be inferred from the remaining arguments when it comes to reusing Coq-printed terms; that can also be worked around by setting the flag to print implicit arguments

view this post on Zulip spaceloop (Dec 03 2022 at 10:58):

Thanks! Now the problem is that for very large proofs, it will print ... for sub-terms. I found Printing Depth, but apparently it has a maximum, which is not enough. Any suggestions how to work around that?

view this post on Zulip Karl Palmskog (Dec 03 2022 at 11:17):

the only reliable way I know of to get terms out from Coq is SerAPI: https://github.com/ejgallego/coq-serapi


Last updated: Jan 29 2023 at 06:02 UTC