proposal for marking files as frozen

Stream: mathlib4

[Scott Morrison]

First, some background. There's been some private discussion on the maintainers list preceding this, but there hasn't yet been a proper public discussion.

We are hoping to soon get started porting files from mathlib3 to mathlib4. This is going to be a gradual process, assisted by the tool mathport.

There is a wiki page with some advice on porting, at https://github.com/leanprover-community/mathlib4/wiki.

There is a page tracking which files have been ported, at https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status

There is a tool under scripts/port_status.py, which will land in #17009, which will provide a list of files which are ready for porting now.

[Scott Morrison]

Now, once files have been successfully ported, PR'd to mathlib4, and merged, we would like the freeze the file back in mathlib3.

[Scott Morrison]

This does not mean it is completely impossible to change --- but you'll need to make the corresponding PR to mathlib4, so it will be more cumbersome.

[Scott Morrison]

We need a way to mark files as frozen. The list at https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status in principle keeps track of this, but it's been suggested there should be a prominent indicator in the files themselves.

[Scott Morrison]

#17039 is my proposal for how to do this.

[Scott Morrison]

It adds a block

> THIS FILE IS FROZEN, AS IT HAS BEEN PORTED TO MATHLIB4
> https://github.com/leanprover-community/mathlib4/pull/467
> No changes accepted without a corresponding PR to mathlib4.

at the very top of each frozen file.

[Scott Morrison]

If we go ahead with this, or something similar, we will also want two additional CI tools:

1. something that labels PRs which touch frozen files with a special label, so reviewers can assure that a mathlib4 PR also exists.
2. something that notifies us when https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status is out of sync with the labels inside actual files.

[Kevin Buzzard]

Video was super-helpful. Thanks a lot @Scott Morrison !

In some sense the most terrifying part right now was the "let's figure out which file to port -- oh look there's a gigantic maze with not enough information". Can someone give some kind of a feeling as to which areas of mathlib are currently "ready for porting"? I am keen to get up to speed with this process ASAP because I think it's an excellent way to simultaneously learn about Lean 4 and mathlib4. I would humbly suggest that enabling non-power-users like me to be able to figure out which files need porting in a less painful way would be very helpful, but until that day comes I'm looking for general guidance about where I should start looking. For example is category theory something that we can start on now or are we in no position to do it? What about group theory (group homs, subgroups etc)?

I should say that I have been waiting for this day for years. Initially I had naively assumed that the entire porting process was going to look like (a much more horrible version of) this (without the computer helping us first) and was rather looking forward to it. October is my horrible month; I am submerged in teaching every year, but it's the 18th so the light is at the end of the tunnel.

[Kevin Buzzard]

PS what was going on with (a) the missing import (nonempty_prop) and (b) the missing function (extend_apply') in the video?

[Scott Morrison]

@Kevin Buzzard, as soon as bors is finished with #17009, you can type at the command line

scripts/port_status.py

[Scott Morrison]

This will show you output something like:

# The following files have all dependencies ported already, and should be ready to port:
# Earlier items in the list are required in more places in mathlib.
logic.basic
data.option.defs
data.sigma.basic
algebra.group.to_additive
algebra.abs
data.bool.basic
control.functor
lean_core.data.vector
data.char
logic.lemmas
category_theory.concrete_category.bundled
algebra.order.floor
category_theory.elementwise
data.bracket
data.stream.defs
data.rbtree.init
data.num.basic
data.lazy_list
data.fin.fin2
data.nat.bits
data.rbtree.default_lt
lean_core.data.dlist
control.ulift
lean_core.data.buffer
lean_core.data.buffer.parser
algebra.group_power.identities
data.json
control.basic
algebra.hierarchy_design

# The following files have their immediate dependencies ported already, and may be ready to port:
data.nat.cast.defs
group_theory.eckmann_hilton

[Scott Morrison]

We may want to have a thread where at regular intervals someone can post an annotated copy of this list.

[Scott Morrison]

I would love to have the output of port_status.py merged with the graph drawing super powers of leanproject import-graph, so we can have pretty progress charts to motivate us. :-)

[Kevin Buzzard]

I remember once a long time ago porting a bunch of logic.basic just for fun. Is there a way of "claiming" a file so that others know it's being worked on?

