-
Notifications
You must be signed in to change notification settings - Fork 310
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
tactic porting tracking issue #430
Comments
I have included information about open PRs, but have not yet gone back through all zulip threads to note other "claims". |
I won't have time to work on porting for the next couple of months, sorry; please consider |
@hrmacbeth, thanks for mentioning that! I'll take up |
Now that the semester has begun at Carnegie Mellon, I am also pretty buried. I don't mind keeping the |
Here is the result of a text search for tactic names in
long tail
replication
words.txt
#!/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 |
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". |
does the wiki have better edit conflict resolution? It's still not using git merge, is it? |
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). |
I've just updated the list above, per the discussion in the 2023-06-27 porting meeting. Our discussion only got to I've also removed everything which was checked off, to declutter the list, per the meeting. |
|
@semorrison You changed the difficulty of |
|
According to git blame, PR #430 on mathlib(3) introduced this.
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 requiredB
: Hard, because it is a big and complicated tacticS
: Possibly easy, because we can just stub it out or replace with something else?
: uncategorizedN
parameter
S
abstract
B
cc
cc
tactic (3/3) #5938M
unfold_projs
N
try_for
S
clean
S
refine_struct
refine'
with built-in..
syntax, e.g.refine' { x := 0, y := 1 .. }
M
match_hyp
N
field
/S
have_field
/S
apply_field
M
h_generalize
M
congrm
congr(...)
congruence quotations and portcongrm
tactic #2544E
ac_change
ac_change
tactic #5869M
decide!
M
delta_instance
M
generalizes
B
itauto
itauto
from lean 3 #9398B
obviously
M
assoc_rw
S
dsimp_result
/N
simp_result
M
trunc_cases
E
apply_normed
M
mono
B
ac_mono
M
unfold_cases
B
equiv_rw
N
nth_rw
nth_rewrite
#823, although this doesn't actually reproduce the mathlib3 behaviourM
compute_degree_le
feat: Add tactic[Merged by Bors] - feat: tacticcompute_degree_le
#5882compute_degree
#6221M
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
pure_coherence
/M
coherence
conv
mode)E
[norm_num
][norm_num-conv] /E
[norm_num1
][norm_num1-conv]@bollu claimed thisis no longer working on it?
protect_proj
protected
can be used for constructors.M
notation_class
M
mono
N
add_tactic_doc
N
mk_simp_attribute
M
add_hint_tactic
@Komyyy PR'd as feat: port tactichint
#5363register_hint
N
def_replacer
M
reassoc_axiom
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.
S
intro
/S
intro!
S
propagate_tags
?
quote
/?
pquote
/?
ppquote
S
mapply
S
destruct
S
rsimp
S
comp_val
decide
.S
async
S
continue
S
extract_goal
extract_goal
tactic #4595S
revert_deps
S
revert_after
S
revert_target_deps
S
rcases?
S
rintro?
S
hint
@Komyyy PR'd as feat: port tactichint
#5363S
clarify
/S
safe
/S
finish
S
cases''
/S
induction''
S
pretty_cases
S
suggest
S
omega
S
transport
S
rw_search
rw_search
tactic #6120S
mk_decorations
S
mv_bisim
S
subtype_instance
S
elide
/S
unelide
S
guard_tags
S
guard_proof_term
S
fail_if_success
S
setup_tactic_parser
?
and*
notations for sytaxes are available without a command.S
#list_unused_decls
S
#simp
S
#where
S
#sample
The text was updated successfully, but these errors were encountered: