Kevin Buzzard interview about Lean · Miscellaneous

while this is definitely something worth highlighting, it's not directly related to Coq dev/plugin dev (hence the move). Or did he talk directly about Coq development?

Paolo Giarrusso (Jul 01 2022 at 18:17):

Coq does not appear on the page AFAICT; this might be more interesting on "how to spread Coq more" — right at the outset it says "[Scholze's proof] was kind of a big public relations win for this software".

Karl Palmskog (Jul 01 2022 at 18:23):

one might think that the ACM award(s) would help with PR, but I don't think I've observed much of an effect

Paolo Giarrusso (Jul 01 2022 at 19:18):

Paolo Giarrusso (Jul 01 2022 at 19:20):

as Buzzard points out, if you talk to mathematicians, and especially if you want their grant money, you shouldn’t talk about strong normalization, but give empirical evidence your tool helps their goals (however misguided they might be, this is still a good strategy to get their ears and maybe fix them).

Paolo Giarrusso (Jul 01 2022 at 19:22):

he very explicitly says that is necessary to get funding, so I suppose he wants to get LOTS of funding from mathematicians (maybe not just for himself, but certainly for Lean)

Paolo Giarrusso (Jul 01 2022 at 19:28):

Enrico Tassi (Jul 01 2022 at 20:01):

Karl Palmskog (Jul 01 2022 at 20:10):

for the record, the most high-profile Coq math release in the recent two years is arguably https://github.com/math-comp/Abel - but I doubt that has/will grow enthusiasm for Coq in the math community (due to the Abel math being "old")

Karl Palmskog (Jul 01 2022 at 20:12):

Coq demographics leans [pun not intended] towards CS, type theory, maybe category theory, I'm not sure if that can change in near-to-medium-distance future

Enrico Tassi (Jul 01 2022 at 20:19):

We can't ignore the momentum,but this magazine is too biased to be taken seriousy IMO

Karl Palmskog (Jul 01 2022 at 20:29):

CS+ITP is seemingly never trending. To be honest, I think HOL4+CakeML is currently well ahead of Coq+CompCert+MetaCoq+CertiCoq in terms of program verification features and TCB, but HOL4 and "momentum" are concepts far apart.

Karl Palmskog (Jul 01 2022 at 20:30):

I'm personally fine with CS+ITP never trending, but there is always the chance that all funding goes in another direction

Paolo Giarrusso (Jul 01 2022 at 20:30):

(The actual Scholze story is more interesting than the pop-science version on Quanta, but we should resist the impulse to criticize the weak points)

Paolo Giarrusso (Jul 01 2022 at 20:31):

Paolo Giarrusso (Jul 01 2022 at 20:40):

But hopefully, not justified, especially since AFAIK Lean can't afford anything close to Coq's diversity: my code couldn't go in mathlib

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:20):

Karl Palmskog (Jul 03 2022 at 14:46):

do you think the following is unbiased? There is no source for this, it's not a quote:

Enrico Tassi (Jul 03 2022 at 14:46):

Maybe you should try to submit an article that claims Coq is great by citing out of context members of the Lean community.

Karl Palmskog (Jul 03 2022 at 14:48):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:51):

Maybe I should submit an article, and see if there is bias indeed. Until then, I would refrain from being dismissive of Quanta which is a magazine of much wider scope than this

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:52):

when I was introduced to Coq in 2012, already that was a wide complain in the US

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:52):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:53):

it is fine if they don't want to do marketing, but then don't claim bias when others do worry about teaching their tool to the wider research community

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:53):

Karl Palmskog (Jul 03 2022 at 14:54):

to say without quoting someone that something "feels jumbled" belongs in opinion columns, not serious articles

Karl Palmskog (Jul 03 2022 at 14:55):

would you accept without complaint that language/claim in a POPL/PLDI/etc. submission you're reviewing?

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:58):

That claim in Quanta seems pretty accurate to me, so if something I have to props the writer

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:58):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:59):

Emilio Jesús Gallego Arias (Jul 03 2022 at 15:00):

Karl Palmskog (Jul 03 2022 at 15:14):

