math-comp [Recurring issue] Checking that all new lemmas, Exports modules, and Canonical Structures are exported in ssralg.v

This is a continuation of #425. The wish is to automate the verification that all new lemmas, canonical structures, and Export modules are duly exported by the GRing.Theory module, module export declarations, and canonical structure declarations. An example of the checks is given in #425.

Nov 25 '19 16:11 ybertot

We should discuss with the Coq developers to see whether visibility can be handled directly at each command using attributes.

Nov 27 '19 09:11 ybertot

For the record, here is the list of constants defined/proved in GRing but not exported (as constants) in GRing.Theory (generated by sed, sort, diff from the output of Print GRing. and Print GRing.Theory.):

(click to expand)

Frobenius_aut, Frobenius_aut_additive, Frobenius_aut_is_rmorphism, Frobenius_aut_rmorphism, If, If_form_qf, If_form_rf, Pick, Pick_form_qf, QEdecFieldMixin, add, add_comoid, add_fun_additive, add_fun_head, add_fun_is_additive, add_fun_is_scalable, add_fun_linear, add_monoid, addoid, addr_closed, and_dnf, and_dnfP, cat_dnfP, char, comm, comp_additive, comp_is_additive, comp_is_multiplicative, comp_is_scalable, comp_linear, comp_lrmorphism, comp_rmorphism, converse, converse_choiceType, converse_eqType, converse_ringMixin, converse_ringType, converse_unitRingMixin, converse_unitRingType, converse_zmodType, divalg_closed, divalg_closedBdiv, divalg_closedZ, divr_2closed, divr_closed, divr_closedM, divr_closedV, divring_closed, divring_closedBM, divring_closed_div, dnf_rterm, dnf_to_form, dnf_to_form_qf, dnf_to_rform, eq0_rform, eval, eval_If, eval_Pick, exp, foldExistsP, foldForallP, formula_ind, formula_rec, formula_rect, formula_sind, fsubst, holds, idfun_additive, idfun_is_additive, idfun_is_multiplicative, idfun_is_scalable, idfun_linear, idfun_lrmorphism, idfun_rmorphism, in_alg_additive, in_alg_head, in_alg_is_rmorphism, in_alg_rmorphism, inv, invr_closed, lastr_eq0, linear_closed, linear_closedB, locked_additive, locked_is_additive, locked_is_multiplicative, locked_is_scalable, locked_linear, locked_lrmorphism, locked_rmorphism, lreg, mul, mul_comoid, mul_monoid, mull_fun_additive, mull_fun_head, mull_fun_is_additive, mull_fun_is_scalable, mull_fun_linear, muloid, mulr_2closed, mulr_closed, mulr_fun_additive, mulr_fun_head, mulr_fun_is_additive, mulr_fun_is_scalable, mulr_fun_linear, natmul, natr_mod_char, null_fun_additive, null_fun_head, null_fun_is_additive, null_fun_is_scalable, null_fun_linear, one, opp, opp_additive, opp_is_additive, opp_is_scalable, opp_linear, oppr_closed, proj_sat, proj_satP, qf_eval, qf_evalP, qf_form, qf_to_dnf, qf_to_dnfP, qf_to_dnf_rterm, quantifier_elim, quantifier_elim_rformP, quantifier_elim_wf, regular, regular_algType, regular_choiceType, regular_comAlgType, regular_comRingType, regular_comUnitAlgType, regular_comUnitRingType, regular_eqType, regular_fieldType, regular_idomainType, regular_lalgType, regular_lmodMixin, regular_lmodType, regular_ringType, regular_unitAlgType, regular_unitRingType, regular_zmodType, rev_unitrP, rformula, rreg, rterm, same_env, same_env_sym, sat, scale, scale_additive, scale_fun_additive, scale_fun_head, scale_fun_is_scalable, scale_fun_linear, scale_is_scalable, scale_linear, scaler_closed, sdivr_closed, sdivr_closedM, sdivr_closed_div, semiring_closed, semiring_closedD, semiring_closedM, smulr_closed, smulr_closedM, smulr_closedN, sol, sol_subproof, sub_fun_additive, sub_fun_head, sub_fun_is_additive, sub_fun_is_scalable, sub_fun_linear, subalg_closed, subalg_closedBM, subalg_closedZ, submod_closed, submod_closedB, submod_closedZ, subr_2closed, subr_char2, subring_closed, subring_closedB, subring_closedM, subring_closed_semi, term_ind, term_rec, term_rect, term_sind, to_rform, to_rformP, to_rform_rformula, to_rterm, to_rterm_id, tsubst, ub_var, unit, unit_divrPred, unit_key, unit_keyed, unit_mulrPred, unit_opprPred, unit_sdivrPred, unit_smulrPred, unitr_sdivr_closed, valid_QE_proj, wf_QE_proj, zero, zmod_closed, zmod_closedD, zmod_closedN.

I think it's possible to remove the boilerplate definitions in the GRing.Theory module by reorganizing modules as in order and ssrnum. In that case, some canonical instances (e.g., add_comoid and add_monoid) should be defined in the theory module but their unqualified names must not be exported. The Local Canonical command can be used to meet this requirement.

Nov 29 '19 08:11 pi8027

Oh, the meaning of the Local Canonical command (in modules) might be changed from "the unqualified name of this constant is local" to "the unification hint synthesized from this declaration is local" in coq/coq#11162. However, since the provided examples are about local canonical instances in sections, I still don't understand the exact behavior and changes on that... cc: @gares

Dec 03 '19 13:12 pi8027

I suggest putting a milestone here not to forget to check ssralg before every release. After checking, it should be postponed to the next milestone.

May 13 '21 15:05 pi8027

@CohenCyril @ybertot Can one of you please check that everyhing that has been added to ssralg.v since the mathcomp-1.12.0 tag and should be exported actually is exported and then update the milestone of this issue to 1.14.0 ?