leanproject --port-complete

Stream: mathlib4

[Scott Morrison]

I wrote something for leanproject that lists all files which are both ported, and all of whose downstream dependencies are ported. (PR soon). These are files which we can "disconnect" from mathlib3, so that people can start work again. I think this is important to do, as many people are ready to get moving!

The current list is actually impressively long, I wouldn't have guessed it. In fact it is longer than the zulip limit, two messages to follow. :-)

[Scott Morrison]

algebra.algebra.unitization
algebra.category.Group.injective
algebra.category.Group.zero
algebra.category.Module.tannaka
algebra.char_p.local_ring
algebra.char_p.mixed_char_zero
algebra.field.power
algebra.free_monoid.count
algebra.gcd_monoid.div
algebra.group.conj_finite
algebra.group.unique_prods
algebra.group.with_one.units
algebra.hierarchy_design
algebra.hom.centroid
algebra.homology.augment
algebra.homology.flip
algebra.homology.functor
algebra.module.bimodule
algebra.module.injective
algebra.module.pointwise_pi
algebra.monoid_algebra.degree
algebra.monoid_algebra.ideal
algebra.monoid_algebra.no_zero_divisors
algebra.monoid_algebra.to_direct_sum
algebra.order.algebra
algebra.order.field.pi
algebra.order.group.densely_ordered
algebra.order.group.prod
algebra.order.monoid.to_mul_bot
algebra.order.positive.field
algebra.order.ring.cone
algebra.order.sub.basic
algebra.order.upper_lower
algebra.quandle
algebra.regular.pow
algebra.ring.order_synonym
algebra.star.chsh
algebra.star.free
algebra.tropical.basic
algebra.tropical.big_operators
algebra.tropical.lattice
algebraic_topology.dold_kan.compatibility
algebraic_topology.dold_kan.decomposition
algebraic_topology.dold_kan.degeneracies
algebraic_topology.dold_kan.equivalence_additive
algebraic_topology.dold_kan.faces
algebraic_topology.dold_kan.functor_gamma
algebraic_topology.dold_kan.functor_n
algebraic_topology.dold_kan.gamma_comp_n
algebraic_topology.dold_kan.homotopies
algebraic_topology.dold_kan.homotopy_equivalence
algebraic_topology.dold_kan.n_comp_gamma
algebraic_topology.dold_kan.n_reflects_iso
algebraic_topology.dold_kan.normalized
algebraic_topology.dold_kan.notations
algebraic_topology.dold_kan.p_infty
algebraic_topology.dold_kan.projections
algebraic_topology.dold_kan.split_simplicial_object
algebraic_topology.nerve
algebraic_topology.split_simplicial_object
analysis.complex.operator_norm
analysis.convex.body
analysis.convex.caratheodory
analysis.convex.extrema
analysis.convex.independent
analysis.convex.join
analysis.convex.quasiconvex
analysis.convex.simplicial_complex.basic
analysis.convex.stone_separation
analysis.hofer
analysis.locally_convex.continuous_of_bounded
analysis.normed.group.controlled_closure
analysis.normed.order.upper_lower
analysis.normed.ring.seminorm
analysis.normed_space.M_structure
analysis.normed_space.banach_steinhaus
analysis.normed_space.compact_operator
analysis.normed_space.int
analysis.normed_space.mazur_ulam
analysis.special_functions.log.monotone
analysis.special_functions.polynomials
analysis.special_functions.trigonometric.chebyshev
analysis.subadditive
category_theory.abelian.generator
category_theory.abelian.subobject
category_theory.action
category_theory.adjunction.adjoint_functor_theorems
category_theory.adjunction.over
category_theory.adjunction.whiskering
category_theory.category.Cat.limit
category_theory.category.Quiv
category_theory.category.Rel
category_theory.category.Twop
category_theory.category.galois_connection
category_theory.cofiltered_system
category_theory.connected_components
category_theory.core
category_theory.endofunctor.algebra
category_theory.generator
category_theory.grothendieck
category_theory.groupoid.free_groupoid
category_theory.idempotents.biproducts
category_theory.idempotents.functor_extension
category_theory.idempotents.homological_complex
category_theory.idempotents.karoubi_karoubi
category_theory.idempotents.simplicial_object
category_theory.limits.constructions.filtered
category_theory.limits.constructions.weakly_initial
category_theory.limits.essentially_small
category_theory.limits.full_subcategory
category_theory.limits.mono_coprod
category_theory.limits.pi
category_theory.limits.preserves.opposites
category_theory.limits.shapes.disjoint_coproduct
category_theory.limits.shapes.wide_equalizers
category_theory.limits.small_complete
category_theory.localization.construction
category_theory.localization.opposite
category_theory.localization.predicate
category_theory.monad.products
category_theory.monoidal.tor
category_theory.noetherian
category_theory.preadditive.eilenberg_moore
category_theory.preadditive.endo_functor
category_theory.preadditive.generator
category_theory.preadditive.hom_orthogonal
category_theory.preadditive.of_biproducts
category_theory.products.associator
category_theory.sigma.basic
category_theory.sites.adjunction
category_theory.sites.induced_topology
category_theory.subobject.comma
category_theory.subobject.types
category_theory.sums.associator
category_theory.sums.basic
category_theory.triangulated.basic
category_theory.triangulated.pretriangulated
category_theory.triangulated.rotate
category_theory.triangulated.triangulated
combinatorics.additive.e_transform
combinatorics.additive.energy
combinatorics.additive.pluennecke_ruzsa
combinatorics.additive.ruzsa_covering
combinatorics.catalan
combinatorics.colex
combinatorics.configuration
combinatorics.double_counting
combinatorics.hales_jewett
combinatorics.hall.basic
combinatorics.hall.finite
combinatorics.hindman
combinatorics.quiver.arborescence
combinatorics.set_family.compression.down
combinatorics.set_family.compression.uv
combinatorics.set_family.harris_kleitman
combinatorics.set_family.intersecting
combinatorics.set_family.kleitman
combinatorics.set_family.lym
combinatorics.set_family.shadow
combinatorics.simple_graph.acyclic
combinatorics.simple_graph.adj_matrix
combinatorics.simple_graph.clique
combinatorics.simple_graph.coloring
combinatorics.simple_graph.connectivity
combinatorics.simple_graph.degree_sum
combinatorics.simple_graph.ends.defs
combinatorics.simple_graph.ends.properties
combinatorics.simple_graph.finsubgraph
combinatorics.simple_graph.hasse
combinatorics.simple_graph.inc_matrix
combinatorics.simple_graph.matching
combinatorics.simple_graph.metric
combinatorics.simple_graph.partition
combinatorics.simple_graph.prod
combinatorics.simple_graph.strongly_regular
combinatorics.simple_graph.subgraph
combinatorics.simple_graph.trails
combinatorics.simple_graph.triangle.basic
combinatorics.young.semistandard_tableau
combinatorics.young.young_diagram
computability.DFA
computability.NFA
computability.ackermann
computability.epsilon_NFA
computability.halting
computability.language
computability.partrec
computability.partrec_code
computability.primrec
computability.reduce
computability.regular_expressions
computability.tm_computable
computability.tm_to_partrec
computability.turing_machine
control.fix
control.fold
control.lawful_fix
data.W.cardinal
data.W.constructions
data.analysis.filter
data.analysis.topology
data.bool.all_any
data.bool.count
data.complex.cardinality
data.complex.determinant
data.countable.small
data.dfinsupp.interval
data.dfinsupp.lex
data.dfinsupp.multiset
data.dfinsupp.ne_locus
data.dfinsupp.order
data.dfinsupp.well_founded
data.dlist.instances
data.erased
data.fin.succ_pred
data.fin.tuple.bubble_sort_induction
data.fin.tuple.monotone
data.fin.tuple.nat_antidiagonal
data.fin.tuple.reflection
data.fin.tuple.sort
data.fin_enum
data.finmap
data.finset.functor
data.finset.interval
data.finset.pi_induction
data.finset.pimage
data.finset.slice
data.finset.sups
data.finset.sym
data.finsupp.alist
data.finsupp.big_operators
data.finsupp.lex
data.finsupp.ne_locus
data.finsupp.pointwise
data.finsupp.well_founded
data.fintype.card_embedding
data.fintype.small
data.fp.basic
data.fun_like.fintype
data.holor
data.int.conditionally_complete_order
data.int.dvd.pow
data.int.nat_prime
data.list.alist
data.list.destutter
data.list.func
data.list.intervals
data.list.lemmas
data.list.rdrop
data.list.sections
data.list.to_finsupp
data.matrix.dual_number
data.matrix.hadamard
data.matrix.kronecker
data.matrix.rank
data.matrix.reflection
data.multiset.fintype
data.multiset.functor
data.multiset.interval
data.multiset.locally_finite
data.multiset.sections
data.mv_polynomial.comap
data.mv_polynomial.division
data.nat.choose.bounds
data.nat.choose.multinomial
data.nat.even_odd_rec
data.nat.factorial.big_operators
data.nat.factorial.double_factorial
data.nat.hyperoperation
data.nat.upto
data.num.prime
data.pfunctor.multivariate.W
data.pi.interval
data.pnat.factors
data.pnat.find
data.pnat.xgcd
data.polynomial.laurent
data.polynomial.partial_fractions
data.psigma.order
data.qpf.multivariate.constructions.comp
data.qpf.multivariate.constructions.const
data.qpf.multivariate.constructions.fix
data.qpf.multivariate.constructions.prj
data.qpf.multivariate.constructions.quot
data.qpf.multivariate.constructions.sigma
data.qpf.univariate.basic
data.rat.nnrat
data.real.enat_ennreal
data.real.hyperreal
data.semiquot
data.seq.parallel
data.seq.wseq
data.set.enumerate
data.set.intervals.ord_connected_component
data.set.intervals.surj_on
data.set.intervals.with_bot_top
data.set.opposite
data.set.sups
data.setoid.partition
data.sigma.interval
data.sigma.lex
data.sigma.order
data.sum.interval
data.sym.card
data.two_pointing
data.vector.mem
data.vector.zip
data.zmod.coprime
data.zmod.parity
deprecated.group
deprecated.ring
deprecated.subfield
deprecated.subgroup
deprecated.submonoid
deprecated.subring

