Stream: math-comp users

Topic: Release of machine learning dataset based on MC 1.9.0


view this post on Zulip Karl Palmskog (Jun 05 2020 at 06:51):

We just released our corpus of Coq code based on MC 1.9.0, including both vernacular source (.v) and serialized machine-readable versions (as sexps) produced by Coq 8.10 and SerAPI: https://github.com/EngineeringSoftware/math-comp-corpus

The initial use of the corpus was for training our also-just-released tool for Coq lemma name generation: https://github.com/EngineeringSoftware/roosterize -- but we expect wide applicability of the corpus in other machine learning tasks, such as Coq formatting learning/prediction.

Suggestions for additional MC-related projects to include in future versions of the corpus would be very welcome.

view this post on Zulip Karl Palmskog (Jun 05 2020 at 07:02):

Many thanks to @Cyril Cohen for his help with project curation and project porting!


Last updated: Jul 15 2024 at 21:02 UTC