archive

Stream: mathlib4

[Anatole Dedecker]

How hard would it be to run mathport on archive/ and counterexamples/? It's obviously not high priority but it would be nice to have if that's not too much work.

[Anatole Dedecker]

Actually, where are we supposed to put these files in mathlib4?

[Jon Eugster]

I thought there was a discussion about this recently here on zulip and there is work planed to make mathport work on them too

[Jon Eugster]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/leanproject.20--port-complete/near/361131341

near this message it seems

[Anatole Dedecker]

Yes I know about this discussion, and that the output was that we want to port these files. My question was wether we could setup the same infrastucture as for other files, or if we had to port them by hand.

[Mario Carneiro]

porting them by hand is certainly not necessary, mathport can definitely do this, but there are some infrastructure questions about where exactly the output is supposed to go (in mathlib3port and mathlib4)

[Eric Wieser]

Porting one file by "hand" (with one-shot) is probably reasonable as an exercise in working out how to set up the infrastructure in mathlib4

[Eric Wieser]

Or alternatively, pick a new IMO problem to formalize from scratch!