[Scott Morrison]

dynamics.circle.rotation_number.translation_number
dynamics.flow
dynamics.omega_limit
group_theory.commensurable
group_theory.commuting_probability
group_theory.double_coset
group_theory.eckmann_hilton
group_theory.free_abelian_group_finsupp
group_theory.free_product
group_theory.group_action.embedding
group_theory.group_action.option
group_theory.group_action.sigma
group_theory.group_action.sum
group_theory.group_action.support
group_theory.is_free_group
group_theory.nielsen_schreier
group_theory.perm.cycle.concrete
group_theory.presented_group
group_theory.semidirect_product
group_theory.specific_groups.alternating
group_theory.subgroup.saturated
group_theory.subsemigroup.membership
information_theory.hamming
linear_algebra.affine_space.matrix
linear_algebra.affine_space.pointwise
linear_algebra.cross_product
linear_algebra.free_algebra
linear_algebra.lagrange
linear_algebra.matrix.circulant
linear_algebra.matrix.dot_product
linear_algebra.matrix.finite_dimensional
linear_algebra.matrix.invariant_basis_number
linear_algebra.matrix.is_diag
linear_algebra.matrix.orthogonal
linear_algebra.multilinear.finite_dimensional
linear_algebra.projective_space.basic
linear_algebra.projective_space.independence
linear_algebra.projective_space.subspace
linear_algebra.tensor_product.matrix
logic.equiv.embedding
logic.hydra
measure_theory.card_measurable_space
measure_theory.decomposition.unsigned_hahn
measure_theory.function.floor
model_theory.definability
model_theory.order
number_theory.ADE_inequality
number_theory.fermat4
number_theory.frobenius_number
number_theory.lucas_lehmer
number_theory.lucas_primality
number_theory.multiplicity
number_theory.pythagorean_triples
number_theory.zsqrtd.to_real
order.category.Frm
order.concept
order.countable_dense_linear_order
order.extension.linear
order.extension.well
order.filter.filter_product
order.filter.modeq
order.filter.partial
order.grade
order.height
order.heyting.boundary
order.heyting.regular
order.ideal
order.ord_continuous
order.pfilter
order.prime_ideal
order.rel_iso.group
order.semiconj_Sup
order.succ_pred.interval_succ
order.succ_pred.linear_locally_finite
order.upper_lower.hom
order.upper_lower.locally_finite
probability.cond_count
probability.conditional_probability
representation_theory.maschke
ring_theory.fintype
ring_theory.flat
ring_theory.ideal.associated_prime
ring_theory.ideal.idempotent_fg
ring_theory.ideal.minimal_prime
ring_theory.mv_polynomial.homogeneous
ring_theory.mv_polynomial.ideal
ring_theory.mv_polynomial.weighted_homogeneous
ring_theory.non_unital_subsemiring.basic
ring_theory.ore_localization.basic
ring_theory.ore_localization.ore_set
ring_theory.polynomial.opposites
ring_theory.ring_invo
ring_theory.valuation.quotient
ring_theory.zmod
set_theory.lists
set_theory.ordinal.cantor_normal_form
set_theory.ordinal.topology
set_theory.zfc.basic
set_theory.zfc.ordinal
topology.algebra.equicontinuity
topology.algebra.localization
topology.algebra.module.linear_pmap
topology.algebra.nonarchimedean.adic_topology
topology.algebra.order.filter
topology.algebra.order.t5
topology.algebra.order.upper_lower
topology.algebra.semigroup
topology.category.Born
topology.category.CompHaus.projective
topology.category.Locale
topology.category.Profinite.as_limit
topology.category.Profinite.projective
topology.continuous_function.locally_constant
topology.continuous_function.t0_sierpinski
topology.covering
topology.extremally_disconnected
topology.filter
topology.hom.open
topology.is_locally_homeomorph
topology.list
topology.locally_constant.algebra
topology.metric_space.infsep
topology.metric_space.shrinking_lemma
topology.omega_complete_partial_order
topology.order.lower_topology
topology.order.priestley
topology.partial
topology.sets.order
topology.sheaves.abelian
topology.uniform_space.absolute_value
topology.uniform_space.compare_reals

[Scott Morrison]

We need to write some CI, now.

1. files on this list should have a different warning in their mathlib3 header, warning that any further changes to these files in mathlib3 will not be forwarded ported (i.e. will effectively be dropped completely), and that the mathlib4 files might already have been modified.
2. probably CI should alert the author of any mathlib3 PR touching one of these files that they should reconsider. :-)

[Scott Morrison]

leanproject PR at https://github.com/leanprover-community/mathlib-tools/pull/163 (@Patrick Massot?)

[Eric Wieser]

