For machine learning on fitting tactics, theorems, and goals, it would be useful to have databases where all successive goals and the corresponding tactics. It would even be more useful if, in the text of these tactics, the domain of each symbol (tactic, or gallina term) was recorded. I suppose that several researchers have already developed the kind of infrastructure needed for this. Can we share on this experience? Can we try to set up a repository for this kind of information, which could be usable for further research?
@Emilio Jesús Gallego Arias and I have done some work of this, and @Clément Pit-Claudel as well. However, I'm not sure how it should be documented. Perhaps one should try to write up a "guide to [current state of] machine interaction with Coq", which showcases SerAPI and some tools built on it.
I'd love to chat or collaborate on something. For now, you can use Alectryon's "movie" format to get a JSON file with goals and tactics, though it doesn't include a lexical analysis of the tactics (I'm waiting on https://github.com/ejgallego/coq-serapi/issues/217 for this, which I think @Emilio Jesús Gallego Arias is planning to work on)
Last updated: Feb 05 2023 at 08:28 UTC