This issue parallels the content of Mathlib/Mathport/Syntax.lean, tracking the remaining work to port mathlib3 tactics to mathlib4, but also contains "ephemeral" information that does not belong in that file.
Primarily, this issue contains a list of tactics (or groups of tactics), along with any relevant information about work-in-progress (e.g. people who've "claimed" a tactic, PRs, abandoned work, etc). Some "claims" are probably out-of-date. Feel free to remove yourself from anything here without explanation!
We hope that everyone will edit this freely to try to keep it up to date.
Currently this is in the same order as Syntax.lean (although with tactics we might skip or only "stub" deferred to the end), but it may be worthwhile to turn this into a prioritised list.
🔹 – unclaimed
◼️ – claimed
☑️ – PR'd, unneeded, or otherwise done
E: Easy. It's a simple macro in terms of existing things,
or an elab tactic for which we have many similar examples. Example: left
M: Medium. An elab tactic, not too hard, perhaps a 100-200 lines file. Example: have
N: Possibly requires new mechanisms in lean 4, some investigation required
B: Hard, because it is a big and complicated tactic
S: Possibly easy, because we can just stub it out or replace with something else
?: uncategorized
We then have a number of tactics and commands for which mere stubs will suffice for the port. Sometimes this is because the tactic is only used during development (but not in PRs to mathlib), other times because it is not used at all anymore in mathlib.
This issue parallels the content of
Mathlib/Mathport/Syntax.lean, tracking the remaining work to port mathlib3 tactics to mathlib4, but also contains "ephemeral" information that does not belong in that file.Primarily, this issue contains a list of tactics (or groups of tactics), along with any relevant information about work-in-progress (e.g. people who've "claimed" a tactic, PRs, abandoned work, etc). Some "claims" are probably out-of-date. Feel free to remove yourself from anything here without explanation!
We hope that everyone will edit this freely to try to keep it up to date.
Currently this is in the same order as
Syntax.lean(although with tactics we might skip or only "stub" deferred to the end), but it may be worthwhile to turn this into a prioritised list.🔹 – unclaimed
◼️ – claimed
☑️ – PR'd, unneeded, or otherwise done
E: Easy. It's a simple macro in terms of existing things,or an elab tactic for which we have many similar examples. Example:
leftM: Medium. An elab tactic, not too hard, perhaps a 100-200 lines file. Example:haveN: Possibly requires new mechanisms in lean 4, some investigation requiredB: Hard, because it is a big and complicated tacticS: Possibly easy, because we can just stub it out or replace with something else?: uncategorizedNparameterSabstractas_aux_lemmaBcccctactic (3/3) #5938Munfold_projsNtry_forScleanSrefine_structrefine'with built-in..syntax, e.g.refine' { x := 0, y := 1 .. }Mmatch_hypNfield/Shave_field/Sapply_fieldMh_generalizeMcongrmcongr(...)congruence quotations and portcongrmtactic #2544Eac_changeac_changetactic #5869Mdecide!Mdelta_instanceMgeneralizesBitautoitautofrom lean 3 #9398BobviouslyMassoc_rwSdsimp_result/Nsimp_resultMtrunc_casesEapply_normedMmonoBac_monoMunfold_casesBequiv_rwNnth_rwnth_rewrite#823, although this doesn't actually reproduce the mathlib3 behaviourMcompute_degree_lefeat: Add tactic[Merged by Bors] - feat: tacticcompute_degree_le#5882compute_degree#6221Mpadic_index_simpEuniqueDiffWithinAt_Ici_Iic_univMghost_fun_tacMghost_calcMinit_ringEghost_simpEwitt_truncate_fun_tacMpure_coherence/Mcoherenceconvmode)E[norm_num][norm_num-conv] /E[norm_num1][norm_num1-conv]@bollu claimed thisis no longer working on it?protect_projprotectedcan be used for constructors.Mnotation_classMmonoNadd_tactic_docNmk_simp_attributeMadd_hint_tactic@Komyyy PR'd as feat: port tactichint#5363register_hintNdef_replacerMreassoc_axiomWe then have a number of tactics and commands for which mere stubs will suffice for the port. Sometimes this is because the tactic is only used during development (but not in PRs to mathlib), other times because it is not used at all anymore in mathlib.
Sintro/Sintro!Spropagate_tags?quote/?pquote/?ppquoteSmapplySdestructSrsimpScomp_valdecide.SasyncScontinueSextract_goalextract_goaltactic #4595Srevert_depsSrevert_afterSrevert_target_depsSrcases?Srintro?Shint@Komyyy PR'd as feat: port tactichint#5363Sclarify/Ssafe/SfinishScases''/Sinduction''Spretty_casesSsuggestSomegaStransportSrw_searchrw_searchtactic #6120Smk_decorationsSmv_bisimSsubtype_instanceSelide/SunelideSguard_tagsSguard_proof_termSfail_if_successSsetup_tactic_parser?and*notations for sytaxes are available without a command.S#list_unused_declsS#simpS#whereS#sample