Not sure I see any reason for self-reflection in this. Assume someone, somewhere makes an idiosyncratic Coq library that is guaranteed to be called out for jumbledness by 100% of Quanta journalists. The author then puts it on GitHub and relies on Coq compatibility policy to keep it alive for a decade or two. Does the Coq community now need to step in and make it idiomatic or tell the author to refactor it?

If you want a consistent library, there are now several to choose from in the Platform, and they are likely to be around for "a while" (decades?) in some reasonable form.

Emilio Jesús Gallego Arias (Jul 03 2022 at 15:43):

Indeed it seems people don't see the need to analyze a few things. The example you put indeed tells me little in terms of what to reflect about it. People do random libraries in Lean all the time, however for math, they seem pretty well organized.

What I wonder is why mathematicians are not using Coq when it had a very large advantage in terms of tech and timing, why, despite investing significant resources, our implementation is stuck in several fronts, why Quanta is publishing about Lean and not Coq, etc....

Karl Palmskog (Jul 03 2022 at 15:46):

one thing the original Quanta article taught me: in interviews about research, insist on providing written answers to questions, that must be written out in full when published or not included at all

Enrico Tassi (Jul 03 2022 at 19:22):

Bas Spitters (Jul 06 2022 at 08:04):

The coq-community has done great work to make the bazar model much more manageable.
We just need more and more people to start using these tools.

Michael Soegtrop (Jul 06 2022 at 08:46):

IMHO the Coq model is better for industrial applications, because there is a certain pressure to keep things compatible. Sure one can get a nicer and cleaner library with a mono repo approach where one can make substantial changes as long as everything is synchronized. But basing derived work on such an infrastructure can be a lot of work. I wonder if substantial derived work can be maintained over say a decade outside of the Lean repo.

With Coq I had so far little trouble keeping my own stuff in sync with Coq - it is usually less than a day of work to adjust my work (that is everything I wrote since 8.5 or so) to a new Coq Platform release. Not sure how my milage would have been with Lean in the same time frame.

Théo Zimmermann (Jul 06 2022 at 09:42):

I think many comparisons of Lean and Coq are mistaken when they try to match one with the cathedral model and one with the bazaar model (or said otherwise with the "unplanned city" quote). Lean itself is developed in cathedral mode, but I think that mathlib is developed more in bazaar mode. While Coq itself is developed in bazaar mode, but math-comp has been developed in cathedral mode (although the entire ecosystem is uncoordinated and may thus feel like bazaar, but bazaar is usually applied to a single project, not to an entire ecosystem).

Emilio Jesús Gallego Arias (Jul 06 2022 at 11:17):

Thanks @Théo Zimmermann that pretty much sums how I see things; for me the problems in Coq are not so much related to the development model, but more to the failure to provide users with some essential features (such as a richer base library, or an object system to manage classes of properties)

Emilio Jesús Gallego Arias (Jul 06 2022 at 11:17):

thus it is common to see really painful code around, reimplementing a lot of basic stuff

Emilio Jesús Gallego Arias (Jul 06 2022 at 11:18):

Bazaar indeed is likely limited if you need to do a deep reachitecturing of the system, and this is bad for Coq because I think it needs one

Paolo Giarrusso (Jul 06 2022 at 12:13):

BTW, if we're comparing with mathlib, we should compare math-comp — which seems far more regular than "all of Coq", probably faster than Lean 3 (who knows about 4), etc...

Théo Zimmermann (Jul 06 2022 at 12:30):

Yeah, that was precisely my point. When comparing mathlib vs math-comp, the bazaar is not on the same side.

Théo Zimmermann (Jul 06 2022 at 12:30):

Paolo Giarrusso (Jul 06 2022 at 14:02):

also important: Lean follows neither cathedral nor bazaar, it follows the "don't use it for real, it's a prototype" model.

Bas Spitters (Jul 07 2022 at 06:01):

@Emilio Jesús Gallego Arias with object system, do you mean type classes?
Does the hierarchy builder solve some issues of that?

Do we really understand the bazar model for mathematics? Unless we want something completely disjoint, I think we'll want some kind of univalence or parametricity to connect different representations of the same thing.
Currently the support for that seems better in Isabelle than in Coq.