This also has the effect that import refactors in mathlib3 are no longer allowed to add new imports of these files, as that would reconnect them to unported files

[Eric Wieser]

(which I know at least one open mathlib3 PR does)

[Yaël Dillies]

Not just import refactors. algebra.order.upper_lower and analysis.normed.order.upper_lower were PRed as prerequisites to measure_theory.order.upper_lower, which hasn't made it yet to master (#16976).

[Yaël Dillies]

For that reason, I don't think the list you just sent is particularly meaningful, Scott.

[Scott Morrison]

I mean, we could also just not worry? It's a one-way process, marking a file as "abandoned", and it's happening to all of the files sooner or later. Why would it matter if we mark a mathlib3 file as abandoned, and then have to add an import to it so that it again depends on unported files? I'd be happy to look at the example you have in mind.

[Yaël Dillies]

A more meaningful measure would be "files whose dependents are all ported, and no open PR to mathlib3 modifies them". Then it would make more obvious that we should take care of the open PRs!

[Scott Morrison]

I think that has been obvious for a year now. :-)

[Scott Morrison]

Unfortunately it's much harder to implement the "and no open PR to mathlib3 modifies them" condition. If you'd like to do it, that would be helpful.

[Scott Morrison]

@Yaël Dillies, I'm sorry I don't understand your example above about upper_lower? (I haven't looked at the PR.) Could you explain which file on my list you think it would be problematic to mark as abandoned, and why?

[Eric Wieser]

Scott Morrison said:

Why would it matter if we mark a mathlib3 file as abandoned, and then have to add an import to it so that it again depends on unported files? I'd be happy to look at the example you have in mind.

The example I'm thinking of is a non-abandoned file gaining an import abandoned_file, which results in the file not actually being abandoned after all

[Yaël Dillies]

algebra.order.upper_lower and analysis.normed.order.upper_lower are in your list but won't be anymore once #16976 is in. They're "abandoned" only because the sequence of PRs that leads to measure_theory.order.upper_lower hasn't fully entered mathlib yet.

[Scott Morrison]

Okay, but I don't really see what goes wrong? They no longer satisfy the proposed condition for adding the "no backporting required" / "further changes may be lost" labels, but they can still have those labels, right?

[Eric Wieser]

Well then it sounds like applying those labels should be a human process rather than an automated one

[Eric Wieser]

Things go wrong if:

• not_abandoned.lean uses declarations from abandoned.lean that have been refactored and removed in mathlib4. Now porting not_abandoned.lean is a mess.
• A change to not_abandoned.leannecessitates a change to abandoned.lean, which now has to be forward-ported even though the label says "changes don't have to be forward-ported".

[Johan Commelin]

I would prefer to just go ahead with Scott's automated solution, and instead figure out a way to use mathport on the open PRs that Yaël is concerned about.

[Johan Commelin]

We're really entering the end game of the port now.

[Eric Wieser]

We're still regularly making changes to mathlib3 in order to speed up or unblock part of the port; I worry that Scott's suggestion is going to make that harder

[Johan Commelin]

Eric Wieser said:

Things go wrong if:

• not_abandoned.lean uses declarations from abandoned.lean that have been refactored and removed in mathlib4. Now porting not_abandoned.lean is a mess.

This is impossible by definition of abandoned.

[Eric Wieser]

Impossible in what way?

[Eric Wieser]

probably CI should alert the author of any mathlib3 PR touching one of these files that they should reconsider

This isn't sufficient to protect against the above; you would also need CI that says "you are not allowed to write import abandoned_file in any other file".

[Eric Wieser]

RIght now it sounds like the definition of "abandoned" is:

• Determined to have no unported dependent files

but the suggested implementation seems to give it the definition

• Determined to have had no unported dependent files at some point in the past

[Johan Commelin]

Yeah, we should just guarantee that once a file is abandoned it stays abandoned.

[Patrick Massot]

@Scott Morrison I merged your leanproject PR. Do you need a pypi release or are you happy to install from source?

[Anatole Dedecker]

I'm fine with locking these files in mathlib3, but I'd say we need a way to port PRs first, otherwise that means that PRs touching these file will need to be ported by hand.

[Eric Wieser]

So what this means is that someone who is working on a file new_stuff.lean that imports:

• abandoned.lean
• 150_files_away_from_being_ported.lean

is unable to do anything with their work until the port is complete; they can't write it in Lean4, but they also can't PR it to mathlib3 as that breaks the proposed rule.

[Eric Wieser]

I think there is definitely an N for which this is a good choice, but 150 seems rather high.

[Scott Morrison]

I'm not sure where the "you may not import abandoned files" rule comes from. I am not proposing that. An author wanting to do that would have to be aware that abandoned.lean may well change by the time their file is being ported, and that they might have to take responsibility themselves for doing the port (which they might achieve by taking responsibility for backporting changes to the imported abandoned file). In particular that file would become "optional" for declaring the port complete, precisely because it was added "too late".

[Scott Morrison]

The point of freely labelling files as "abandoned" is that we need to enable forward progress on mathlib4, and if that comes at the expense of progress on mathlib3, that's a very easy judgement to make! Several people have mentioned here at Banff that they would like to have this freedom when adding new material in mathlib4.

[Scott Morrison]

How about this as the message for mathlib4 files:

/-
All of the mathlib3 dependents of this file have been ported to mathlib4 as of 2023-05-22.
You may make changes to this file and its dependents without needing to backport these changes to mathlib3.
-/

and this for mathlib3:

/-
This file, and all of its downstream dependencies, were ported to mathlib4 as of 2023-05-22.
This file is thus "abandoned", and contributors may make changes in mathlib4
without these changes being backported to mathlib3.

Further, we are not planning on forward porting any further changes to this file,
and so additional changes to this file will be preserved in the deprecated mathlib3 repository
but otherwise lost.

If you would like to add any new files to mathlib3 which depend on this file
(or any "abandoned" file), then you should be aware that:
* it will be considered as optional for declaring the porting process complete
* as such the author takes responsibility for porting it themselves
* they need to be aware that the imported "abandoned" file may have changed in mathlib4
  in the meantime, and that they will need to make changes themselves to adapt to these changes.
-/

[Scott Morrison]

I'd prefer a different word than "abandoned", which I've only been using here for effect. :-)

[Scott Morrison]

Anatole Dedecker said:

I'm fine with locking these files in mathlib3, but I'd say we need a way to port PRs first, otherwise that means that PRs touching these file will need to be ported by hand.

Could someone with a PR all of whose dependencies are ported please try running mathport oneshot and report their experience? I think we have a way to port PRs, at least ones that don't modify existing files. The documentation is a disaster, but we need authors who want to use this to help us fix it.

[Scott Morrison]

I'm planning on updating the documentation to explain how to port projects depending on mathlib, but haven't got there yet!

[Eric Wieser]

We should think carefully about whether it makes sense to include SHAs in these comments, since we forgot to do that last time in mathlib4 and it was occasionally painful.

[Eric Wieser]

(but conversely, we also previously put PR numbers in the mathlib3 comments and that was also painful)

[Joseph Myers]

Does "downstream dependencies" here include such dependencies in archive, counterexamples and test (the first two not yet ported at all; I'm not sure what tracking there is of the porting status of test as a whole or individual files therein)? (I'd guess that not much in archive or counterexamples depends on files listed here, however.)

[Scott Morrison]

I think we're simply not tracking test at all. Hopefully tactic writing are looking through these to bring across suitable test cases. (I've found it useful to bring things across wholesale and leave them commented out even if an initial port of a tactic is not feature complete.)

