mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

tactic porting tracking issue

Open kim-em opened this issue 3 years ago • 5 comments
trafficstars

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

Things to port not in the syntax file:

  • :black_medium_square: ? solve_by_elim has a minimal port, but is not feature complete.
    • ~~Justus Springer will look at this~~ is no longer working on it, and @semorrison can help
  • :black_medium_square: (attribute) ? simps
    • @fpvandoorn has PR'd as #445

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.

kim-em avatar Sep 20 '22 03:09 kim-em

I have included information about open PRs, but have not yet gone back through all zulip threads to note other "claims".

kim-em avatar Sep 20 '22 03:09 kim-em

I won't have time to work on porting for the next couple of months, sorry; please consider copy_doc_string abandoned.

hrmacbeth avatar Sep 21 '22 00:09 hrmacbeth

@hrmacbeth, thanks for mentioning that! I'll take up copy_doc_string / add_decl_doc / add_tactic_doc then (I'm also busy at the moment, but will be able to get to it October 4th).

lakesare avatar Sep 21 '22 00:09 lakesare

Now that the semester has begun at Carnegie Mellon, I am also pretty buried. I don't mind keeping the injections tactics on my to do list in the hopes that I'll eventually find the time, but anyone else looking for something to do should feel free to claim them.

avigad avatar Sep 22 '22 20:09 avigad

Here is the result of a text search for tactic names in mathlib3port: (no promises about false positives)

6101 [M] ext
5517 [S] intro
2601 [N] dsimp
2253 [E] convert
1339 [N] congr
756 [B] tidy
714 [M] split_ifs
570 [E] norm_num
550 [E] ring
500 [B] linarith
384 [M] filter_upwards
384 [B] lift
337 [M] contrapose
282 [B] choose
256 [E] symm
209 [B] obviously
205 [M] slice_lhs
203 [M] field_simp
198 [E] trans
158 [B] abel
152 [B] tauto
136 [N] nth_rw
135 [M] apply_fun
128 [M] tfae_have
106 [M] generalize
102 [N] for
96 [B] refine_struct
93 [M] slice_rhs
92 [M] nontriviality
87 [M] mono
87 [B] mono
73 [B] cc
71 [M] continuity
67 [E] norm_num1
58 [M] apply_rules
50 [B] wlog
49 [M] fin_cases
49 [E] ring_nf
34 [M] nlinarith
31 [E] convert_to
30 [E] ring_exp
30 [B] ring_exp
27 [M] group
25 [M] tfae_finish
23 [M] generalize_proofs
21 [E] unfold_coes
18 [M] unfold_projs
18 [M] assoc_rw
17 [E] unfold_wf
17 [E] clear_value
15 [S] propagate_tags
15 [N] field
15 [E] ring1
long tail 

14 [N] abstract
14 [M] cases_type
14 [M] casesm
13 [S] with_cases
13 [M] unfold_aux
13 [E] nth_rw_rhs
13 [E] noncomm_ring
12 [M] interval_cases
12 [B] equiv_rw
11 [N] measurability
11 [M] delta_instance
9 [M] ghost_fun_tac
8 [S] interactive
8 [M] rcongr
8 [M] init_ring
8 [E] infer_auto_param
7 [M] ghost_calc
7 [M] cancel_denoms
7 [M] apply_assumption
7 [E] witt_truncate_fun_tac
6 [M] zify
5 [M] reassoc
5 [M] pi_instance
5 [M] apply_congr
5 [E] unit_interval
4 [S] extract_goal
4 [M] slice
4 [M] padic_index_simp
4 [M] clean
4 [E] ghost_simp
4 [B] ac_mono
3 [N] simp_intro
3 [N] parameter
2 [S] safe
2 [S] pretty_cases
2 [N] dsimp_result
2 [N] def_replacer
2 [M] trunc_cases
2 [M] reassoc_axiom
2 [M] linear_combination
2 [M] generalizes
2 [E] try_for
2 [E] nth_rw_lhs
2 [E] apply_normed
2 [E] ac_change
1 [S] transport
1 [S] suggest
1 [S] squeeze_scope
1 [S] omega
1 [S] mv_bisim
1 [S] hint
1 [S] finish
1 [S] destruct
1 [N] simp_result
1 [M] unfold_cases
1 [M] match_hyp
1 [M] h_generalize
1 [E] fsplit
1 [B] itauto
1 [B] equiv_rw_type
replication

words.txt obtained by searching for /- (.) -/ syntax.*?"(.*?)" in Mathport/Syntax.lean