Karl Palmskog (Jul 07 2022 at 08:21):

However, this [bridging specific encodings with or without tool support] is probably as cold a topic as it gets. Even with Paramcoq in the Platform, its use remains niche.

Bas Spitters (Jul 07 2022 at 09:08):

I think the topic is still hot, or at least hott, there's good support in cubical agda, but with primitives not supported in Coq (yet?)

Paolo Giarrusso (Jul 07 2022 at 12:47):

Even if you had the equal types, you end up needing to restate lemmas just to bridge between ecosystems.

Paolo Giarrusso (Jul 07 2022 at 12:49):

And AFAICT, migrating to univalence doesn't look like "add an axiom" but more like "start over everything from scratch"... Except I'm not sure it ever happened

Bas Spitters (Jul 07 2022 at 12:52):

Yes, UA won't be a small change. My question was just whether we believe we claim to understand how the bazar model should work for mathematics, say, based on opam.

Paolo Giarrusso (Jul 07 2022 at 13:27):

One possibility is that you will have multiple interfaces for related concepts (e.g. decidable equality) that do not interoperate well. That is what we already see in Coq libraries, and what we see in usual programming ecosystems...

Karl Palmskog (Jul 07 2022 at 13:37):

the current bazaar model is unfortunately mostly about people putting Coq math code in an ever growing number of GitHub repos, compatible with different versions of Coq (if any), and not really telling anyone about them. The Platform helps by coordinating some of the more basic/foundational libraries. But the Platform can't account for more exotic math and one-off proofs

Paolo Giarrusso (Jul 07 2022 at 13:42):

Karl Palmskog (Jul 07 2022 at 13:44):

the problems are: (1) not compatible with the same Coq version(s), (2) nobody knowing that they exist (not in any archive like AFP). That's what the "unfortunately" refers to.

Karl Palmskog (Jul 07 2022 at 13:46):

there are other issues of course, like homemade build scripts that don't work, ad-hoc dependency management, no explicit (open source) license, etc.

Paolo Giarrusso (Jul 07 2022 at 13:51):

For libraries that would be useful in the ecosystem, agreed.
OTOH, expecting that all programs in some language must live in some central archive still seems strange — you explained it to be once but clearly I wasn't convinced :sweat_smile: .

Karl Palmskog (Jul 07 2022 at 13:58):

I don't mind if there are several archives managed by different people. But right now you are basically forced to use GitHub code search to find elementary Coq math code

Karl Palmskog (Jul 07 2022 at 14:00):

I also think there is a difference between "registering" that your code exists in an archive, such as via opam metadata, and actually putting code in a central repository, like what they do with AFP

Karl Palmskog (Jul 07 2022 at 14:01):

for Coq code produced by people paid by tax money, it seems obvious that you should make others aware of the code by registering it in an archive or two, so taxpayers get some value out of the whole project

Emilio Jesús Gallego Arias (Jul 07 2022 at 14:28):

Yes, I mean a common system to implement objects in Coq; we have two and the two have problems, HB indeed may solve that, but it is not part of Coq, moreover it has some non trivial engineering challenges (depends on a full-blown LProlog interpreter, requires learning a new language, etc....)

Emilio Jesús Gallego Arias (Jul 07 2022 at 14:28):

Compare how easy is in Lean to say "this is my new type, please derive decidable equality for it"

Paolo Giarrusso (Jul 07 2022 at 14:31):

It's almost as easy with TCs in Coq — modulo exponential blowups with TCs hierarchies... IIUC Lean's hash-consing fixes that

Emilio Jesús Gallego Arias (Jul 07 2022 at 14:31):

Emilio Jesús Gallego Arias (Jul 07 2022 at 14:32):

Paolo Giarrusso (Jul 07 2022 at 14:39):

that needs a metaprogram in both languages — but with TCs it would only generate one instance, like in Haskell

Paolo Giarrusso (Jul 07 2022 at 14:39):

so the metaprogram is easier to write and to debug for its authors, and probably also for the users

Emilio Jesús Gallego Arias (Jul 07 2022 at 14:40):

Paolo Giarrusso (Jul 07 2022 at 14:40):

