UniMath/agda-unimath

Navigation is impossible on mobile

Closed this issue · 11 comments

So I was having a quick look at our website this morning on my phone, and at first I noticed this button at the bottom that doesn't go anywhere:
Screenshot_20231004_081729_com.brave.browser.jpg

Then I tried to use the side bar, but apparently it doesn't display:
Screenshot_20231004_081816_com.brave.browser.jpg

Same in Chrome:
Screenshot_20231004_082034_com.android.chrome.jpg

Oh no! In the past it worked fine. I’ve used the mobile version before and the website was usable.

I also noticed that when you search for something you get a screen with file titles and lists of content creators:

IMG_5357

It would probably be more useful if we would display a portion of the Idea section there

Interesting. I can reproduce the behavior, but that must be a recent thing, because even last week I used my phone to look at the website and everything was alright. I'll try to track it down and fix it.

It would probably be more useful if we would display a portion of the Idea section there

I'm not sure how much influence we have over these results; we're using mdbook's search feature, which delegates to a third party library. I was already thinking that the results could be more useful, but I don't have a concrete proposal, and in the worst case we'd have to reimplement the search ourselves, which TBH isn't something I'd like to spend time on right now.

It would probably be more useful if we would display a portion of the Idea section there

I'm not sure how much influence we have over these results; we're using mdbook's search feature, which delegates to a third party library. I was already thinking that the results could be more useful, but I don't have a concrete proposal, and in the worst case we'd have to reimplement the search ourselves, which TBH isn't something I'd like to spend time on right now.

Fair enough:)

Update: I'm pretty sure it's caused by this change in mdbook rust-lang/mdBook#2175. It changed some default assets which we're overriding, so I'll try to port them over and see if it fixes the issue. I'll pin the versions of mdbook and the other mdbook- packages in the installation script and in the CI, so that things like this don't happen in the future.

Well done for finding what caused the issue!

But is pinning a version of mdbook really the right idea? Sure, it will guarantee that our website doesn't break because of changes to mdbook. On the other hand, over time we will be stuck to an outdated version of mdbook and I'm not sure why we would want that.

Well nothing prevents us from updating the pinned version in the future, but it will be our choice. Currently I'd bet there is even a discrepancy between the CI version of mdbook and the version that contributors have installed, because the latter depends on when they run make install-website-dev (for example, what do you get when you run mdbook --version? The CI uses 0.4.35, which had these breaking changes).

The status quo is the worst of both worlds - we have no control over the version of mdbook installed, we need to notice the breakage, and we still need some manual intervention to port our assets, and in the meantime the website is broken. By pinning the version of mdbook we at least have control over when we want to dedicate some time to porting to a new release (and to be honest, looking at the changelog for the last few versions, I don't think we really benefit from staying on the bleeding edge anyway).

Alright! Let's pin the version ot 4.34 then:)

I'm on it 👌

The previous PR didn't actually fix the issue, the new one #819 should.

Thank you for resolving the main issue, @VojtechStep! However, I'd like to note that the navigation buttons on the bottom of the webpage still don't seem to work. I'll open a new issue for that, and I don't think it is as pressing as the issue you resolved previously.