[Kevin Buzzard]

I don't care about the graphs, I think the text list is fine. The graphs are I'm sure helpful if your goal is "port file X" but my goal is "learn Lean 4 and port all the files"

[Scott Morrison]

I think the process to claim a file is to create a "porting coordination" thread in this stream, post a copy of that list, and say that you're working on it. :-)

[Scott Morrison]

That list is sorted, and the number of uses of each file drops off pretty precipitously as you go down the list. I wasn't sure whether it would be more or less helpful to show this number after each file, e.g.

logic.basic (2563)
data.option.defs (2557)
data.sigma.basic (2515)
algebra.group.to_additive (2433)
algebra.abs (2352)
data.bool.basic (2229)
control.functor (2048)
lean_core.data.vector (2030)
data.char (1768)
logic.lemmas (883)
category_theory.concrete_category.bundled (813)
algebra.order.floor (742)
category_theory.elementwise (564)
data.bracket (147)
data.stream.defs (26)
data.rbtree.init (23)
data.num.basic (21)
data.lazy_list (20)
data.fin.fin2 (16)
data.nat.bits (15)
data.rbtree.default_lt (11)
lean_core.data.dlist (4)
control.ulift (3)
lean_core.data.buffer (3)
lean_core.data.buffer.parser (2)
algebra.group_power.identities (1)
data.json (0)
control.basic (0)
algebra.hierarchy_design (0)

[Scott Morrison]

Realistically, I think everything there with >100 uses is worth doing immediately, and everything with <=100 is not.

[Kevin Buzzard]

I see -- the idea being that once everything with > 100 uses is done, there will be more things which appear on the list with > 100 uses.

[Scott Morrison]

Whereas when you do something with <100 uses, ipso facto the new things that appear also have <100 uses!

[Jakob von Raumer]

@Scott Morrison So the second part of the output are files that have non-ported indirect imports?

[Kevin Buzzard]

Can someone clarify why logic.basic is on the list but there's already a file Logic.Basic in mathlib4/Mathlib?

[Kevin Buzzard]

Same question for data.option.defs

[Kevin Buzzard]

I tried to start on data.sigma.basic but despite the claim above that all dependencies are ported already, I can find none of the three imports

import Mathlib.Meta.Univs
import Mathlib.Tactic.Lint.Default
import Mathlib.Tactic.Ext

in mathlib4. I am not clear about whether just deleting them all and pressing on will ultimately add more confusion or whether it's a worthwhile endeavour. Sorry for all the questions, I'm just getting the feeling for this -- I would ultimately like to get Imperial undergraduates working on this stuff but I need to figure it out myself first.

[Floris van Doorn]

The script looks at which files on this page have been marked as Yes: https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status
Logic.Basic is not a yes, because it was only a partial port: many things from mathlib3 are still missing.

[Floris van Doorn]

For tactic/meta imports: I think it is useful to look at the status of which tactics have already been ported in the list mathlib4#430.
If the tactics mentioned in the imports are already ported, you can import the corresponding mathlib4 files (the file name might have changed a bit). If not, you can replace the 'No' on https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status by 'Waiting on tactic X' or something.

[Kevin Buzzard]

Thanks -- this is very helpful

[Patrick Massot]

Floris, could you add those explanations to the wiki page?

[Floris van Doorn]

Good idea. I added it.

[Floris van Doorn]

I must say I'm a bit worried about the missing tactics/attributes in mathlib4. I think that quite soon we will hit a roadblock where files depend on unported tactics, and the porting either has to wait, or we have to do a lot more manual work.

[Kevin Buzzard]

David Renshaw pointed out in the other thread I opened (I wasn't sure if this thread was a place for porting questions) that both the ext and nolint attributes seem to be working (it had not occurred to me to look for instances of them in mathlib4)

[David Renshaw]

Note that a chunk of ported Logic.Basic things moved to std4 in https://github.com/leanprover-community/mathlib4/pull/403. (And yes, there's still a bunch that's totally unported too.)

[David Renshaw]

https://github.com/leanprover/std4/commit/3f3803e26e2894b0469196303b5afb2e300b68b9

[Joseph Myers]

Scott Morrison said:

If we go ahead with this, or something similar, we will also want two additional CI tools:

1. something that labels PRs which touch frozen files with a special label, so reviewers can assure that a mathlib4 PR also exists.
2. something that notifies us when https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status is out of sync with the labels inside actual files.

I think there are various race conditions to consider with this proposal, with associated CI implications.

• A PR touching a frozen file might be an old one from before the file was frozen - PRs often take a while to review. So you need to detect that case and mark old PRs (on branches in which the file is not marked as frozen) accordingly. Likewise if a change to the frozen file gets added in the old branch later. Likewise if a new PR is created from a branch predating the freezing.
• Or there might be changes to the file in mathlib3 after the version on which the mathlib4 file was based (mathlib3port currently seems to be 9 days old, if people start with files from there they won't get the most recent mathlib3 changes without adding them manually). Or changes occurring in parallel to the porting process or the process of marking as frozen (including merging in the same bors batch, or approved to merge while the batch merging the freeze is going through CI).

I think what these race conditions really indicate is that assertions that a file is fully ported need to be versioned. Entries in mathlib4-port-status shouldn't say 'Yes', they should specify a mathlib3 commit such that all the content of the mathlib3 file as of that commit has been confirmed to be fully ported to mathlib4. (mathport might e.g. be made to put comments in the files it generates saying what mathlib3 commit of that file they are up to date with, to help people identify the exact version they have ported.) Once the data about what is ported is explicitly versioned, you no longer need some complicated way for CI to detect and avoid all race conditions (or error-prone manual checks for recent unmerged changes when reviewing a PR to mark a file as frozen), just a much simpler way to list files that were ported based on a version of the mathlib3 file that is no longer the most recent version, and so need more recent changes ported over.

(There should also be documentation of how to apply the source-level porting to a single changed file or definition, to help people in porting changes to a previously ported file - including helping anyone who wants to do a PR to a frozen file and so would like the automatically generated version of their new or changed definitions or lemmas as a starting point for doing a corresponding mathlib4 PR. In general, my impression is that documentation for users of (Lean 3 + mathlib + leanproject) wanting to start doing things with Lean 4, and so wanting to know both how to convert source code and the Lean 4 equivalents of the things they do with Lean 3 + mathlib + leanproject, is fairly sparse at present.)

[Patrick Massot]

David Renshaw said:

Note that a chunk of ported Logic.Basic things moved to std4 in https://github.com/leanprover-community/mathlib4/pull/403. (And yes, there's still a bunch that's totally unported too.)

@Mario Carneiro I'm sorry that we ask so much work from you but here I think we really need help to figure out what needs to be ported from this file. We will very quickly hit the time where all porting is blocked on that one. If you have a clear view of what was moved to core or std or is irrelevant, could you create a branch where you simply take the mathport output and remove everything we shouldn't port?

[Mario Carneiro]

@Patrick Massot I'm confused by the question. The rule is the same as for any port: if stuff already exists upstream, then #align it, otherwise port it. If it exists upstream with the same name then it can be removed (and yes, that will mean that mathlib4's Logic.Basic file will be much smaller than it was).

[Patrick Massot]

The issue is to determine whether the stuff already exists upstream

[Mario Carneiro]

I have already done several full passes over Logic.Basic so it should be pretty complete already, but stuff moves on

[Mario Carneiro]

I have not made any attempt to freeze mathlib3's logic.basic yet

[Patrick Massot]

Oh. Should we consider it ported then?

[Mario Carneiro]

I would say it needs another pass to finalize it. You can find most of the theorems by watching for duplicate definition errors, and there are a few more which have been renamed in std4 (Std.Logic is the new home for most of logic.basic)

[Mario Carneiro]

the #align directives for these are missing

[Patrick Massot]

Should we start with the output from mathport or the current state of the file in mathlib4 then?

[Mario Carneiro]

The output from mathport should hopefully be well formed enough to get those duplicate definition errors

[Mario Carneiro]

the current mathlib4 file can be used as an "answer key" for most of it

[Patrick Massot]

Ok, I'll try to that tomorrow if nobody is faster. Now is bedtime. I really want to work on the port. Like Kevin I'm super excited that we're now instructed to port theories instead of complicated tactics.

[Scott Morrison]

I agree the race conditions coming from existing PRs, and from mathlib3port lagging behind current mathlib, are somewhat worrisome.

I propose we do the following

• make sure (?) it is easy to see in mathlib3port which commit hash was used to generate the files
• PRs to mathlib4 porting files should include this hash in the PR description?
• https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status should include some extra information besides 'Yes'.
  • I propose we go with 'Yes mathlib4#nnn mmmmm', where 'nnn' is the pull request number for mathlib4, and 'mmmmm' is the commit hash from mathlib3.

[Scott Morrison]

However this is all extra work and overhead, which I'm not thrilled about. Winging it is another alternative, until we notice things going wrong.

[Scott Morrison]

Perhaps all these race conditions (which fail by dropping contributions to mathlib3) are features, not bugs: they encourage people to divert their work on mathlib3 into work on mathlib4. :-)

[Mario Carneiro]

Maybe we can start having "nightlies" for mathlib: that is, certain designated (tagged?) commits which will be used by mathport CI and carried around

[Mario Carneiro]

the bors pipeline means that we already basically have "six-hour-lies"

[Kevin Buzzard]

Another rather brutal approach would just be to freeze all of mathlib3. I thought that this was the plan at some point? Has this been deemed unworkable?

[Mario Carneiro]

At the rate things are going this would be hugely disruptive

[Mario Carneiro]

it's certainly not any time soon

[Scott Morrison]

@Mario Carneiro, what if we just tweak mathport to add a comment to all the generated .lean files:
-- This file was generated from mathlib at commit XXXX
-- Please remove this comment before making a pull request to mathlib4, but include the commit hash in your PR description.

[Mario Carneiro]

sure, we can do that

[Mario Carneiro]

actually I guess that requires some more complicated CI scripting

[Mario Carneiro]

since the mathport executable doesn't actually know that information

[Mario Carneiro]

maybe the mathlib3port build script can do that?

[Mario Carneiro]

Oh, actually maybe this isn't such a good idea, it will cause a lot of merge conflicts

[Mario Carneiro]

I like the idea of putting the mathlib commit in the mathlib3port commit message though

[Scott Morrison]

We really just need a way of making the mathlib3 commit sha visible to someone grabbing a file from mathlib3port.

[Scott Morrison]

I see, so git log in mathlib3port would tell you the latest mathlib3 sha.

[Scott Morrison]

So it's just the update.sh script in mathlib3port that needs to know which mathlib3 is being used.

[Scott Morrison]

I guess we could have mathport CI just put an extra file into the release process, that contains exactly that version information.

[Scott Morrison]

i.e. we would modify

• in mathport .github/workflows/build.yml (and predata.yml), to add an extra file to the release bundle, say version.yaml containing mathlib: XXXX etc
• in mathlib3port update.sh, to grab that file from the release bundle, and include the mathlib version in the commit message

[Scott Morrison]

(For simplicity perhaps the extra file shouldn't be a yaml, it can just contain the bare sha.)

[Scott Morrison]

okay, I will try this later today

[Scott Morrison]

There's going to be a slightly annoying thing here:

• in the port-status wiki file, we update a file to Yes mathlib4#999 1234abcd after the PR to mathlib4 lands.
• we then make a PR back to mathlib3, to label that file as frozen, per this thread
• this lands in commit 7890cdef for mathlib3, so now the port-status file is out of date, and potentially we worry that the file has meaningfully changed

Possible solutions:

• just cope
• when the freezing commit lands, remember to update the port-status wiki file
• have CI do that, by tracking appropriate labels

[Mario Carneiro]

The file very well could have changed in that time. When reviewing the PR back to mathlib3, one of the tasks is to make sure that there are no such changes, and if there are, to open a mathlib4 update PR.

[Scott Morrison]

I've updated the porting script in #17056, so if the port-status wiki file includes comments after No, it prints those. I've also update the port-status wiki header to state that the statuses MUST start with either 'Yes' or 'No' for now.

Example output now:

# The following files have all dependencies ported already, and should be ready to port:
# Earlier items in the list are required in more places in mathlib.
logic.basic
data.option.defs
data.prod.basic    -- WIP
data.sigma.basic
algebra.group.to_additive
data.bool.basic
control.functor
lean_core.data.vector
data.char
logic.lemmas
category_theory.concrete_category.bundled
algebra.order.floor
category_theory.elementwise
data.bracket
data.stream.defs
data.rbtree.init
data.num.basic
data.lazy_list
data.fin.fin2    -- PRd as #478
data.nat.bits
data.rbtree.default_lt
lean_core.data.dlist
control.ulift
lean_core.data.buffer
lean_core.data.buffer.parser
algebra.group_power.identities    -- Blocked by current status of ring tactic: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/status.20of.20.60ring.60/near/303965507
data.json
control.basic
algebra.hierarchy_design

# The following files have their immediate dependencies ported already, and may be ready to port:
data.nat.cast.defs
group_theory.eckmann_hilton

[Scott Morrison]

(Perhaps people writing WIP should add their name. :-)

[Mario Carneiro]

The port-status file looks pretty intimidating (in part because it's a yaml file rendered as markdown). Can we make this less user visible, for example by using a bot to update it automatically when a PR lands?

[Scott Morrison]

I agree it's gross. I think this is the current set of transitions:

• When running port_status.py, it dumps a new port_status.yaml in the current directory with new lines for newly added files. These should be periodically included in the wiki.
• People are adding WIP and PRd as and Blocked by... comments
• When a PR is merged into mathlib4, we can change No to Yes mathlib4#XXX, or ideally Yes mathlib4#XXX abcd1234 to record the mathlib sha.
• When someone freezes the file in mathlib3, they should update the sha.

I'd propose we handle things manually for at least a few days, and then ask if someone can write a bot for us to help with CI. (Ask Sarah for help on this at the mathlib porting meeting with her?)

[Joseph Myers]

I'm not sure the person freezing the file in mathlib3 updating the sha is the best option, because of the risk that they get it wrong (miss that there are intermediate commits that still need porting). Rather, it might be better to have automation that checks if the sha is older than the current revision of the file in mathlib3 - and make that automation able to detect if a commit just does freezing but nothing else, and ignores the commit in that case (so an update isn't needed after a freezing commit but you still get the information when the mathlib4 file is genuinely out of date compared to mathlib3). Alternatively, the automation could update the sha itself in the case where the only mathlib3 commit to the file subsequent to the port to mathlib4 is a freezing-only commit.

[Scott Morrison]

I agree that would be ideal, but it adds more requirements for the automation (detecting freeze-only commits).

[Mario Carneiro]

not putting the freeze message in the file itself might help with this

[Mario Carneiro]

it might suffice to have PRs that touch some frozen files get a comment from a bot saying "this PR touches files X, Y, Z that have already been ported. Please make sure to open a companion PR on mathlib4"

[Scott Morrison]

It was suggested above that people would like to know that a file is synchronized before they start, and a bot that only touched PRs would be late in the game.

[Scott Morrison]

I don't think this is a show stopper, though, and I really like the prospect of fewer commits/PRs to make this all happen.

[Scott Morrison]

I guess we could keep the SYNCHRONIZED messages in individual files, but they would not be the "source of truth" (which I guess for now is the port-status page on the wiki).

One bot could label prs that touch synchronized files.
Perhaps another bot could at regular intervals add the SYNCHRONIZED messages itself. (i.e. like our bot that updates nolints)

[Gabriel Ebner]

Scott Morrison said:

i.e. we would modify

• in mathport .github/workflows/build.yml (and predata.yml), to add an extra file to the release bundle, say version.yaml containing mathlib: XXXX etc
• in mathlib3port update.sh, to grab that file from the release bundle, and include the mathlib version in the commit message

FYI, we already add a rev file in the predata. https://github.com/leanprover-community/mathport/blob/897d11a96d142d09757acb99461624e7cfc581df/Makefile#L76

[Jakob von Raumer]

Do we need a way to not accidentally freeze files which are still about to change in open mathlib PRs?

[Scott Morrison]

Freezing files will, I think, have higher priority. Open PRs that have a "freeze" event intervene will have to cope.

[Scott Morrison]

(That's just a suggestion, not me saying how things have to be. :-)

[Jakob von Raumer]

Should mathlib3port be bumped more frequently?

[Jakob von Raumer]

Does your script ignore Init? RBTree.Init depends on init.data.ordering.basic, which hasn't been ported

[Jakob von Raumer]

Or is there something like mathlib3port for old init files?

[Jakob von Raumer]

Can someone grant me write access to non-master branches on mathlib4?

[Jakob von Raumer]

The instruction page for porting seems to be missing a reminder to put new files in Mathlib.lean

[Jakob von Raumer]

I added a few comments to the file about blocking tactics and about blocking missing init files

[Jakob von Raumer]

Point 8 is now a bit painful, why do we need to track the mathlib commit hash we checked again? Shouldn't it be always on track with the most recent mathlib version?

[Scott Morrison]

How will we know that it is on track with the most recent mathlib version?

[Scott Morrison]

We need to keep track, somewhere, of the promise "mathlib4 reflects all changes to this file up to commit X".

[Scott Morrison]

So that if that file has any changes in to post X, we have a way of noticing and not losing those changes.

[Scott Morrison]

The proposal is that the "source of truth" for such promises is in the port status wiki page.

[Scott Morrison]

If someone makes a PR that touches a file that is synchronized, there will need to be a PR to mathlib4 to make the corresponding changes.

[Scott Morrison]

Once both PRs have merged we can update the port status wiki page sha for that file.

[Scott Morrison]

I agree point 8 is super painful for now. So we need some CI assistance.

[Scott Morrison]

• a script that tells us a list of synchronized files but which have fresh changes
• perhaps some automation that updates the port status wiki page --- but I'm not really sure what automation helps here, as it seems all the steps need human verification that something has been done correctly...

[Jakob von Raumer]

Right, thanks for the explanation :)

[Jakob von Raumer]

I think what could be useful would be a way to automatically PR the freeze comment to mathlib

[Scott Morrison]

Okay, that's a good point. What should trigger it? A PR being merged to mathlib4 that ...? We need to work out how a bot would parse the PR to decide which files it should mark as synchronized.

[Scott Morrison]

If someone wants to write such a bot I will happily test it and merge the CI changes. :-)

