Formalizing unfinished proofs and external citations

Stream: general

[Andrej Bauer]

A while ago, in the prenatal stages of the Formal abstracts project by Tom Hales et al., we experimented with formalizing code that is not finished, and code that refers to external references (such as published papers). The experiment still works, somewhat amazingly, at https://github.com/andrejbauer/formalabstracts You can look at meta_data.lean for some explanation and the definitions, and the fabstract folder for usage examples.

Anyhow, the idea is to replace the rather uninformative sorry with a more structured and manageable way of introducing unfinished business with a new unfinished keyword, which equips some unfinished proof or construction with a description (informal text, references to literature, etc.).

If there's some interest in this sort of thing, I can prepare a pull request for the library so that we can discuss the possibility of introducing this sort of thing.

[Kevin Buzzard]

Reid Barton introduced such a keyword: todo, which is only used in the roadmap directory of mathlib, and not in src.

[Andrej Bauer]

Ah, very good. I am proposing a significant upgrade to todo. It's like a todo which carries information (informal description, references, citations). Are sorry's in mathlib proper forbidden?

[Johan Commelin]

Yep (-; The roadmap directory is the only place where sorry-like things are allowed (for now).
Personally I think src/ should always remain sorry-free.

[Johan Commelin]

But providing a richer experience to sorry with something like unfinished sounds like a very good idea to have in mathlib.

[Johan Commelin]

If only to have it available in projects that depend on mathlib.

[Andrej Bauer]

Ok, I can make some light-weight functionality and will issue a PR. Where would this go, in src/meta or in src/tactic?

[Johan Commelin]

src/tactic, I think.

[Bryan Gin-ge Chen]

@Andrej Bauer Our CI scripts only work fully for branches in the main mathlib repo, so we prefer PRs made from branches of mathlib rather than forks. I've sent you an invite: https://github.com/leanprover-community/mathlib/invitations

[Andrej Bauer]

Thanks. Is there a technical reason for breaking the received wisdom about forks and PRs?

[Eric Wieser]

Yes, because the CI scripts need a secret token to upload the built artefacts centrally

[Kevin Buzzard]

And because mathlib is so big now that I can't review a PR which touches a file high up in the import heirarchy unless the system is also offering me fully compiled oleans of the PR

[Andrej Bauer]

So in principle if someone else sets up the CI for themselves, then they could issue PRs, but it's technically more demanding to set up the CI (and it requires resources). If you get really popular, you won't be able to just inviite everyone who wants to make a PR, but I suppose you'll cross that bridge when you come to it :-)

[Alex J. Best]

The compiled oleans are uploaded via CI to oleanstorage.azureedge.net which is a URL hardcoded in the python script leanproject, this storage is only writable by the mathlib CI (so its not free storage for anyone else!) and allows anyone who wants to inspect your PR to very conveniently get a built version of mathlib with your PR included (with leanproject get-cache). So its more than just more demanding to setup the CI for you, currently you'd be asking any reviewers to go through a non-standard process to get oleans for your branch (or build them themselves) and therefore make the review process more involved for them if you don't use the existing mechanism.

This is not dissimilar to the Sage computer algebra system (a fairly large and long-running project), which has a centralised git repo called trac that everyone signs up for an account on, and then patchbots that build sage for all branches to check for errors.

[Andrej Bauer]

I see. Thanks for the explanation.