Keep working on disconnect from network

[david-a-wheeler]

After viewing the metamath-lamp page and downloading the mm database (set.mm), I often end up disconnected (especially on my phone, but also sometimes my laptop).

It'd be nice if metamath-lamp kept working during a disconnect, as long as the app and relevant database(s) were downloaded.

[expln]

I tested this situation and metamath-lamp kept working for me. Do you see any error after a disconnect? Or any functionality stops working? As I know, metamath-lamp keeps working after a disconnect until you refresh the page.

[expln]

@david-a-wheeler

Hi David. Could you please provide more details on the disconnect issue? As I wrote in my last comment, mm-lamp keeps working on disconnect.

[expln]

Looks like I reproduced this issue. I worked in mm-lamp on my phone. Then I locked the phone. I wanted to resume my work in about 4 hours. But the page with mm-lamp was reloaded automatically as soon as I opened it.

I think this depends on the browser. Looks like browsers on phones reload pages after some time of inactivity. I never experienced such auto reloads in browsers on laptops. Mm-lamp doesn’t have any functionality to reload itself. I don’t think I can do anything with that. But I will leave this issue open as a reminder that this problem exists.

[david-a-wheeler]

Ah, thanks! It does look like it's especially likely when you lock a phone. I did find this:
https://stackoverflow.com/questions/59085507/is-there-a-function-to-stop-mobile-android-browser-from-automatically-reloading

[expln]

This confirms my guess that this is purely a browser issue and I will not be able to resolve it. Thanks for the research. Do you think this issue may be closed? Or you have any idea how this can be resolved?

[david-a-wheeler]

Let me do a little research first. In some sense all that matters is that it can impact users. If there's a workaround, we should document it (or implement it if there is one).

[david-a-wheeler]

Basically, we want to discourage the web browser from discarding this page, especially if the user knows they're about to lose Internet connectivity.

Here are some useful pointers:

• On desktop Chrome you can view chrome://discards to see potential discard state. A lot of information is here: https://developer.chrome.com/docs/web-platform/page-lifecycle-api#testing-your-app-in-the-frozen-and-discarded-states
• There are various heuristics. For example, a page that is hidden but is showing an alert is prioritized so it's NOT likely to be discarded. More about the heuristics are here: https://docs.google.com/document/d/1QJpuBTdllLVflMJSov0tlFX3e3yfSfd_-al2IBavbQM/edit?tab=t.0#heading=h.5hz2j9h1wysg

I've learned that in Chrome there's a setting called "Always keep these sites active" ("Sites you add will always stay active and memory won't be freed up from them"), where you can "add sites manually". Firefox & other browsers may have similar mechanisms. Testing is needed, but if that would solve the problem, it should be documented. Then people (like me) can prevent the reload.

[expln]

Thanks for the ideas. I will check.

[david-a-wheeler]

At the very least, we can add something like this to the documentation:

Preventing discards for disconnected operations

Once this application loads whatever database it needs, it can work without an internet connection (aka "disconnected operations"). However, web browsers often discard tabs to save memory, under the presumption that they can reload data later. Obviously reloading information from the internet won't work if there's no internet connection.

If you know you will lose your internet connection, you may be able to keep using the application if you plan ahead. The details depend on your web browser:

• If you're using the desktop Chrome web browser, you can open the URL chrome://discards/, and look for the row for "Metamath lamp" (URL https://expln.github.io/lamp. Go to the column "Auto Discardable" and click its toggle so it shows an "X" (do not auto discard).
• In all browsers, try to keep that tab visible. Browsers generally try to avoid discarding tabs if they are currently visible.

[expln]

Yes, this is a good note. Will you add it?

As of working completely offline, I can add a JavaScript script which should be launched with node.js. This script will start a local web server and serve mm-lamp resources. This will work completely without internet.