[Jakob von Raumer]

I'll look into it tomorrow.

[Jakob von Raumer]

Made a manual PR for the comment for mathlib4#480 at #17077. Maybe we can fast-track those PRs or add a specific label or switch off some of the CI?

[Jakob von Raumer]

(Ah, damn, I just noticed, that your proposal for that message might not be cast in stone as of now)

[Johan Commelin]

A specific label certainly seems like a good idea.

[Johan Commelin]

I think we can just bors merge such PRs without waiting for CI.

[Scott Morrison]

I created the mathlib4-synchronization label for these.

[Joseph Myers]

Scott Morrison said:

Freezing files will, I think, have higher priority. Open PRs that have a "freeze" event intervene will have to cope.

I think this rule adds to the case that we need good Lean 4 migration documentation, so that PR submitters (who may never have used Lean 4 and may not have followed any Lean 4 discussions either so don't know any details of the differences between Lean 3 and Lean 4 or the mathlib conversion process) can be pointed to a guide covering how to do with Lean 4 (+ mathlib4 + lake + any other tools used with Lean 4) what they are used to doing in Lean 3 + mathlib + leanproject, and how to run the automated conversion for the new code in their PR. (Without the freeze of converted files we'd still have needed such migration documentation eventually, but maybe not until the conversion was much more advanced.)

Regarding another comment, shouldn't permissions to push to non-master branches of mathlib4 be copied from the permissions on mathlib, so people don't need to request such permissions individually? (Note: I don't know whether this has in fact been done.)

[Scott Morrison]

Yikes, yes, we have a little over 300 people with write access to the mathlib repository. Do we really want to copy over all those permissions? We'd have to work out how to do it in bulk.

[Joseph Myers]

Or at least the permissions for those who opened a mathlib PR in the last six months or something like that, but I don't know how much fewer that is (presumably the GitHub API can be used to get a list of such users).

[Joseph Myers]

There's an assumption here that mathlib4 CI works (or will work) like mathlib CI, i.e. on branches in the main repository but not so well on forks (and will end up providing downloadable oleans for such branches, even if it doesn't yet, and mathlib4 will end up slow enough to build that having such oleans will be important). I don't know if that's actually the case or not.

[Scott Morrison]

Yes, I think that assumption is correct.