Emilio Jesús Gallego Arias (Jul 07 2022 at 14:40):

Enrico Tassi (Jul 07 2022 at 14:41):

Paolo Giarrusso (Jul 07 2022 at 14:42):

#[global] Instance: EqDecision Client_metadata.
Proof. solve_decision. Defined.

is almost as easy as [@deriving equality]; I'm sure you could bridge the difference with elpi.

Enrico Tassi (Jul 07 2022 at 14:43):

This almost works already IMO #[global] Instance: EqDecision Client_metadata := ltac:(solve_decision).

Paolo Giarrusso (Jul 07 2022 at 14:46):

deriving should also generate statements like #[global] Instance: EqDecision X -> EqDecision (container X). . Also deriving A, B, C is more compact than stating those separately

@Enrico Tassi re "leaking", I'm wondering how leaky is the HB abstraction. While it's nice that you can generate N hints, is it possible that in some cases the user the user will have to _understand_ something about those N hints? They might come up when debugging traces at least.

Enrico Tassi (Jul 07 2022 at 14:48):

Well, it is as tight as a Coq abstraction can be. I mean, we put stuff in inner modules to hide it. If you import these, or explicitly say Builders__11.foo then you will be punished ;-)

Enrico Tassi (Jul 07 2022 at 14:49):

Paolo Giarrusso (Jul 07 2022 at 14:49):

Paolo Giarrusso (Jul 07 2022 at 14:51):

and while "as tight as a Coq abstraction can be" is cool and impressive, I think in this thread it's fair to ask if it's also as tight as a _Lean_ abstraction can be.

Enrico Tassi (Jul 07 2022 at 14:51):

Yes, CS instances mention these constants. And they must be transparent. Typically the user does not see them (implict args) but if you set printing all and the unfold them (they are decently named, and have long names by design) then you see the curft

Enrico Tassi (Jul 07 2022 at 14:52):

The best I could imagine is to instruct the pretty printer and stuff like unfold to insist not doing what you ask.

Enrico Tassi (Jul 07 2022 at 14:52):

Enrico Tassi (Jul 07 2022 at 14:54):

I'm personally OK with the "python way", if something is called __private then you don't use it. It is what we try to do in HB when we have no other option.

Paolo Giarrusso (Jul 07 2022 at 14:55):

hiding those from pretty printing sounds like what people regret about primitive projections, so please ask PMP before doing it

Paolo Giarrusso (Jul 07 2022 at 14:55):

but again, I suspect this wasn't the question. Let's assume HB is the perfect solution within the constraints of Coq!

Enrico Tassi (Jul 07 2022 at 14:56):

Not hiding really, I mostly would like to avoid copy/pasting these terms, since their names are not part of the "API"

Paolo Giarrusso (Jul 07 2022 at 15:00):

Pedro Abreu (Jul 07 2022 at 15:00):

