feat: export pretty-printed tactic states #702
Conversation
This small commit, in combination with the ast parsing in mathport, together make it straightforward to produce high-quality datasets of tactic applications.
src/library/tactic/tactic_log.h
Outdated
| @@ -87,6 +88,7 @@ class tactic_log { | |||
|
|
|||
| private: | |||
| mutable std::vector<tactic_invocation> m_invocs; | |||
| mutable std::vector<std::string> m_tspps; // tactic state pretty-printeds | |||
| using state_map = std::unordered_map<summary, tactic_state_id, summary_hash, summary_eq>; | |||
| mutable state_map m_state_map; | |||
| mutable std::vector<summary> m_states; | |||
There was a problem hiding this comment.
| mutable std::vector<summary> m_states; | |
| mutable std::vector<std::pair<summary, std::string>> m_states; |
If you push the pp into the state array then you only ever pretty print a state once. Correspondingly, the json export should put the pretty printed state at root.states[i].pp instead of root.tspps.
There was a problem hiding this comment.
Thanks. I just added it to the summary object instead.
@digama0 suggested something similar leanprover-community#702 (comment)
@digama0 suggested something similar leanprover-community#702 (comment)
src/library/tactic/tactic_log.cpp
Outdated
| os << ts.pp(); | ||
| get_tspps(l).push_back(os.str()); | ||
| os << s.pp(); | ||
| pp = optional<std::string>(os.str()); |
There was a problem hiding this comment.
No, this should not be done in summarize because that is before deduplication. It should either be like I wrote it, separate from the summary so that summarize does not produce it, or else summarize should always produce pp = none, the hash and eq should ignore this field, and it should only be set in get_id when we actually want to push it to get_states.
|
What is the status of this PR? |
|
Mario had some comments, from my side it looks good. bors d=digama0 |
|
✌️ digama0 can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Oops, I did squash and merge instead of bors. I assume it's fine? |
|
The commit message is fugly, but I'm happy as long as it builds. |
cc @PatrickMassot