My version of offline mathlib help and TryLean4 Windows

Stream: general

[Jz Pan]

I'd like to share my attempt of offline mathlib help (and, with a lower priority, TryLean4 Windows bundle).

The repository is https://github.com/acmepjz/TryLean4Bundle1.

It contains two version of code of offline mathlib help, with the same feature.

• The first one is Windows PowerShell version of offline Mathlib help launcher, with a little bit better GUI.
• The second one is cross platform Python version of offline Mathlib help launcher.

Instructions for Python version:

1. Download OfflineMathlibHelpPython.zip (if CI uploads that file to release) or clone the repository.
2. Download and put doc.zip next to the script file, or use built-in update feature in script file.
3. chmod a+x TryLean4Launcher.py
4. ./TryLean4Launcher.py or python3 TryLean4Launcher.py
5. The GUI should be self-explanatory.

Currently the CI is configured to run once a week, so the offline Mathlib help will not be too out-of-date. The update feature in the script will allow you to update the offline Mathlib help data fairly easily.

I'd like to here some feedbacks.

[Jz Pan]

cc @Riccardo Brasca @Filippo A. E. Nuccio as I've promised the built-in update feature last month

[Filippo A. E. Nuccio]

I must say that I tried it last month and it is awesome: I recommend it very much. I will soon try to test the new version and give some feedback.

[Filippo A. E. Nuccio]

Is the button "Update offline mathlib help" meant to be "Update offline mathlib documentation"?

[Filippo A. E. Nuccio]

Concerning the update : I've run the above button and then launched the help=docs. The first page says that it has been built using commit https://github.com/leanprover/lean4/tree/045d07d2349b9989278991fbcd79a6430032930d which is some 2 months old, I think.

[Filippo A. E. Nuccio]

Am I doing something wrong?

[Jz Pan]

Filippo A. E. Nuccio said:

Is the button "Update offline mathlib help" meant to be "Update offline mathlib documentation"?

Yes. I think all "mathlib help" should be changed to "mathlib documentation". Sorry for my poor English.

[Jz Pan]

Filippo A. E. Nuccio said:

Concerning the update : I've run the above button and then launched the help=docs. The first page says that it has been built using commit https://github.com/leanprover/lean4/tree/045d07d2349b9989278991fbcd79a6430032930d which is some 2 months old, I think.

I don't think it should happen. What's the version of mathlib docs it reports? I.e. in the dialog pop up when you click the "update" button. (If you're on windows, when that dialog is in focus, press Ctrl+C will copy the contents of the dialog.)

This is my version:

730e4db21155a3faee9cadd55d244dbf72f06391
2025-06-06T23:07:12.000Z

(And I think a newer version will be automatically build on Saturday.)

When I launch the offline mathlib doc, the front page shows version https://github.com/leanprover/lean4/tree/6741444a63eec253a7eae7a83f1beb3de015023d which is the same as that in https://leanprover-community.github.io/mathlib4_docs/.

Remark: Please note that this version is not the mathlib version, but only the Lean4 version. To see mathlib version, navigate to any declaration in mathlib (for example Nontrivial), then its "source" link will provide the real version of mathlib. It is https://github.com/leanprover-community/mathlib4/blob/730e4db21155a3faee9cadd55d244dbf72f06391/Mathlib/Logic/Nontrivial/Defs.lean#L23-L27 which is the same version reported by the above dialog.

Could you check it again?

[Filippo A. E. Nuccio]

Sorry if it took too much, here a screenshot of the popup when I click on update (I am sorry, I do not know how to copy-paste...):
image.png

[Filippo A. E. Nuccio]

The lean version is the same as the online one.

[Filippo A. E. Nuccio]

mathlib is at least as updated as last week

[Filippo A. E. Nuccio]

so I think I was doing something wrong from the start. Let me ping @Antoine Chambert-Loir and @Thomas Browning with whom I was discussing this beautiful tool some minutes ago.

[Jz Pan]

Seems that the contents in the window get blurred (technically, it's called that "the program is not DPI aware"). Let me figure out how to fix it.