To be entirely honest it seems to me that this discussion once again comes down to documentation + UX. As Emilio points out, Lean has a well documented form of deriving equality (that any introductory user can understand what's going on), but we if you want to do it in Coq you'd need to come to the Zulip to figure it out and rely on some lifting of type classes instantiations.

Paolo Giarrusso (Jul 07 2022 at 15:02):

@Pedro Abreu UX and documentation in Coq are not ideal, but some of those problems aren't fixable purely via UX

Karl Palmskog (Jul 07 2022 at 15:02):

it's highly unlikely that any way of deriving instances will be the "official" one in Coq, so documentation will be specific to type classes and canonical structures, and to specific libraries which enhance those instances

Karl Palmskog (Jul 07 2022 at 15:04):

maybe what someone will do is to make a custom Coq for typeclasses with Stdpp, and then bundle it with a bunch of stuff and docs (a specialized Platform)

Karl Palmskog (Jul 07 2022 at 15:06):

on the MathComp side, it seems likely we will eventually get a workflow for Coq+MC without the stdlib - so in practice the only way to work there will be via canonical structures (which may get instance derivation via HB, Elpi, etc.)

Pedro Abreu (Jul 07 2022 at 15:06):

@Paolo Giarrusso I understand that, and it's ok. My main point here is that this sort of usability seems to be a main concern for Lean to begin with, and that gets them good points with new users. I don't know much about lean, but that's the impression that I'm constantly having, specially when we talk about usability for mathematicians, no?

Enrico Tassi (Jul 07 2022 at 15:13):

I agree with the observations, but given the traffic on Lean's zulip I imagine good doc and ergonomy is not the ultimate solution, even for them.

Enrico Tassi (Jul 07 2022 at 15:14):

This does not mean Coq should not get better doc, even if there can't be just one, since the ecosystem is less uniform, for the good and the bad

Paolo Giarrusso (Jul 07 2022 at 15:15):

Paolo Giarrusso (Jul 07 2022 at 15:16):

I guess _one_ possible question is (a) will Lean's momentum overtake Coq? (b) Is that a problem, and if so should there be a strategy to address that?

Paolo Giarrusso (Jul 07 2022 at 15:17):

Note that (a) isn't clear — I haven't seen significant Lean adoption in verification, they haven't migrated to Lean 4, Lean 3 seems much slower, etc etc

Enrico Tassi (Jul 07 2022 at 15:23):

The only clear thing to me is that many mathematicians got interested in that tool, and I believe the snowball effect played a major role. I don't think most of them did really scrutiny other systems. People doing math in Coq (for a long time) are clearly not so happy all this new blood went there, but at the same time I'm not so sure that having a [@derive] or a nicer UI and doc would have changed this in a radical way.

Karl Palmskog (Jul 07 2022 at 15:24):

unless Coq devs get defunded across France in a big way for some reason, I think things will keep going as usual. We have releases rolling out, and Platform projects ticking along. Is growth a requirement? I'd like to see more new faces/hands working on stuff in Coq-community, for example, but we tick along there too.

Enrico Tassi (Jul 07 2022 at 15:26):

Karl Palmskog (Jul 07 2022 at 15:28):

Paolo Giarrusso (Jul 07 2022 at 15:29):

I've been overly negative, but if Coq is hamstrung by backward compatibility, I wonder if or when it might be time for "Coq 9". @Arthur Charguéraud's recent talk had also some strategic suggestions.

Paolo Giarrusso (Jul 07 2022 at 15:32):

or even if it's not Coq 9, larger incremental breaking changes: there is only so much bug-to-bug compatibility that a project can sustain, and current and new users will keep suffering those bugs.

Bas Spitters (Jul 08 2022 at 11:36):

@Paolo Giarrusso how do you see the contribution of the iris group to the coq-community?
Is it working as one would hope. I believe the main libraries are in platform, but I could be wrong.

Karl Palmskog (Jul 08 2022 at 11:40):

@Bas Spitters I think we should keep Coq-community (the GitHub organization) and the Platform and the general Coq community (no hyphen) separate conceptually. The Platform shares people with Coq-community, but the goals are very different. Most projects in the Coq Platform are not in Coq-community.

Paolo Giarrusso (Jul 08 2022 at 11:41):

And there's also a distinction between the Coq community and coq-community: Bas did you mean the latter?

Paolo Giarrusso (Jul 08 2022 at 11:41):

Those libraries are in the platform indeed... But can you elaborate on the rest of the question?

Karl Palmskog (Jul 08 2022 at 11:41):

from my point of view, the Platform-to-Iris connection seems to be working well (we get releases of stdpp and Iris itself for every Platform release so far).

It would be nice with more Iris-related projects joining the Platform or at least having regular releases.

Karl Palmskog (Jul 08 2022 at 11:43):

as for Iris and Coq-community (with hyphen), I think the connection is very weak (the only one I can think of is that Ralf maintains autosubst1 in Coq-community), but I think that's not really an issue for either party

Bas Spitters (Jul 08 2022 at 11:48):

Karl Palmskog (Jul 08 2022 at 11:55):

@Bas Spitters as one example Aneris (and Actris) would be most welcome in the Coq opam archive, and possibly also in the Coq Platform

Stream: Miscellaneous

Topic: Kevin Buzzard interview about Lean

Jim Fehrle (Jul 01 2022 at 17:32):

Notification Bot (Jul 01 2022 at 17:56):

Karl Palmskog (Jul 01 2022 at 17:57):

Paolo Giarrusso (Jul 01 2022 at 18:17):

Karl Palmskog (Jul 01 2022 at 18:23):

Paolo Giarrusso (Jul 01 2022 at 19:18):

Paolo Giarrusso (Jul 01 2022 at 19:20):

Paolo Giarrusso (Jul 01 2022 at 19:22):

Paolo Giarrusso (Jul 01 2022 at 19:28):

Enrico Tassi (Jul 01 2022 at 20:01):

Karl Palmskog (Jul 01 2022 at 20:10):

Karl Palmskog (Jul 01 2022 at 20:12):

Enrico Tassi (Jul 01 2022 at 20:19):

Karl Palmskog (Jul 01 2022 at 20:29):

Karl Palmskog (Jul 01 2022 at 20:30):

Paolo Giarrusso (Jul 01 2022 at 20:30):

Paolo Giarrusso (Jul 01 2022 at 20:31):

Paolo Giarrusso (Jul 01 2022 at 20:40):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:20):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:20):

