add training directory defining training sets, update README.md

Author: palmskog

README.md

@@ -2,6 +2,9 @@
 
 Roosterize is a tool for suggesting lemma names in verification
 projects that use the [Coq proof assistant](https://coq.inria.fr).
+The tool is based on leveraging neural networks that take serialized Coq
+lemma statements and elaborated terms as input; see the [Technique](#Technique)
+section below.
 
 ## Requirements
 
@@ -78,7 +81,7 @@ project, and `$SERAPI_OPTIONS` should be replaced with the SerAPI
 command line options for mapping logical paths to directories (see [SerAPI's
 documentation](https://github.com/ejgallego/coq-serapi/blob/v8.11/FAQ.md#does-serapi-support-coqs-command-line-flags)).
 For example, if the logical path (inside Coq) for the project is `Verified`,
-you should set `SERAPI_OPTIONS="-Q $PATH_TO_PROJECT,Verified"`.
+you should set `SERAPI_OPTIONS="-R $PATH_TO_PROJECT,Verified"`.
 
 The command extracts all lemmas from the project, uses Roosterize's
 pre-trained model (at `./models/roosterize-ta`) to predict a lemma name
@@ -90,8 +93,6 @@ Below is an example of printed suggestions:
 infotheo/ecc_classic/bch.v: infotheo.ecc_classic.bch.BCH.BCH_PCM_altP1 -> inde_F2
 infotheo/ecc_classic/bch.v: infotheo.ecc_classic.bch.BCH.BCH_PCM_altP2 -> inde_mul
 infotheo/ecc_classic/bch.v: infotheo.ecc_classic.bch.BCH.PCM_altP -> F2_eq0
-infotheo/ecc_classic/bch.v: infotheo.ecc_classic.bch.BCH.PCM_alt_GRS -> P
-infotheo/ecc_classic/bch.v: infotheo.ecc_classic.bch.BCH_codebook -> map_P
 ...
 ```
 
@@ -109,7 +110,7 @@ For example, the Coq lemma sentence
 ```coq
 Lemma mg_eq_proof L1 L2 (N1 : mgClassifier L1) : L1 =i L2 -> nerode L2 N1.
 ```
-is serialized into the following tokens:
+is serialized into the following tokens (simplified):
 ```lisp
 (Sentence((IDENT Lemma)(IDENT mg_eq_proof)(IDENT L1)(IDENT L2)
   (KEYWORD"(")(IDENT N1)(KEYWORD :)(IDENT mgClassifier)
@@ -134,7 +135,8 @@ architecture, as applied to this example:
 Our [research paper][arxiv-paper] outlines the design of Roosterize,
 and describes an evaluation on a [corpus][math-comp-corpus]
 of serialized Coq code derived from the [Mathematical Components][math-comp-website]
-family of projects.
+family of projects. The training, validation, and testing sets of Coq files from the corpus
+used in the evaluation are defined in the `training` directory.
 
 If you have used Roosterize in a research project, please cite
 the research paper in any related publication:

training/allgroup-all.json

@@ -0,0 +1,32 @@
+[
+    "math-comp_math-comp/mathcomp/ssreflect/path.v",
+    "math-comp_real-closed/theories/polyorder.v",
+    "math-comp_fourcolor/theories/initgtree.v",
+    "affeldt-aist_coq-robot/scara.v",
+    "math-comp_math-comp/mathcomp/field/falgebra.v",
+    "math-comp_fourcolor/theories/finitize.v",
+    "coq-community_coq-bits/src/ssrextra/nat.v",
+    "math-comp_fourcolor/theories/ctreerestrict.v",
+    "palmskog_coq-reglang/theories/nfa.v",
+    "palmskog_monae/example_monty.v",
+    "palmskog_comp-dec-pdl/libs/base.v",
+    "certichain_toychain/Extraction/TypesImpl.v",
+    "math-comp_odd-order/theories/BGsection2.v",
+    "imdea-software_fcsl-pcm/pcm/pred.v",
+    "math-comp_fourcolor/theories/fourcolor.v",
+    "math-comp_fourcolor/theories/discretize.v",
+    "strub_elliptic-curves-ssr/src/ecgroup.v",
+    "math-comp_math-comp/mathcomp/algebra/ssrint.v",
+    "math-comp_odd-order/theories/BGsection12.v",
+    "math-comp_odd-order/theories/BGsection8.v",
+    "math-comp_math-comp/mathcomp/ssreflect/ssrmatching.v",
+    "math-comp_math-comp/mathcomp/solvable/sylow.v",
+    "math-comp_fourcolor/theories/grid.v",
+    "math-comp_math-comp/mathcomp/algebra/intdiv.v",
+    "gstew5_games/extrema.v",
+    "math-comp_math-comp/mathcomp/character/classfun.v",
+    "math-comp_analysis/altreals/xfinmap.v",
+    "DistributedComponents_disel/Core/InductiveInv.v",
+    "DistributedComponents_disel/Core/Process.v",
+    "math-comp_math-comp/mathcomp/algebra/mxalgebra.v"
+]

training/allgroup-test.json

@@ -0,0 +1,304 @@
+[
+    "math-comp_math-comp/mathcomp/ssreflect/eqtype.v",
+    "palmskog_monae/convex_space_category.v",
+    "palmskog_monae/example_relabeling.v",
+    "math-comp_odd-order/theories/PFsection11.v",
+    "palmskog_comp-dec-pdl/PDL/rewrite_inequality.v",
+    "math-comp_real-closed/theories/complex.v",
+    "affeldt-aist_coq-robot/ssr_ext.v",
+    "math-comp_odd-order/theories/BGsection11.v",
+    "gstew5_games/potential.v",
+    "math-comp_fourcolor/theories/hypermap.v",
+    "coq-community_coq-bits/src/spec/operations.v",
+    "gstew5_games/dyadic.v",
+    "math-comp_math-comp/mathcomp/algebra/matrix.v",
+    "math-comp_math-comp/mathcomp/character/all_character.v",
+    "palmskog_comp-dec-pdl/libs/fset.v",
+    "math-comp_fourcolor/theories/part.v",
+    "math-comp_math-comp/mathcomp/algebra/vector.v",
+    "math-comp_math-comp/mathcomp/ssreflect/ssrfun.v",
+    "imdea-software_fcsl-pcm/finmap/finmap.v",
+    "affeldt-aist_coq-robot/differential_kinematics.v",
+    "strub_elliptic-curves-ssr/src/ecpolyfrac.v",
+    "affeldt-aist_coq-robot/frame.v",
+    "math-comp_analysis/normedtype.v",
+    "math-comp_fourcolor/theories/unavoidability.v",
+    "DistributedComponents_disel/Core/NetworkSem.v",
+    "math-comp_fourcolor/theories/matte.v",
+    "math-comp_math-comp/mathcomp/solvable/alt.v",
+    "math-comp_math-comp/mathcomp/fingroup/gproduct.v",
+    "math-comp_odd-order/theories/PFsection14.v",
+    "math-comp_fourcolor/theories/dedekind.v",
+    "math-comp_math-comp/mathcomp/solvable/hall.v",
+    "DistributedComponents_disel/Core/Always.v",
+    "palmskog_comp-dec-pdl/CPDL/hilbert_ref.v",
+    "certichain_toychain/Systems/Protocol.v",
+    "math-comp_odd-order/theories/BGsection5.v",
+    "math-comp_real-closed/theories/qe_rcf_th.v",
+    "affeldt-aist_coq-robot/skew.v",
+    "strub_elliptic-curves-ssr/src/ecdivlr.v",
+    "math-comp_fourcolor/theories/real.v",
+    "strub_elliptic-curves-ssr/src/ecrr.v",
+    "math-comp_fourcolor/theories/birkhoff.v",
+    "math-comp_fourcolor/theories/walkup.v",
+    "math-comp_math-comp/mathcomp/ssreflect/ssrbool.v",
+    "math-comp_odd-order/theories/PFsection2.v",
+    "math-comp_fourcolor/theories/chromogram.v",
+    "palmskog_monae/category.v",
+    "thery_twoSquare/fermat2.v",
+    "math-comp_fourcolor/theories/patch.v",
+    "math-comp_real-closed/theories/mxtens.v",
+    "coq-community_coq-bits/src/extraction/axioms16.v",
+    "math-comp_multinomials/src/ssrcomplements.v",
+    "math-comp_math-comp/mathcomp/algebra/polyXY.v",
+    "math-comp_math-comp/mathcomp/solvable/commutator.v",
+    "math-comp_fourcolor/theories/gtree.v",
+    "imdea-software_fcsl-pcm/pcm/axioms.v",
+    "coq-community_coq-bits/src/spec/operations/properties.v",
+    "palmskog_comp-dec-pdl/PDL/hilbert_ref.v",
+    "math-comp_analysis/classical_sets.v",
+    "math-comp_math-comp/mathcomp/character/character.v",
+    "math-comp_fourcolor/theories/initctree.v",
+    "math-comp_fourcolor/theories/present10.v",
+    "certichain_toychain/Structures/Forests.v",
+    "strub_elliptic-curves-ssr/common/polyfrac.v",
+    "math-comp_odd-order/theories/PFsection1.v",
+    "math-comp_math-comp/mathcomp/algebra/countalg.v",
+    "gstew5_games/dist.v",
+    "palmskog_monae/monad_composition.v",
+    "math-comp_math-comp/mathcomp/algebra/fraction.v",
+    "affeldt-aist_coq-robot/quaternion.v",
+    "palmskog_monae/proba_monad_model.v",
+    "math-comp_math-comp/mathcomp/ssreflect/choice.v",
+    "math-comp_fourcolor/theories/configurations.v",
+    "math-comp_fourcolor/theories/color.v",
+    "math-comp_fourcolor/theories/discharge.v",
+    "imdea-software_fcsl-pcm/pcm/lift.v",
+    "affeldt-aist_coq-robot/vec_angle.v",
+    "palmskog_coq-reglang/theories/myhill_nerode.v",
+    "math-comp_math-comp/mathcomp/ssreflect/prime.v",
+    "strub_elliptic-curves-ssr/3rdparty/fraction.v",
+    "math-comp_math-comp/mathcomp/solvable/finmodule.v",
+    "math-comp_fourcolor/theories/jordan.v",
+    "math-comp_fourcolor/theories/cfreducible.v",
+    "math-comp_math-comp/mathcomp/algebra/mxpoly.v",
+    "coq-community_coq-bits/src/extraction/axioms8.v",
+    "math-comp_odd-order/theories/PFsection9.v",
+    "math-comp_odd-order/theories/PFsection5.v",
+    "math-comp_math-comp/mathcomp/solvable/center.v",
+    "math-comp_finmap/finmap.v",
+    "math-comp_real-closed/theories/polyrcf.v",
+    "math-comp_math-comp/mathcomp/algebra/interval.v",
+    "certichain_toychain/Structures/Parameters.v",
+    "palmskog_comp-dec-pdl/libs/fset_tac.v",
+    "math-comp_odd-order/theories/PFsection12.v",
+    "math-comp_fourcolor/theories/revsnip.v",
+    "palmskog_monae/state_monad.v",
+    "math-comp_math-comp/mathcomp/fingroup/all_fingroup.v",
+    "math-comp_fourcolor/theories/kempetree.v",
+    "math-comp_math-comp/mathcomp/field/fieldext.v",
+    "imdea-software_fcsl-pcm/pcm/mutex.v",
+    "certichain_toychain/Structures/Types.v",
+    "palmskog_coq-reglang/theories/misc.v",
+    "coq-community_coq-bits/src/ssrextra/tuple.v",
+    "math-comp_odd-order/theories/PFsection13.v",
+    "gstew5_games/games.v",
+    "math-comp_analysis/Rbar.v",
+    "math-comp_math-comp/mathcomp/ssreflect/seq.v",
+    "palmskog_comp-dec-pdl/libs/modular_hilbert.v",
+    "coq-community_coq-bits/src/bits.v",
+    "math-comp_math-comp/mathcomp/algebra/ssrnum.v",
+    "math-comp_math-comp/mathcomp/field/closed_field.v",
+    "math-comp_fourcolor/theories/approx.v",
+    "palmskog_coq-reglang/theories/wmso.v",
+    "strub_elliptic-curves-ssr/src/eceval.v",
+    "strub_elliptic-curves-ssr/common/fracfield.v",
+    "math-comp_fourcolor/theories/sew.v",
+    "math-comp_math-comp/mathcomp/algebra/zmodp.v",
+    "math-comp_math-comp/mathcomp/solvable/cyclic.v",
+    "math-comp_math-comp/mathcomp/ssreflect/fingraph.v",
+    "palmskog_monae/altprob_model.v",
+    "strub_elliptic-curves-ssr/src/ecdiv.v",
+    "certichain_toychain/Properties/InvMisc.v",
+    "palmskog_monae/trace_monad.v",
+    "math-comp_odd-order/theories/BGsection4.v",
+    "math-comp_odd-order/theories/PFsection4.v",
+    "math-comp_fourcolor/theories/present.v",
+    "math-comp_math-comp/mathcomp/fingroup/fingroup.v",
+    "imdea-software_fcsl-pcm/pcm/pcm.v",
+    "math-comp_math-comp/mathcomp/fingroup/action.v",
+    "certichain_toychain/Systems/States.v",
+    "math-comp_fourcolor/theories/dyck.v",
+    "math-comp_math-comp/mathcomp/solvable/jordanholder.v",
+    "math-comp_fourcolor/theories/gtreerestrict.v",
+    "math-comp_multinomials/src/xfinmap.v",
+    "DistributedComponents_disel/Core/InferenceRules.v",
+    "palmskog_coq-reglang/theories/languages.v",
+    "math-comp_math-comp/mathcomp/algebra/rat.v",
+    "math-comp_odd-order/theories/PFsection6.v",
+    "math-comp_real-closed/theories/realalg.v",
+    "imdea-software_fcsl-pcm/pcm/heap.v",
+    "math-comp_math-comp/mathcomp/all/all.v",
+    "math-comp_analysis/Rstruct.v",
+    "DistributedComponents_disel/Core/State.v",
+    "DistributedComponents_disel/Core/Worlds.v",
+    "math-comp_fourcolor/theories/cfmap.v",
+    "math-comp_math-comp/mathcomp/ssreflect/ssrnat.v",
+    "certichain_toychain/Systems/Address.v",
+    "math-comp_finmap/multiset.v",
+    "math-comp_fourcolor/theories/redpart.v",
+    "math-comp_math-comp/mathcomp/algebra/poly.v",
+    "math-comp_bigenough/bigenough.v",
+    "math-comp_analysis/altreals/realsum.v",
+    "math-comp_odd-order/theories/BGsection16.v",
+    "palmskog_coq-reglang/theories/two_way.v",
+    "math-comp_math-comp/mathcomp/fingroup/morphism.v",
+    "thery_grobner/grobner.v",
+    "math-comp_finmap/order.v",
+    "math-comp_math-comp/mathcomp/fingroup/perm.v",
+    "palmskog_monae/smallstep_monad.v",
+    "math-comp_math-comp/mathcomp/solvable/burnside_app.v",
+    "math-comp_math-comp/mathcomp/ssreflect/ssreflect.v",
+    "imdea-software_fcsl-pcm/pcm/unionmap.v",
+    "math-comp_math-comp/mathcomp/solvable/gseries.v",
+    "palmskog_comp-dec-pdl/libs/edone.v",
+    "imdea-software_fcsl-pcm/finmap/ordtype.v",
+    "math-comp_math-comp/mathcomp/field/separable.v",
+    "math-comp_math-comp/mathcomp/solvable/pgroup.v",
+    "math-comp_math-comp/mathcomp/solvable/extraspecial.v",
+    "math-comp_fourcolor/theories/quiz.v",
+    "affeldt-aist_coq-robot/dh.v",
+    "DistributedComponents_disel/Core/While.v",
+    "gstew5_games/christodoulou.v",
+    "math-comp_odd-order/theories/BGsection3.v",
+    "DistributedComponents_disel/Core/NewStatePredicates.v",
+    "DistributedComponents_disel/Core/Injection.v",
+    "affeldt-aist_coq-robot/rot.v",
+    "palmskog_monae/smallstep.v",
+    "DistributedComponents_disel/Core/Freshness.v",
+    "math-comp_odd-order/theories/wielandt_fixpoint.v",
+    "palmskog_comp-dec-pdl/libs/sltype.v",
+    "math-comp_fourcolor/theories/gridmap.v",
+    "math-comp_real-closed/theories/all_real_closed.v",
+    "gstew5_games/smooth.v",
+    "math-comp_fourcolor/theories/snip.v",
+    "math-comp_fourcolor/theories/present6.v",
+    "imdea-software_fcsl-pcm/pcm/natmap.v",
+    "math-comp_math-comp/mathcomp/solvable/nilpotent.v",
+    "math-comp_math-comp/mathcomp/field/algC.v",
+    "math-comp_odd-order/theories/BGsection14.v",
+    "strub_elliptic-curves-ssr/common/ssrring.v",
+    "math-comp_odd-order/theories/BGsection7.v",
+    "math-comp_math-comp/mathcomp/ssreflect/ssrnotations.v",
+    "math-comp_odd-order/theories/BGsection10.v",
+    "math-comp_analysis/forms.v",
+    "math-comp_math-comp/mathcomp/field/algebraics_fundamentals.v",
+    "certichain_toychain/Systems/Network.v",
+    "math-comp_math-comp/mathcomp/field/algnum.v",
+    "palmskog_comp-dec-pdl/CPDL/demo.v",
+    "coq-community_coq-bits/src/extraction/axioms32.v",
+    "palmskog_coq-reglang/theories/shepherdson.v",
+    "math-comp_finmap/set.v",
+    "palmskog_monae/model.v",
+    "certichain_toychain/Properties/InvCliqueTopology.v",
+    "palmskog_coq-reglang/theories/minimization.v",
+    "palmskog_monae/proba_monad.v",
+    "DistributedComponents_disel/Core/StatePredicates.v",
+    "certichain_toychain/Extraction/Recipe.v",
+    "palmskog_monae/monad.v",
+    "math-comp_math-comp/mathcomp/solvable/maximal.v",
+    "math-comp_math-comp/mathcomp/character/mxrepresentation.v",
+    "math-comp_math-comp/mathcomp/solvable/abelian.v",
+    "math-comp_math-comp/mathcomp/solvable/extremal.v",
+    "gstew5_games/general.v",
+    "math-comp_math-comp/mathcomp/solvable/frobenius.v",
+    "DistributedComponents_disel/Core/HoareTriples.v",
+    "math-comp_math-comp/mathcomp/fingroup/presentation.v",
+    "gstew5_games/numerics.v",
+    "strub_elliptic-curves-ssr/src/ec.v",
+    "math-comp_analysis/altreals/discrete.v",
+    "palmskog_coq-reglang/theories/dfa.v",
+    "math-comp_math-comp/mathcomp/ssreflect/bigop.v",
+    "DistributedComponents_disel/Core/Domain.v",
+    "strub_elliptic-curves-ssr/common/xmatrix.v",
+    "DistributedComponents_disel/Core/DiSeLExtraction.v",
+    "certichain_toychain/Extraction/Impl.v",
+    "gstew5_games/routing.v",
+    "strub_elliptic-curves-ssr/src/ecorder.v",
+    "math-comp_real-closed/theories/ordered_qelim.v",
+    "math-comp_math-comp/mathcomp/fingroup/quotient.v",
+    "math-comp_multinomials/src/mpoly.v",
+    "math-comp_math-comp/mathcomp/solvable/all_solvable.v",
+    "math-comp_math-comp/mathcomp/ssreflect/tuple.v",
+    "math-comp_fourcolor/theories/cfcontract.v",
+    "math-comp_odd-order/theories/BGsection9.v",
+    "math-comp_fourcolor/theories/cfcolor.v",
+    "math-comp_fourcolor/theories/ctree.v",
+    "math-comp_math-comp/mathcomp/algebra/ring_quotient.v",
+    "math-comp_fourcolor/theories/realcategorical.v",
+    "math-comp_math-comp/mathcomp/field/cyclotomic.v",
+    "math-comp_odd-order/theories/BGsection13.v",
+    "DistributedComponents_disel/Core/Actions.v",
+    "math-comp_fourcolor/theories/present11.v",
+    "imdea-software_fcsl-pcm/pcm/prelude.v",
+    "math-comp_math-comp/mathcomp/field/all_field.v",
+    "palmskog_monae/example_spark.v",
+    "math-comp_analysis/topology.v",
+    "math-comp_real-closed/theories/cauchyreals.v",
+    "DistributedComponents_disel/Core/Rely.v",
+    "math-comp_odd-order/theories/stripped_odd_order_theorem.v",
+    "math-comp_analysis/posnum.v",
+    "math-comp_fourcolor/theories/coloring.v",
+    "math-comp_math-comp/mathcomp/character/inertia.v",
+    "strub_elliptic-curves-ssr/common/polydec.v",
+    "math-comp_math-comp/mathcomp/ssreflect/generic_quotient.v",
+    "math-comp_analysis/reals.v",
+    "math-comp_math-comp/mathcomp/character/integral_char.v",
+    "math-comp_math-comp/mathcomp/ssreflect/finset.v",
+    "gstew5_games/dynamics.v",
+    "math-comp_fourcolor/theories/realsyntax.v",
+    "math-comp_math-comp/mathcomp/algebra/polydiv.v",
+    "math-comp_fourcolor/theories/realplane.v",
+    "palmskog_comp-dec-pdl/PDL/PDL_def.v",
+    "math-comp_fourcolor/theories/present9.v",
+    "math-comp_odd-order/theories/PFsection7.v",
+    "math-comp_multinomials/src/freeg.v",
+    "thery_twoSquare/gauss_int.v",
+    "math-comp_fourcolor/theories/present7.v",
+    "strub_elliptic-curves-ssr/src/ecpoly.v",
+    "math-comp_analysis/altreals/realseq.v",
+    "math-comp_fourcolor/theories/hubcap.v",
+    "affeldt-aist_coq-robot/euclidean3.v",
+    "math-comp_fourcolor/theories/present8.v",
+    "math-comp_math-comp/mathcomp/ssreflect/finfun.v",
+    "math-comp_fourcolor/theories/cfquiz.v",
+    "coq-community_coq-bits/src/spec/spec/properties.v",
+    "math-comp_odd-order/theories/PFsection10.v",
+    "math-comp_math-comp/mathcomp/solvable/gfunctor.v",
+    "math-comp_analysis/altreals/distr.v",
+    "palmskog_coq-reglang/theories/regexp.v",
+    "palmskog_coq-reglang/theories/setoid_leq.v",
+    "math-comp_odd-order/theories/BGsection6.v",
+    "palmskog_comp-dec-pdl/CPDL/PDL_def.v",
+    "palmskog_comp-dec-pdl/PDL/demo.v",
+    "math-comp_fourcolor/theories/cube.v",
+    "affeldt-aist_coq-robot/screw.v",
+    "math-comp_analysis/derive.v",
+    "DistributedComponents_disel/Core/DepMaps.v",
+    "math-comp_analysis/landau.v",
+    "math-comp_math-comp/mathcomp/ssreflect/fintype.v",
+    "math-comp_fourcolor/theories/present5.v",
+    "math-comp_odd-order/theories/BGsection1.v",
+    "strub_elliptic-curves-ssr/common/xseq.v",
+    "certichain_toychain/Structures/Chains.v",
+    "math-comp_math-comp/mathcomp/character/mxabelem.v",
+    "math-comp_fourcolor/theories/embed.v",
+    "math-comp_odd-order/theories/BGsection15.v",
+    "affeldt-aist_coq-robot/angle.v",
+    "math-comp_fourcolor/theories/geometry.v",
+    "palmskog_monae/monad_model.v",
+    "math-comp_math-comp/mathcomp/field/galois.v",
+    "math-comp_odd-order/theories/BGappendixC.v",
+    "palmskog_comp-dec-pdl/libs/induced_sym.v",
+    "math-comp_math-comp/mathcomp/algebra/all_algebra.v"
+]