[Eric Wieser]

I think we should consider files imported by unported files inarchive and counterexamples as ineligible for being considered abandoned

[Eric Wieser]

Because otherwise there's a big risk they rot, and the whole point of having those directories in mathlib was to prevent their contents rotting

[Eric Wieser]

If that means we can't declare anything abandoned until we get mathport CI working on these directories, then I think that's a good thing

[Scott Morrison]

Oh, I was about to say the opposite: to propose that "the porting effort" doesn't include archive and counterexample, and leave this up to individual authors. The goal had always been that in archive the "generally useful results" had to be put directly in mathlib.

[Scott Morrison]

Obviously it would be nice to have them.

[Yaël Dillies]

That's currently wrong, at least. Erdos-Szekeres is in archive even though it's generally useful in combinatorics.

[Patrick Massot]

Yaël, your example should move out of archive if it's useful elsewhere.

[Scott Morrison]

Hmm, that should be fixed asap? :-) If it's not up to standard, then perhaps when it is needed in mathlib someone can just revise it directly into Lean 4.

[Eric Wieser]

What about the freek 100 list?

[Scott Morrison]

They just stay in mathlib3?

[Scott Morrison]

They don't serve any direct purpose beyond getting Lean on the list, and Freek is not going to take them off the list just because Lean 4 arrives?

[Yaël Dillies]

That's... not how an archive works. You can't just throw it all away.

[Scott Morrison]

I mean, authors who would like them in mathlib4 can move them.

[Eric Wieser]

What concerns me is that the motivation for throwing them out seems to just be "oh we haven't told mathport about them"

[Scott Morrison]

We're not planning on deleting mathlib3.

[Anatole Dedecker]

Scott Morrison said:

Oh, I was about to say the opposite: to propose that "the porting effort" doesn't include archive and counterexample, and leave this up to individual authors. The goal had always been that in archive the "generally useful results" had to be put directly in mathlib.

Well the point of having them in mathlib was that they would be kept up to date with mathlib right? Otherwise they would have been in repos depending on (a specific version of) mathlib.

[Scott Morrison]

I mean yes, of course, if there is capacity to port them we can and should, but I'm proposing that nothing wait on them if that capacity is not there.

[Yaël Dillies]

Things in the archive precisely are usually written by newcomers, which might have left the community afterwards. So we can't just rely on authors to port their own work.

[Scott Morrison]

They will still be kept up to date with mathlib3. :-)

[Eric Wieser]

if there is capacity to port them we can and should,

I think we just need capacity from someone CI oriented (@Mario Carneiro?), and then the capacity to port them will appear automatically

[Eric Wieser]

If no one can work out how to use mathport for archives and counterexamples, things aren't looking promising for other downstream lean3 projects.

[Scott Morrison]

I mean yes, of course if someone would like to do this (I would like to do this!) and they find the time, we will bring counterexample and archive along. But I don't think we should stop everyone who is chafing at the bit to add to mathlib4 from doing so because of worries about ease of later porting counterexample and archive!

Planning to "officially" port them comes at a distinct cost.

[Scott Morrison]

After my talk today I will promise to look into doing more in mathport CI. :-) At least I will write up the instructions for porting projects.

[Eric Rodriguez]

is there any examples of people who are waiting for permission to put new stuff in mathlib4? furthermore, is there any of those that desperately can't just put it in a new file? I don't really see why we should throw away a lot of good old work because "we don't want to set up mathport CI"; archive&counterexample porting could also be a really good way to teach new people how to do porting

[Eric Rodriguez]

on the other hand, I can't see these modifications of mathlib4 that can't be done in lean3 likely to cause issues porting these files in the future, either...

[Kevin Buzzard]

I absolutely agree with Scott. Freek does not keep track of version numbers. If we solve other problems in Lean 4 he will just add it to the Lean list. Random Freek list questions are really a necessary part of mathlib. But people will be welcome to port them if they want.

[Eric Rodriguez]

honestly, what I see most are people who really want to get their lean3 projects in before stuff freezes, not new lean4 projects

[Kevin Buzzard]

is there any examples of people who are waiting for permission to put new stuff in mathlib4?

No. Everyone who has asked has been given permission. I have a PhD student developing Krull dimension theory of rings in mathlib4. What we have are examples of people who are using the port as an excuse to wait to PR a huge for_mathlib directory, but they are definitely not waiting for permission.

[Eric Rodriguez]

I worry that those for_mathlib repos will rot forever if we keep not porting them, though...

[Kevin Buzzard]

Yes. But that is also not mathlib4's problem. Mathlib4 is open for business.

[Eric Rodriguez]

I feel like throwing away good old work for the sake of getting the port done some iota faster is just a way to lose maths instead of gain any :/ I still don't see why new development can't just stay in new files, but I do understand that people here who have far more experience disagree

[Kevin Buzzard]

Jujian's development is being done in new files in mathlib4.

[Patrick Massot]

What we are seeing in this thread is that some people care about what's in the archive folder. Why not letting those people do the work of porting this stuff? It's all about priorities. Porting the actual mathlib is the important thing, and non-important things should not hold it off. But people who want to work on less important things are still welcome to do so, that's always been the rule.

[Eric Wieser]

@Eric Rodriguez, new development can't always stay in new files for the same reason as mathlib3 development can't stay in unported files. The tradeoff is between:

• Ask mathlib4 contributors to make all such changes to mathlib3 first, then forward-port them. Nothing in mathlib3 is thrown away, but for these files this is maybe 3x more work.
• Allow the changes to happen in mathlib4 (only). The file is now out of sync and all future work in mathlib3 in these files is thrown away.

[Kevin Buzzard]

And my observation is that given the current rate of porting, the second option is only a few weeks away anyway, so feel free to debate between 1 and 2 but you're just postponing the inevitable.

[David Renshaw]

For what it's worth, I'm maintaining the stuff that I contributed to archive/imo in https://github.com/dwrensha/math-puzzles-in-lean4

[Eric Rodriguez]

I think something that would really ease this pain is an easy way to run mathport for ourselves - I'm currently trying it and it's not only taking a while, but there's issues too (see Floris' comments, too, which I don't think have really changed - it also doesn't run lake exe cache get...

[Eric Rodriguez]

I'd love to do stuff like e.g. #18861 in Mathlib4, but until I can easily port files like https://github.com/leanprover-community/mathlib/blob/little-wedderburn/src/ring_theory/little_wedderburn.lean to Lean4 (or at least roughly), I don't _have a choice_ but to put everything in Mathlib3

[Eric Rodriguez]

I know I'm speaking very personally here, but I have a feeling this is the same for a lot of people - if people could easily run Mathport on their projects, and deal with any fallout easily themselves, it seems far less daunting. The only way for us to get mathport output these days seems to just be "PR it into mathlib3", which then gets more and more demonised by the day...

[Eric Wieser]

Note that there should be a working gitpod container for mathport now; but it still takes a while to start up

[Eric Rodriguez]

Is there instructions/documentation for that? I wasn't even aware of this

[Patrick Massot]

Eric you can still help with the port and then port your new file by hand.

[Eric Rodriguez]

I'm happy to help with the port, and I have been when I can (I just had exams!)

[Eric Wieser]

I don't think there is much documentation on the gitpod setup. Go to http://gitpod.io/#https://github.com/leanprover-community/mathport and you'll get a compatible version of ubuntu with the right dependencies installed. Then you follow the regular readme on how to actually use it

