Yves Bertot (Sep 25 2020 at 09:38): Yves Bertot (Sep 25 2020 at 09:38):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?
Karl Palmskog (Sep 25 2020 at 11:17):@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.
Clément Pit-Claudel (Sep 25 2020 at 13:46):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: Oct 01 2023 at 19:01 UTC