Karl Palmskog (Jul 03 2022 at 14:46):

Enrico Tassi (Jul 03 2022 at 14:46):

Karl Palmskog (Jul 03 2022 at 14:48):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:51):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:52):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:52):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:52):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:52):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:52):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:53):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:53):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:53):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:53):

Karl Palmskog (Jul 03 2022 at 14:54):

Karl Palmskog (Jul 03 2022 at 14:55):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:58):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:58):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:59):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:59):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:59):

Emilio Jesús Gallego Arias (Jul 03 2022 at 14:59):

Emilio Jesús Gallego Arias (Jul 03 2022 at 15:00):

Emilio Jesús Gallego Arias (Jul 03 2022 at 15:00):

Karl Palmskog (Jul 03 2022 at 15:14):

Emilio Jesús Gallego Arias (Jul 03 2022 at 15:43):

Karl Palmskog (Jul 03 2022 at 15:46):

Enrico Tassi (Jul 03 2022 at 19:22):

Bas Spitters (Jul 06 2022 at 08:04):

Michael Soegtrop (Jul 06 2022 at 08:46):

Théo Zimmermann (Jul 06 2022 at 09:42):

Emilio Jesús Gallego Arias (Jul 06 2022 at 11:17):

Emilio Jesús Gallego Arias (Jul 06 2022 at 11:17):

Emilio Jesús Gallego Arias (Jul 06 2022 at 11:18):

Paolo Giarrusso (Jul 06 2022 at 12:13):

Théo Zimmermann (Jul 06 2022 at 12:30):

Théo Zimmermann (Jul 06 2022 at 12:30):

Paolo Giarrusso (Jul 06 2022 at 14:02):

Bas Spitters (Jul 07 2022 at 06:01):

Karl Palmskog (Jul 07 2022 at 08:21):

Bas Spitters (Jul 07 2022 at 09:08):

Paolo Giarrusso (Jul 07 2022 at 12:47):

Paolo Giarrusso (Jul 07 2022 at 12:49):

Bas Spitters (Jul 07 2022 at 12:52):

Paolo Giarrusso (Jul 07 2022 at 13:27):

Karl Palmskog (Jul 07 2022 at 13:37):

Paolo Giarrusso (Jul 07 2022 at 13:42):

Karl Palmskog (Jul 07 2022 at 13:44):

Karl Palmskog (Jul 07 2022 at 13:46):

Paolo Giarrusso (Jul 07 2022 at 13:51):

Karl Palmskog (Jul 07 2022 at 13:58):

Karl Palmskog (Jul 07 2022 at 14:00):

Karl Palmskog (Jul 07 2022 at 14:01):

Emilio Jesús Gallego Arias (Jul 07 2022 at 14:28):

Emilio Jesús Gallego Arias (Jul 07 2022 at 14:28):

Paolo Giarrusso (Jul 07 2022 at 14:31):

Emilio Jesús Gallego Arias (Jul 07 2022 at 14:31):

Emilio Jesús Gallego Arias (Jul 07 2022 at 14:32):

Paolo Giarrusso (Jul 07 2022 at 14:39):