[Anatole Dedecker]

I think that a lot of the fears expressed in this thread (and others before) will go away once we have a good documentation on how to port PR and everyone get convinced that "porting a PR then merging it to mathlib4" is not harder than "rush the PR in mathlib3 then forward-port it". For port-complete files, it is clear that the first one should be the right approach, but currently our whole infrastructure pushes towards the second.

[Mario Carneiro]

Let me just say that I am strongly opposed to abandoning the archive or treating it as a second class citizen here. Things in archive and counterexamples should absolutely count against --port-complete, modulo implementation concerns, and they are part of the port. Like Patrick says, they are at the bottom of the importance hierarchy here, just like so many leaf files in mathlib, but it is absolutely not acceptable to just leave it behind. It's also not reasonable to expect the original authors to do the porting work, as they may have moved on (or worse). We are in no hurry to get the work done, but the port won't be done until those parts are ported.

[Scott Morrison]

So I just had a look at running mathport on archive and counterexamples. It is a bit painful, mostly as it is hard to create a single lean file that imports them all.

An easy fix for this would just be to move archive and counterexamples under src! This would also have the great advantage of making current mathport CI automatically include all the files.

(We could of course plan to move them back out of the Mathlib directory later when the port is done.)

[Eric Rodriguez]

I like this, this is a simple solution that keeps everyone happy :) they may have to be clones as there's some CI that runs against archive/counterexamples iirc

[Eric Rodriguez]

this will also make the numbers smaller temporarily which is a shame

[Mario Carneiro]

Scott Morrison said:

So I just had a look at running mathport on archive and counterexamples. It is a bit painful, mostly as it is hard to create a single lean file that imports them all.

An easy fix for this would just be to move archive and counterexamples under src! This would also have the great advantage of making current mathport CI automatically include all the files.

How will that fix the "hard to create a single lean file that imports them all" problem? I think it would be better to have archive and counterexamples be separate lake packages also hosted in the mathlib repo, assuming we can solve the importing problem.

We have two directions there: we could try to fix that by a mathlib3 refactor to wrap everything in namespaces, or we could adjust the lake package setup so that we don't assume a single file can import everything (which is a more advanced configuration but IIUC possible to do). For mathport, you can specify many top level roots by passing them on the command line via xargs or a script.

[Scott Morrison]

The problem is just that in a Lean 3 project we can't import files outside of src.

[Scott Morrison]

I'm trying this out on #19074.

[Joseph Myers]