words.txt 
[N]parameter
[S]quoteₓ
[S]pquoteₓ
[S]ppquoteₓ
[S]%%ₓ
[S]propagate_tags
[S]mapply
[S]with_cases
[S]destruct
[M]casesm
[M]cases_type
[M]cases_type!
[N]abstract
[M]constructorm
[N]simp_intro
[E]symm
[E]trans
[B]cc
[M]unfold_projs
[E]infer_auto_param
[S]rsimp
[S]comp_val
[S]async
[N]for
[N]dsimp
[E]apply'
[E]fapply'
[E]eapply'
[E]apply_with'
[E]mapply'
[E]rfl'
[E]symm'
[E]trans'
[E]fsplit
[E]try_for
[E]unfold_coes
[E]unfold_wf
[M]unfold_aux
[S]continue
[M]generalize
[M]clean
[B]refine_struct
[M]match_hyp
[E]guard_tags
[E]guard_proof_term
[E]fail_if_success?
[N]field
[N]have_field
[N]apply_field
[M]apply_rules
[M]h_generalize
[M]h_generalize!
[S]extract_goal
[S]extract_goal!
[S]revert_deps
[S]revert_after
[S]revert_target_deps
[E]clear_value
[M]apply_assumption
[S]hint
[B]choose
[B]choose!
[N]congr
[M]rcongr
[E]convert
[E]convert_to
[E]ac_change
[S]rcases?
[S]rintro?
[M]decide!
[M]delta_instance
[M]elide
[M]unelide
[S]clarify
[S]safe
[S]finish
[M]generalizes
[M]generalize_proofs
[S]cases''
[S]induction''
[B]itauto
[B]itauto!
[B]lift
[B]obviously
[S]pretty_cases
[M]contrapose
[M]contrapose!
[M]assoc_rw
[N]dsimp_result
[N]simp_result
[M]split_ifs
[S]squeeze_scope
[S]simp?
[S]simp_all?
[S]dsimp?
[S]suggest
[B]tauto
[B]tauto!
[M]trunc_cases
[E]apply_normed
[E]abel1
[E]abel1!
[B]abel
[B]abel!
[E]ring1
[E]ring1!
[E]ring_nf
[E]ring_nf!
[E]ring!
[B]ring_exp_eq
[B]ring_exp_eq!
[B]ring_exp
[B]ring_exp!
[E]noncomm_ring
[M]linear_combination
[B]linarith
[B]linarith!
[M]nlinarith
[M]nlinarith!
[S]omega
[M]tfae_have
[M]tfae_finish
[B]mono
[B]ac_mono
[M]apply_fun
[M]fin_cases
[M]interval_cases
[M]reassoc
[M]reassoc!
[M]derive_reassoc_proof
[M]slice_lhs
[M]slice_rhs
[N]subtype_instance
[M]group
[M]cancel_denoms
[M]zify
[S]transport
[M]unfold_cases
[M]field_simp
[B]equiv_rw
[B]equiv_rw_type
[N]nth_rw
[E]nth_rw_lhs
[E]nth_rw_rhs
[S]rw_search
[S]rw_search?
[M]pi_instance_derive_field
[M]pi_instance
[B]tidy
[B]tidy?
[B]wlog
[M]elementwise
[M]elementwise!
[M]derive_elementwise_proof
[S]mk_decorations
[M]nontriviality
[M]filter_upwards
[E]isBounded_default
[N]op_induction
[S]mv_bisim
[M]continuity
[M]continuity!
[M]continuity?
[M]continuity!?
[E]unit_interval
[N]measurability
[N]measurability!
[N]measurability?
[N]measurability!?
[M]padic_index_simp
[E]uniqueDiffWithinAt_Ici_Iic_univ
[M]ghost_fun_tac
[M]ghost_calc
[M]init_ring
[E]ghost_simp
[E]witt_truncate_fun_tac
[M]apply_congr
[E]norm_num1
[E]norm_num
[E]ring_nf
[E]ring_nf!
[E]ring
[E]ring!
[E]ring_exp
[E]ring_exp!
[M]slice
[S]intro
[S]intro!
[M]ext
[M]higher_order
[S]interactive
[M]mk_iff
[S]protect_proj
[M]notation_class
[M]mono
[M]reassoc
[N]ancestor
[M]elementwise
[N]copy_doc_string
[N]add_tactic_doc
[N]add_decl_doc
[S]setup_tactic_parser
[N]mk_simp_attribute
[M]add_hint_tactic
[S]#explode
[S]#list_unused_decls
[M]mk_iff_of_inductive_prop
[N]def_replacer
[S]#simp
[S]#where
[M]reassoc_axiom
[S]#sample

#!/bin/bash
for i in $(cat words.txt); do
  esc=$(echo "${i:3}" | sed 's/[^^]/[&]/g; s/\^/\\^/g')
  l=`grep -roah "  $esc\b" ../mathlib3port | wc -w`
  echo "$l ${i:0:3} ${i:3}"
done

digama0 avatar Sep 23 '22 00:09 digama0

Should we move this tracking to a wiki page, similar to https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status ?

That would lower the chances of edit conflicts. Currently I think if there are parallel edits to the comment then it's "last submission wins".

dwrensha avatar Nov 15 '22 16:11 dwrensha

does the wiki have better edit conflict resolution? It's still not using git merge, is it?

digama0 avatar Nov 15 '22 21:11 digama0

Ah, according to https://stackoverflow.com/questions/10553085/how-does-github-merge-web-based-wiki-edits-with-ones-through-the-repository it's last-edit-wins there too (or at least was as of 2014).

dwrensha avatar Nov 15 '22 21:11 dwrensha

I've just updated the list above, per the discussion in the 2023-06-27 porting meeting. Our discussion only got to refine_struct (lots has been deleted above that!), so we should resume this sometime.

I've also removed everything which was checked off, to declutter the list, per the meeting.

kim-em avatar Jun 26 '23 23:06 kim-em

fail_if_success? seems the mistake for fail_if_success.

Komyyy avatar Jul 13 '23 14:07 Komyyy

@semorrison You changed the difficulty of cc from B to S. Can you tell me how to port this tactic easily?

Komyyy avatar Jul 15 '23 04:07 Komyyy

S means that we are not planning on porting it for mathlib, at least in the first pass, because mathlib doesn't use it enough and we can just avoid it. It is still on the list because it is still a todo item, just not high priority.

digama0 avatar Jul 15 '23 06:07 digama0