Zulip Chat Archive

Stream: mathlib4

Topic: Porting `stream`s (`Nat → α`)


Adrien Champion (May 17 2022 at 13:16):

Original discussion in #lean4 > infinite lists.

I ported the stream type from mathlib/data/stream/defs.lean and mathlib/data/stream/init.lean which encodes streams as functions over discrete time (Nat → α).

If deemed worth it, I would be interested in contributing this code to mathlib4. I wrote it as an exercise: naming the stream type FStream might not have been a good idea, and commits (all two of them) do not follow lean's commit conventions, but that's easily fixed.

Marcus Rossel (May 17 2022 at 17:13):

Not sure about this, but I'm guessing this will be covered by synport. Are you aware of the general porting strategy for mathlib4?

Adrien Champion (May 17 2022 at 20:50):

Well in the original discussion @Mario Carneiro pointed to the ported version of these files

I was then told that they would most likely not work right away, or at least the Initfile, because of the dependency on tactic.ext. The port itself was initially more of an exercise than anything for me, so I did not investigate much.

All I can say is that I was using the ported Init.lean and went back to the Lean 3 version when I ran into a few theorems/proofs that did not make sense. I don't remember precisely what the problem was but I can re-discover it if you want more details (I vaguely remember notation clashes or something like that but I'm not sure)

Adrien Champion (May 17 2022 at 20:52):

Marcus Rossel said:

Not sure about this, but I'm guessing this will be covered by synport. Are you aware of the general porting strategy for mathlib4?

To address your question no, I was not aware of this page. Thank you for mentioning it I'll read this asap

Adrien Champion (May 17 2022 at 20:59):

Also, my version includes Lean-4-ifying some aspects that (I assume) synport would not cover. (Slightly) more documentation is one aspect, but I'm thinking more of defining functions in the appropriate namespace for accessibility and val.fun args notation. For instance the original version has appendStream : List -> stream a -> stream a which I changed to List.appendStream, and added FStream.prependList.

Adrien Champion (May 17 2022 at 21:01):

Admittedly there are few situations like that in the port

Mario Carneiro (May 18 2022 at 13:55):

I think we should try not to make any naming changes for things that already exist, because this makes downstream porting a lot harder. If your innovations are possible to do in lean 3 as well as lean 4, it seems better to submit them first to mathlib and then port it to mathlib4.

Mario Carneiro (May 18 2022 at 13:56):

Perhaps we should also back-port the new name, since stream is taken

Adrien Champion (May 20 2022 at 13:11):

I understand. Sadly, I have virtually no experience with Lean 3 and not enough time to get into it for the sake of this (very minor) contribution :/

Adrien Champion (May 20 2022 at 13:12):

Thank you all for the feedback though!


Last updated: Dec 20 2023 at 11:08 UTC