Namespacing for archive and counterexamples was done a few months ago to the extent required to be able to import all the files together, in order to generate documentation for them (#18388).

[Joseph Myers]

Along with mathport CI to generate ported versions of archive and counterexamples, it would be good to get the mathlib4 CI set up for wherever those files are meant to end up in mathlib4 (which is probably a no-op if they go under Mathlib/, maybe more work if they go somewhere else in the mathlib4 repository) - as that CI seems important to have before ported versions of archive and counterexamples files start getting added, to make sure that the ports keep working after they are added. Having that CI in mathlib4 would also allow people to add new archive / counterexamples files to mathlib4 with no mathlib3 version, should anyone wish to do so at this stage, as well as allowing people to start adding ported files there. Thus the CI (which potentially unblocks other work) seems like it should be higher priority than the actual porting of existing files from archive / counterexamples (which nothing depends on).

[Scott Morrison]

I have a branch in which I've consistently namespaced everything in archive and counterexamples. Let's wait on #19074 to deploy it.

[Scott Morrison]

The leanproject port-complete list has shrunk a bit, now counting dependencies via archive and counterexamples:

algebra.algebra.unitization
algebra.algebraic_card
algebra.category.Group.injective
algebra.category.Group.zero
algebra.category.GroupWithZero
algebra.category.Module.tannaka
algebra.char_p.local_ring
algebra.char_p.mixed_char_zero
algebra.dual_quaternion
algebra.field.power
algebra.free_monoid.count
algebra.gcd_monoid.div
algebra.group.with_one.units
algebra.hierarchy_design
algebra.hom.centroid
algebra.homology.augment
algebra.homology.flip
algebra.homology.functor
algebra.module.bimodule
algebra.module.injective
algebra.module.pointwise_pi
algebra.monoid_algebra.degree
algebra.monoid_algebra.ideal
algebra.monoid_algebra.no_zero_divisors
algebra.monoid_algebra.to_direct_sum
algebra.order.algebra
algebra.order.field.pi
algebra.order.group.densely_ordered
algebra.order.group.prod
algebra.order.monoid.to_mul_bot
algebra.order.positive.field
algebra.order.ring.cone
algebra.order.sub.basic
algebra.order.upper_lower
algebra.quandle
algebra.regular.pow
algebra.ring.order_synonym
algebra.star.chsh
algebra.star.free
algebra.tropical.basic
algebra.tropical.big_operators
algebra.tropical.lattice
algebraic_topology.dold_kan.compatibility
algebraic_topology.dold_kan.decomposition
algebraic_topology.dold_kan.degeneracies
algebraic_topology.dold_kan.equivalence_additive
algebraic_topology.dold_kan.faces
algebraic_topology.dold_kan.functor_gamma
algebraic_topology.dold_kan.functor_n
algebraic_topology.dold_kan.gamma_comp_n
algebraic_topology.dold_kan.homotopies
algebraic_topology.dold_kan.homotopy_equivalence
algebraic_topology.dold_kan.n_comp_gamma
algebraic_topology.dold_kan.n_reflects_iso
algebraic_topology.dold_kan.normalized
algebraic_topology.dold_kan.notations
algebraic_topology.dold_kan.p_infty
algebraic_topology.dold_kan.projections
algebraic_topology.dold_kan.split_simplicial_object
algebraic_topology.nerve
algebraic_topology.split_simplicial_object
analysis.complex.operator_norm
analysis.convex.body
analysis.convex.caratheodory
analysis.convex.extrema
analysis.convex.independent
analysis.convex.join
analysis.convex.quasiconvex
analysis.convex.simplicial_complex.basic
analysis.convex.stone_separation
analysis.hofer
analysis.locally_convex.continuous_of_bounded
analysis.locally_convex.strong_topology
analysis.normed.group.controlled_closure
analysis.normed.order.upper_lower
analysis.normed.ring.seminorm
analysis.normed_space.M_structure
analysis.normed_space.banach_steinhaus
analysis.normed_space.compact_operator
analysis.normed_space.int
analysis.normed_space.mazur_ulam
analysis.special_functions.log.monotone
analysis.special_functions.polynomials
analysis.special_functions.trigonometric.chebyshev
analysis.subadditive
category_theory.abelian.generator
category_theory.abelian.subobject
category_theory.action
category_theory.adjunction.adjoint_functor_theorems
category_theory.adjunction.over
category_theory.adjunction.whiskering
category_theory.category.Cat.limit
category_theory.category.Quiv
category_theory.category.Rel
category_theory.category.Twop
category_theory.category.galois_connection
category_theory.cofiltered_system
category_theory.connected_components
category_theory.core
category_theory.endofunctor.algebra
category_theory.generator
category_theory.grothendieck
category_theory.groupoid.free_groupoid
category_theory.idempotents.biproducts
category_theory.idempotents.functor_extension
category_theory.idempotents.homological_complex
category_theory.idempotents.karoubi_karoubi
category_theory.idempotents.simplicial_object
category_theory.limits.constructions.filtered
category_theory.limits.constructions.weakly_initial
category_theory.limits.essentially_small
category_theory.limits.full_subcategory
category_theory.limits.mono_coprod
category_theory.limits.pi
category_theory.limits.preserves.opposites
category_theory.limits.shapes.disjoint_coproduct
category_theory.limits.shapes.wide_equalizers
category_theory.limits.small_complete
category_theory.localization.construction
category_theory.localization.opposite
category_theory.localization.predicate
category_theory.monad.products
category_theory.monoidal.tor
category_theory.noetherian
category_theory.preadditive.eilenberg_moore
category_theory.preadditive.endo_functor
category_theory.preadditive.generator
category_theory.preadditive.hom_orthogonal
category_theory.preadditive.of_biproducts
category_theory.products.associator
category_theory.sigma.basic
category_theory.sites.adjunction
category_theory.sites.induced_topology
category_theory.subobject.comma
category_theory.subobject.types
category_theory.sums.associator
category_theory.sums.basic
category_theory.triangulated.basic
category_theory.triangulated.pretriangulated
category_theory.triangulated.rotate
category_theory.triangulated.triangulated
combinatorics.additive.e_transform
combinatorics.additive.energy
combinatorics.additive.pluennecke_ruzsa
combinatorics.additive.ruzsa_covering
combinatorics.catalan
combinatorics.colex
combinatorics.configuration
combinatorics.double_counting
combinatorics.hales_jewett
combinatorics.hall.basic
combinatorics.hall.finite
combinatorics.hindman
combinatorics.quiver.arborescence
combinatorics.set_family.compression.down
combinatorics.set_family.compression.uv
combinatorics.set_family.harris_kleitman
combinatorics.set_family.intersecting
combinatorics.set_family.kleitman
combinatorics.set_family.lym
combinatorics.set_family.shadow
combinatorics.simple_graph.acyclic
combinatorics.simple_graph.clique
combinatorics.simple_graph.coloring
combinatorics.simple_graph.degree_sum
combinatorics.simple_graph.ends.defs
combinatorics.simple_graph.ends.properties
combinatorics.simple_graph.finsubgraph
combinatorics.simple_graph.hasse
combinatorics.simple_graph.inc_matrix
combinatorics.simple_graph.matching
combinatorics.simple_graph.metric
combinatorics.simple_graph.partition
combinatorics.simple_graph.prod
combinatorics.simple_graph.strongly_regular
combinatorics.simple_graph.triangle.basic
combinatorics.young.semistandard_tableau
combinatorics.young.young_diagram
computability.DFA
computability.NFA
computability.ackermann
computability.epsilon_NFA
computability.halting
computability.language
computability.partrec
computability.partrec_code
computability.primrec
computability.reduce
computability.regular_expressions
computability.tm_computable
computability.tm_to_partrec
computability.turing_machine
control.fix
control.fold
control.lawful_fix
data.W.cardinal
data.W.constructions
data.analysis.filter
data.analysis.topology
data.bool.all_any
data.bool.count
data.complex.cardinality
data.complex.determinant
data.countable.small
data.dfinsupp.interval
data.dfinsupp.multiset
data.dfinsupp.well_founded
data.dlist.instances
data.erased
data.fin.succ_pred
data.fin.tuple.bubble_sort_induction
data.fin.tuple.monotone
data.fin.tuple.reflection
data.fin.tuple.sort
data.fin_enum
data.finmap
data.finset.functor
data.finset.interval
data.finset.pi_induction
data.finset.pimage
data.finset.slice
data.finset.sups
data.finset.sym
data.finsupp.alist
data.finsupp.big_operators
data.finsupp.ne_locus
data.finsupp.pointwise
data.finsupp.well_founded
data.fintype.small
data.fp.basic
data.fun_like.fintype
data.holor
data.int.conditionally_complete_order
data.int.dvd.pow
data.list.alist
data.list.destutter
data.list.func
data.list.intervals
data.list.lemmas
data.list.rdrop
data.list.sections
data.list.to_finsupp
data.matrix.dual_number
data.matrix.hadamard
data.matrix.kronecker
data.matrix.rank
data.matrix.reflection
data.multiset.fintype
data.multiset.functor
data.multiset.interval
data.multiset.locally_finite
data.multiset.sections
data.mv_polynomial.comap
data.mv_polynomial.division
data.nat.choose.bounds
data.nat.choose.multinomial
data.nat.even_odd_rec
data.nat.factorial.big_operators
data.nat.factorial.double_factorial
data.nat.hyperoperation
data.nat.upto
data.num.prime
data.pfunctor.multivariate.W
data.pi.interval
data.pnat.factors
data.pnat.find
data.pnat.xgcd
data.polynomial.laurent
data.polynomial.partial_fractions
data.psigma.order
data.qpf.multivariate.constructions.comp
data.qpf.multivariate.constructions.const
data.qpf.multivariate.constructions.fix
data.qpf.multivariate.constructions.prj
data.qpf.multivariate.constructions.quot
data.qpf.multivariate.constructions.sigma
data.qpf.univariate.basic
data.rat.nnrat
data.real.enat_ennreal
data.real.hyperreal
data.semiquot
data.seq.parallel
data.seq.wseq
data.set.enumerate
data.set.intervals.ord_connected_component
data.set.intervals.surj_on
data.set.intervals.with_bot_top
data.set.opposite
data.set.sups
data.setoid.partition
data.sigma.interval
data.sigma.lex
data.sigma.order
data.sum.interval
data.sym.card
data.two_pointing
data.vector.mem
data.vector.zip
data.zmod.coprime
data.zmod.parity
deprecated.group
deprecated.ring
deprecated.subfield
deprecated.subgroup
deprecated.submonoid
deprecated.subring

[Scott Morrison]

dynamics.circle.rotation_number.translation_number
dynamics.ergodic.conservative
dynamics.flow
dynamics.omega_limit
field_theory.ax_grothendieck
group_theory.commensurable
group_theory.commuting_probability
group_theory.double_coset
group_theory.eckmann_hilton
group_theory.free_abelian_group_finsupp
group_theory.free_product
group_theory.group_action.embedding
group_theory.group_action.option
group_theory.group_action.sigma
group_theory.group_action.sum
group_theory.group_action.support
group_theory.is_free_group
group_theory.nielsen_schreier
group_theory.perm.cycle.concrete
group_theory.presented_group
group_theory.semidirect_product
group_theory.specific_groups.alternating
group_theory.subgroup.saturated
group_theory.subsemigroup.membership
information_theory.hamming
linear_algebra.affine_space.matrix
linear_algebra.affine_space.pointwise
linear_algebra.annihilating_polynomial
linear_algebra.bilinear_form.tensor_product
linear_algebra.cross_product
linear_algebra.free_algebra
linear_algebra.lagrange
linear_algebra.matrix.circulant
linear_algebra.matrix.dot_product
linear_algebra.matrix.dual
linear_algebra.matrix.finite_dimensional
linear_algebra.matrix.invariant_basis_number
linear_algebra.matrix.is_diag
linear_algebra.matrix.orthogonal
linear_algebra.multilinear.finite_dimensional
linear_algebra.projective_space.basic
linear_algebra.projective_space.independence
linear_algebra.projective_space.subspace
linear_algebra.tensor_product.matrix
logic.hydra
measure_theory.card_measurable_space
measure_theory.decomposition.unsigned_hahn
measure_theory.function.floor
measure_theory.function.special_functions.is_R_or_C
measure_theory.integral.lebesgue_normed_space
measure_theory.integral.riesz_markov_kakutani
model_theory.definability
model_theory.order
number_theory.ADE_inequality
number_theory.fermat4
number_theory.frobenius_number
number_theory.lucas_primality
number_theory.multiplicity
number_theory.pythagorean_triples
number_theory.zsqrtd.to_real
order.category.Frm
order.concept
order.countable_dense_linear_order
order.extension.linear
order.extension.well
order.filter.filter_product
order.filter.modeq
order.filter.partial
order.grade
order.height
order.heyting.boundary
order.heyting.regular
order.ideal
order.ord_continuous
order.pfilter
order.prime_ideal
order.rel_iso.group
order.semiconj_Sup
order.succ_pred.interval_succ
order.succ_pred.linear_locally_finite
order.upper_lower.hom
order.upper_lower.locally_finite
representation_theory.maschke
ring_theory.flat
ring_theory.henselian
ring_theory.ideal.associated_prime
ring_theory.ideal.idempotent_fg
ring_theory.ideal.minimal_prime
ring_theory.mv_polynomial.homogeneous
ring_theory.mv_polynomial.ideal
ring_theory.mv_polynomial.weighted_homogeneous
ring_theory.non_unital_subsemiring.basic
ring_theory.ore_localization.basic
ring_theory.ore_localization.ore_set
ring_theory.polynomial.opposites
ring_theory.ring_invo
ring_theory.valuation.quotient
ring_theory.zmod
set_theory.lists
set_theory.ordinal.cantor_normal_form
set_theory.ordinal.topology
set_theory.zfc.basic
set_theory.zfc.ordinal
topology.algebra.equicontinuity
topology.algebra.localization
topology.algebra.module.linear_pmap
topology.algebra.nonarchimedean.adic_topology
topology.algebra.order.filter
topology.algebra.order.t5
topology.algebra.order.upper_lower
topology.algebra.semigroup
topology.category.Born
topology.category.CompHaus.projective
topology.category.Locale
topology.category.Profinite.as_limit
topology.category.Profinite.projective
topology.continuous_function.locally_constant
topology.continuous_function.t0_sierpinski
topology.covering
topology.extremally_disconnected
topology.filter
topology.hom.open
topology.is_locally_homeomorph
topology.list
topology.locally_constant.algebra
topology.metric_space.infsep
topology.metric_space.shrinking_lemma
topology.omega_complete_partial_order
topology.order.lower_topology
topology.order.priestley
topology.partial
topology.sets.order
topology.sheaves.abelian
topology.uniform_space.absolute_value
topology.uniform_space.compare_reals

[Scott Morrison]

Oh! Actually, it made essentially no difference. The list is 5 items shorter now. :-)

