Rob Lewis
Rob Lewis
It turns out there's a "standard trick" for doing this without search: see e.g. section 2.2 of https://arxiv.org/pdf/1007.3615.pdf . I'll investigate whether Sage/Singular supports this trick out of the box...
Note to self, the json changes here will need to be adapted when #15429 lands.
I've implemented the "standard trick" (see also 4.2 Prop 8 of Cox, Little, O'Shea). This is still pending docs, test updates, and #15428 (which I think is ready to go)....
Yes, there were merge conflicts with #15429 and I didn't resolve cleanly, apparently. This is effectively a reset of the PR -- the new implementation is unrelated to the old....
And I've marked this awaiting-review mostly for comments on: > While this approach is clearly better overall than the old "search up" approach, there's one downside, namely, it doesn't fall...
There are plans to overhaul the docs search, but I wouldn't expect changes in the immediate future.
This is great! Thanks Polly! Let's let GitHub do its thing and build it for all of us to try out: #deploy Or, maybe that needs to be in its...
Hmm, our deploy action is broken...
> It might not work for PRs opened from external forks? See e.g. [#115 (comment)](https://github.com/leanprover-community/doc-gen/pull/115#issuecomment-779953415) Aha, yes, that seems to be it. I think we can delete all of those...