Reservoir search results

Stream: general

[Rick de Wolf]

Just a quick observation - when I try to search for 'paperproof', 'paper proof', or 'paper-proof' in Reservoir I get zero search results, even though Paperproof is number three on the list of most popular packages. Maybe the search algorithm needs some tuning or changes?

[Kim Morrison]

CC'ing @Mac Malone

[Julian Berman]

I think one of the criteria is it needs to be a repo which is majority Lean? (And paperproof appears to be majority typescript)

[Julian Berman]

Oh, no, not sure where I got that from, but https://reservoir.lean-lang.org/inclusion-criteria doesn't say it, so never mind me.

[Rick de Wolf]

Just for clarification, Paperproof is listed in Reservoir, but it can't be found by using Reservoir's search.

[Mac Malone]

The problem here is partly reservoir#33. The name of root package in paper-proof is examples, which causes it to be indexed under that name.(Papeproof's manifest needs updating.) Since searching by owner is not yet supported, this means finding it by search sadly does not yet work.

[Mac Malone]

Reservoir is my current focus, so hopefully I should be be able to solve the search issue soon.

[Rick de Wolf]

Ahh I'd noticed that naming issue because one of my bookmarks was broken, I figured it wouldn't have anything to do with this.

[Rick de Wolf]

I sent a message to one of the Paperproof contributors earlier, I'll remember to bring up the manifest update when they reply.

[Rick de Wolf]

Also, the reservoir#33 link you sent points to the previous home of reservoir in a different Github organization. I think that has something to do with Zulip automatically generating links? Do you know who to CC to fix this?
Nevermind, it works just fine for me.

[Julian Berman]

(Sorry, I should have mentioned here, @Bryan Gin-ge Chen fixed it here it just doesn't update links posted prior to the fix, which ... TIL.)

[Johan Commelin]

I also can't find "mathematics in lean"

[Rick de Wolf]

Julian Berman said:

(Sorry, I should have mentioned here, Bryan Gin-ge Chen fixed it here it just doesn't update links posted prior to the fix, which ... TIL.)

I wasn't expecting a fix to drop in the middle of convo :rolling_on_the_floor_laughing: thanks for the quick fix Bryan

[Kevin Buzzard]

I was interested to see which lean projects on github have mathlib as a dependency. I found mathlib on reservoir and clicked on "dependencies" and I get to this page, but this list can't be complete because FLT depends on mathlib and it's not in the list at that link, yet it is indexed by reservoir. What is the complete list?

[Kim Morrison]

It's a bug, which I reported yesterday at https://github.com/leanprover/lean4/issues/5371