[Mario Carneiro]

what do we have to do to get it in the port-progress output?

[Scott Morrison]

Sorry, to get what in the port-progress output? The bot that posts daily in the port-progress thread runs on my machine, I can update it to add something.

[Scott Morrison]

This output comes from the master branch of mathlib-tools (i.e. with pip install .), and then leanproject port-complete.

[Mario Carneiro]

to list that N/M files are port-complete along with the other stats

[Mario Carneiro]

where N is the length of the list you just posted above and M is the maximum size that list could get (which is probably the number of files)

[Eric Wieser]

Scott Morrison said:

So I just had a look at running mathport on archive and counterexamples. It is a bit painful, mostly as it is hard to create a single lean file that imports them all.

I'm confused by this claim, leanproject mk-all can do it.

[Scott Morrison]

ah -- mathport can't handle relative imports

[Eric Wieser]

What uses relative imports?

[Scott Morrison]

Ah, I see, I was trying to use scripts/mk_all.sh, which claims to work with non-default directories, but gives you files with relative imports when run on archive and counterexample. I'll try again with leanproject mk-all at some point.

[Eric Wieser]

It does look like some of the archive files themselves contain relative imports, but that would be an easy thing to fix

[Mario Carneiro]

I will look into making mathport support relative imports

[Johan Commelin]

Isn't that a lot of effort for a little bit of gain? Why can't we just go along with Scott's PR. We just take the following steps.

1. Move archive and counterexamples into src
2. They are picked up immediately by all our tooling. We don't have to change mathport and we don't have to worry about other edge cases.
3. They are ported to Lean 4 as part of the regular process.
4. In a few months time, we move them out of the Mathlib directory, and make them standalone packages.

[Mario Carneiro]

I am very concerned about controlling the size of the Mathlib package. It is a multiplier on many things

[Mario Carneiro]

in both lean 3 and lean 4

[Mario Carneiro]

Everything we need to do to make this work either needs to be done eventually anyway or is relevant to things other than just those two projects. For example relative imports are not just used by the archive, several third party projects use relative imports

[Mario Carneiro]

We managed to get pretty far without addressing some things because mathlib is fairly homogeneous style-wise but once we start branching out we will need to handle more unusual lean setups and syntax

[Mario Carneiro]

again, are we going to do the same thing for LTE? sphere eversion? MIL? The mathlib PRs? There are plenty of other projects out there, we can't put it all in mathlib so we have to deal with this situation eventually.

[Mauricio Collares]

But isn't moving archive and counterexamples out of src (i.e. undoing the proposed changes sometime in the future) pretty simple? Moving back could happen as soon as the mathport work is complete, with the advantage of extra parallelism in the meantime.

[Eric Rodriguez]

There's some Ci that runs against that sort of stuff so all of that has to get changed

[Eric Wieser]

The docs build will break as soon as we move stuff.

[Johan Commelin]

Mario Carneiro said:

again, are we going to do the same thing for LTE?

I always imagined that files in LTE/for_mathlib/ would be ported on an individual basis, to the extent that they will be ported.

[Johan Commelin]

A whole bunch of that stuff has already been refactored (e.g. by Joël) and is being PRd to mathlib(4).

[Johan Commelin]

I don't see the point of porting the non-for-mathlib part of LTE.

[Johan Commelin]

Tl;dr: I thought that mathport-oneshot would suffice for the use cases outside of mathlib.

[Eric Wieser]

The point would be to port the whole project at once, and then PR the for_mathlib directory at leisure

[Johan Commelin]

That port is going to be insanely painful. And I don't see the point of doing it.

[Johan Commelin]

Why can't we just leave it in Lean 3, and mathport-oneshot the for_mathlib directory at leisure, when we want to PR some file in it to mathlib4

[Johan Commelin]

95% of LTE is not going to be used (in the next 10 years) by any other project. The 5% that is useful needs to be rewritten thoroughly anyway. So either oneshot it, or just use it as inspiration, but start over from scratch.

[Eric Wieser]

The advantage of having the for_mathlib directory be in a living project is that you can remove things from that directory as they're added to mathlib

[Eric Wieser]

I have very little feel for how hard a porting task LTE would be

[Johan Commelin]

Eric Wieser said:

The advantage of having the for_mathlib directory be in a living project is that you can remove things from that directory as they're added to mathlib

I think that a comment along the lines of

/-
The contents of this file have been effectively integrated into mathlib 4.
-/

at the top of files in LTE3/for_mathlib would be sufficient to keep track of such things.

[Johan Commelin]

I should do that anyways with some of the files. We are already in a situation where files in for_mathlib can't be removed because it would require a pretty annoying mathlib bump in LTE. And we just don't have time and energy for that.

[Scott Morrison]

Eric Wieser said:

The docs build will break as soon as we move stuff.

Could you clarify what the problem would be there? Surely as subdirectories of src, archive and counterexamples would just have documentation generated in the same way as everything else.

[Johan Commelin]

LTE/for_mathlib can serve as a source of inspiration. But it isn't in mathlib-ready shape at all.

[Mauricio Collares]

Scott Morrison said:

Could you clarify what the problem would be there? Surely as subdirectories of src, archive and counterexamples would just have documentation generated in the same way as everything else.

I think the problem is that the most recent doc-gen commit added special support for the archive and counterexamples directories, but worst-case it would just be a matter of (temporarily) reverting it.

[Mauricio Collares]

The tooling is nice, but we're talking about 68 files with no inter-dependencies and fewer than 10 open PRs touching them (most of them stale). There are so many feasible approaches, the most low-tech being to run mathport locally once, push it to a branch somewhere, declare the two directories frozen in mathlib3 and have a GH ticket tracking progress.

[Eric Wieser]

Ah, that's a good point; if for-mathlib doesn't consume anything outside the for-mathlib folder, then you could just create a new lte-for-mathlib project and port that exhaustively

[Eric Rodriguez]

There's other whole projects that want lean4 porting - flt-reg for one :)

[Riccardo Brasca]

I am very confident we will port flt-regular completely during the summer :grinning:

[Riccardo Brasca]

At the moment for example we need !4#4339

[Eric Rodriguez]

We're already getting to splitting fields! Woop

[Eric Rodriguez]

Johan Commelin said:

Tl;dr: I thought that mathport-oneshot would suffice for the use cases outside of mathlib.

I was thinking about this tho

[Eric Wieser]

I don't think it makes any sense to use it for flt-regular; why not just use mathport non-one shot to do the whole repo?

[Eric Wieser]

Also, #port-dashboard now includes archive and counterexamples!

[Eric Rodriguez]

Eric Wieser said:

I don't think it makes any sense to use it for flt-regular; why not just use mathport non-one shot to do the whole repo?

I'm confused what's the issue, then - I assumed this message meant that non-one-shot was not great

[Eric Wieser]

The only issue with non-one shot is that AFAIK no one has demonstrated successfully using it

[Eric Wieser]

Eric Wieser said:

Also, #port-dashboard now includes archive and counterexamples!

27 of the IMO problems are ready to port (port-status#imo/imo2008_q3 takes the prize for furthest away); I imagine that these would be fun files for people new to the port to work on once we have them as mathport output.

[Johan Commelin]

Eric Wieser said:

The only issue with non-one shot is that AFAIK no one has demonstrated successfully using it

@Scott Morrison has been writing down instructions. I think it is quite realistic that one-shot will be usable in the near future.

[Eric Wieser]

For "one-shot" or for "multi-shot"/"full-project" mode? My claim is that "one-shot" is a hack suitable for reviving PRs, but the wrong tool for converting an entire project

[Johan Commelin]

We are now discussing two issues that I think are almost orthogonal:

• Refactoring mathport so that it works well on external projects
• Labelling completely ported downsets of mathlib

Mathport

• @Scott Morrison wrote a branch of the mathport repo https://github.com/leanprover-community/mathport/tree/projects_instructions with an updated README that has instructions for using one-shot. These instructions are being tested by people here in Banff. This is work in progress, but should stabilize in the near future.
• @Mario Carneiro is looking at relative imports, which will be useful for archive/, counterexamples/ and external projects.
• To port archive/ and counterexamples/ we will need CI that publishes the output of mathport so that start-port.sh picks it up. Alternatively we move those dirs into src/ and comment out a bit of doc-gen code.

Completely ported downsets

• We need bots to label files in mathlib3 and mathlib4 that have all of their downstream dependents completely ported. @Scott Morrison is happy to write these bots.
• If we don't move stuff into src/ then leanproject --port-complete will be slightly overeager, and need to special case ~5 files.
  *

[Eric Wieser]

Do we actually care about leanproject --port-complete? I could quite easily expose this information on #port-dashboard, which already does the right thing without the special cases. Is anyone going to run this on the command line?

[Scott Morrison]

It doesn't matter where it is exposed. The main thing is that we want a bot that automatically labels files in mathlib4 which can be modified without required backporting. We can implement this right now on top of leanproject --port-complete, and I'd prefer not to be waiting on other intermediate steps.

[Scott Morrison]

But if you can do that easily based on the existing bot that updates headers in mathlib3, that would be perfect.

[Scott Morrison]

@Eric Wieser, just checking, is that thumbs up saying "yes, I'm planning on doing this at some point"? :-)

[Eric Wieser]

It's "I might do that if I get around to it, but I wouldn't count on it happening in the next week"

[Eric Wieser]

What's the source of truth for whether a file is "completely ported"?

[Eric Wieser]

For "synchronized" the source of truth is the mathlib4 header comment

[Scott Morrison]

I'm not certain what you mean. We can determine if a file is "downstream-closed-ported" by running leanproject --port-complete. I was thinking to run this every day and update the headers of both mathlib3 and mathlib4 files from that?

[Eric Wieser]

That approach can lead to a file becoming un-complete

[Eric Wieser]

Which you said you didn't want to allow

[Scott Morrison]

Maybe I'm confused. I thought I said I wanted the condition to be "at some point has been in the output of leanproject port-complete". People adding more stuff to mathlib during the next month or so will just have to be aware that if they depend on a file in this condition there could potentially be breaking changes in mathlib4 already. In the vast majority of cases it is just going to be additional lemmas or changed imports.

[Eric Wieser]

That's a good definition, but it means you can't use --port-complete to ask "is this file complete"

[Scott Morrison]

Ah, okay, I was just thinking the logic would be:

• each day, run leanproject port-complete
• for each file in the output, check if the mathlib3 and mathlib4 files already have the new header
• if not, add the header
• if a tool or CI needs to check if something is "downstream-closed-ported", we check for these headers.

[Eric Wieser]

I think it probably makes sense to make the mathlib4 header the source of truth

[Eric Wieser]

As that's consistent with what we do for unported/ported, and prevents us having two different ways for things to fail if file are moved

[Mario Carneiro]

The CI script for processing the archive and counterexamples directories is now up at mathport#238. I am not sure whether the PR CI will already produce the relevant releases.

[Eric Wieser]

What does it output in the source header comments?

[Eric Wieser]

(the dashboard will be happy if it's just the same as how src is handled, with no mention of archive)

[Mario Carneiro]

that's exactly what it does

[Eric Wieser]

Do you have an example, or should I just wait till tomorrow?

[Mario Carneiro]

/-
Copyright (c) 2022 Bhavik Mehta, Kexing Ying. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Bhavik Mehta, Kexing Ying

! This file was ported from Lean 3 source module «100-theorems-list».«30_ballot_problem»
! leanprover-community/mathlib commit 57ac39bd365c2f80589a700f9fbb664d3a1a30c2
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Probability.CondCount

/-!
# Ballot problem
...

[Eric Wieser]

That looks very sensible, though I have no doubt we have a script or two to fix!

[Mario Carneiro]

We have a result from mathport. It looks like the error is caused by a missing predata, so hopefully this will be fixed when the next predata runs (or possibly once it is merged and then predata runs)

[Eric Wieser]

Mario Carneiro said:

We have a result from mathport. It looks like the error is caused by a missing predata, so hopefully this will be fixed when the next predata runs (or possibly once it is merged and then predata runs)

I've merged master into the branch

[Mario Carneiro]

I don't think it will make any difference, the last predata still ran using the old script. We shouldn't merge this until the archive issues are fixed though