Zulip Chat Archive

Lean is not a product. I work for Microsoft Research, and I can pick my own research projects. Nobody at Microsoft is expecting to make money with Lean.

Leonardo de Moura (Nov 16 2018 at 05:13):

@Kenny Lau

on the one hand me and kevin want to promote it
and on the other hand the big devs don't want it to be promoted

I know Lean has serious performance and usability problems. I tried to make this clear in the FAQ document https://github.com/leanprover/lean/blob/master/doc/faq.md. I told the CMU guys many times it was a bad idea to develop mathlib at this point, and that they were going to hit performance problems and bugs. There is no point in promoting the system at this point. It is useful as a playground for trying ideas, but it is not ready for serious use.

Kevin Buzzard (Nov 16 2018 at 08:57):

Kenny -- the ideas we are currently trying include "is dependent type theory actually robust enough in practice to deal with definitions and basic properties of the complex objects which serious research level mathematicians use in their daily work" and "is it possible to integrate formal proof verification systems into teaching of undergraduate mathematics". I'm having quite a lot of fun investigating these things. I think it's pretty clear at this point that there are no optimal choices for the underlying software. There are problems with Coq, problems with Lean, problems with Isabelle HOL, problems with univalent foundations -- there seems to me to be currently no good answer to "which system should we use". I am a mathematician and I cannot really help with these problems, which view as firmly living in the domain of computer science -- deciding whether it's this kind of type theory or that kind of type theory, and how the type class system should work, are not really things I can help with. This still seems to me to be a fairly young research area and what you are seeing is simply the consequences of the nature of cutting edge research. One thing I am convinced of is that to make progress with these questions we absolutely need to have mathematicians using this kind of software, so that is what I am promoting. Without mathematicians we're just going going to get more pieces of software and more proofs of Godel's incompleteness theorem. There is still a long journey ahead though. Maybe the software that mathematicians as a community end up using is some new piece of software that hasn't even been written yet.

One thing I've always been adamant about though is that Lean 3.4.1 is perfectly adequate as a tool for working with undergraduate level mathematics; I see evidence of this time and time again. I have to figure out how to really use it to help more people to actually learn and do undergraduate level mathematics, and this is something I am actively working on, and for which the CS problems are now solved -- Lean 3.4.1 will do fine.

Kenny Lau (Nov 16 2018 at 09:04):

how about adding the elaborator attributes back to nat.strong_rec_on and int.induction_on...

Bryan Gin-ge Chen (Nov 16 2018 at 09:44):

How hard is it to build a custom version of the lean web editor? Are the instructions at the "lean-web-editor" repo still up to date?

Patrick Massot (Nov 16 2018 at 10:03):

There was a lot of discussions about this at https://gitter.im/leanprover_public/lean_js?source=orgpage

Bryan Gin-ge Chen (Nov 16 2018 at 10:31):

I'm having trouble with the live version of the lean-web-editor in firefox (63.0.3) currently. The editor seems to work fine in Chrome though. In firefox, I'm not getting any messages when I type things like #eval 2+2 in the window. If I refresh the window with some #eval code in the URL, then I get multiple eval result messages, but when I start typing it seems to break again. I didn't have these issues a few months ago when I last seriously tried using the editor so maybe some recent changes to firefox has messed things up somehow.

Patrick Massot (Nov 16 2018 at 10:33):

I've always had trouble with the web editor in Firefox.

Bryan Gin-ge Chen (Nov 16 2018 at 10:37):

Also, I just tried following the instructions on the lean-web-editor repo and things seem to work (in chrome), except that when I tried to create an up-to-date version of library.zip by editing leanpkg.toml and running leanpkg upgrade and then mk_library.py, I get file '/library/init/default.lean' not found in the web-editor (served locally by webpack-dev-server). Chrome says that library.zip is loading, and when I unzip library.zip I do find init/default.olean.

Bryan Gin-ge Chen (Nov 16 2018 at 10:39):

(Everything works fine if I just use the library.zip downloaded using fetch_lean_js.sh)

Bryan Gin-ge Chen (Nov 17 2018 at 13:43):

OK, I managed to build a working library.zip. I had changed the lean_version in combined_lib/leanpkg.toml to nightly, so that leanpkg upgrade would put in an up-to-date commit of mathlib. But the instructions say "Make sure you run the same Lean version locally as the javascript version you target", so I changed it back to 3.4.1 and then running mk_library.py worked.

Still no idea how to solve the firefox issues, but outside of that I support what @Scott Morrison said in the lean_js gitter:

We might consider adding the lean-web-editor to a travis build, so that there is an online version that is always tracking mathlib (and we get notifications as soon as something breaks).
My guess is that this would be more appropriate at part of the mathlib travis build than the lean build.

Perhaps we could set up github pages for leanprover-community with a copy of lean-web-editor including an automatically compiled version of mathlib?

Bryan Gin-ge Chen (Nov 18 2018 at 19:48):

More on firefox issues: After playing around more with lean-web-editor and lean-client-js-browser, I think the issue is with the 3.4.1 wasm builds of lean. In particular, the 3.3.0 version works fine for me in firefox. Was something changed between 3.3.0 and 3.4.1 that could have broken firefox compatibility? @Gabriel Ebner @Sebastian Ullrich

Unfortunately, per earlier discussion here, compiling a wasm build with emscripten requires linux, so it will be hard for me to investigate this further on my own.

Bryan Gin-ge Chen (Apr 20 2019 at 02:09):

Update: I gave this another shot tonight and I was able to build lean 3.4.2 with emscripten on macOS with a few changes that I'm PR'ing to community lean. In the meantime it also looks like all the Firefox issues have gone away (at least in firefox 66.0.3).

Kevin Buzzard (Apr 20 2019 at 02:27):

Can you make a build which also imports mathlib and another arbitrary project? For things like an introductory analysis class, this is the sort of thing one would need.

Kevin Buzzard (Apr 20 2019 at 02:27):

Well done, by the way! I tried all this in 2018 and it was a nightmare.

Kevin Buzzard (Apr 20 2019 at 02:28):

@Mohammad Pedramfar this might be of interest to you.

Simon Hudon (Apr 20 2019 at 02:30):

@Kevin Buzzard I think we could make a build in the mathlib repo to check various versions of Lean against mathlib

Bryan Gin-ge Chen (Apr 20 2019 at 02:30):

Sure, you can do that with the mk_library.py script in lean-web-editor.

My impression was Mohammed was already able to get that working here though?

Bryan Gin-ge Chen (Apr 20 2019 at 02:31):

@Simon Hudon maybe we could have a community version of the lean web editor with an up-to-date version of mathlib / other libraries?

Kevin Buzzard (Apr 20 2019 at 02:32):

The last time I talked to him, it "worked" in the sense that if you went to the firefox page and then waited for ten minutes, everything would finish compiling and then things would work fine.

Simon Hudon (Apr 20 2019 at 02:33):

I'm all for but I know next to nothing about the web editor

Kevin Buzzard (Apr 20 2019 at 02:34):

If I can get lean + mathlib + xena running with zero start-up time in the Lean web editor I might be able to persuade my department to pay for hosting, because I will be able to use it for teaching.

Kevin Buzzard (Apr 20 2019 at 02:34):

xena is just an example -- any repo which I can update and then recompile and get it all working, reliably, will do.

Kevin Buzzard (Apr 20 2019 at 02:37):

(deleted)

Bryan Gin-ge Chen (Apr 20 2019 at 02:40):

On my laptop the editor starts working after a few seconds or so (including downloading files into the browser cache, etc.), though I'm just using mathlib and the other default libraries in the lean-web-editor leanpkg.toml . I haven't tried other packages there yet.

Simon Hudon (Apr 20 2019 at 02:41):

There is something in the Haskell community called Stackage. It's a curated collection of Haskell packages together with a version GHC (the main Haskell compiler) in which all the packages work together. I'd like to do that with Lean. Have a monthly snapshot of the Lean ecosystem in such a way that all the versions picked for every package work together. We make sure to test all of them together.

Mohammad Pedramfar (Apr 21 2019 at 20:42):

The last time I talked to him, it "worked" in the sense that if you went to the firefox page and then waited for ten minutes, everything would finish compiling and then things would work fine.

Oh, that problem is solved now. What I put up in github can turn a Lean code and turn it into an interactive version that works as fast as the original online lean. (It imports more things which can slow it down, otherwise it's the same).
I couldn't build lean with emscripten, so the code would download compiled lean javascript server.

Bryan Gin-ge Chen (May 15 2019 at 03:01):

Another update: the nightly releases of the community fork of Lean 3 now include the Emscripten build! If you want to try building it yourself, see these instructions. Thanks to @James King, @Gabriel Ebner, and especially @Simon Hudon for their help!

You can try it out online with a recent build of mathlib, where it powers a fork of the lean-web-editor. In the fork, I added:

a form to load .lean files from the web (try pasting a "raw" link from github like this into the form). You can also append #url=https://url/to/file.lean to the link, like this,
a button to load a .lean file from your computer into the editor,
a save button,
a basic "about" window (click the little purple ? button),
the ability to hide/show the header (click the colored bar at the very top), and
type information and docstrings for the term under the cursor are now displayed in the info view.
I also worked around an issue where the cursor position was incorrectly placed after inputting Unicode.

There are a few non-UI changes: I updated the mk_library.py script to compress library.zip (which cuts its size by a factor of 4) and also gave it command-line options. Finally, I edited the lean-client-js-browser dependency so this web editor's version of library.zip will be cached in your browser's IndexedDB storage and only be re-downloaded if necessary (this seems to be more reliable than the browser cache).

Johan Commelin (May 15 2019 at 05:10):

Wow, nice work! @Bryan Gin-ge Chen (and all the others)

Scott Morrison (Jun 05 2019 at 02:32):

Hi @Bryan Gin-ge Chen, how hard would it be to get a version online that uses a branch of mathlib?

Bryan Gin-ge Chen (Jun 05 2019 at 03:02):

Not hard at all; I tried to update the instructions in my fork here.

Bryan Gin-ge Chen (Jun 05 2019 at 03:05):

Which branch were you thinking of using? I can quickly upload another copy of the page if you want to just experiment with it.

Scott Morrison (Jun 05 2019 at 03:16):

Hmm... could you do back?

Scott Morrison (Jun 05 2019 at 03:16):

That would be amazingly lovely, and I would use it in a talk tomorrow.

Scott Morrison (Jun 05 2019 at 03:18):

hang on one sec, let me commit a few final things to it :-)

Bryan Gin-ge Chen (Jun 05 2019 at 03:19):

Yeah, it looks like it's not building at the moment...

Bryan Gin-ge Chen (Jun 05 2019 at 03:22):

Oh wait, how do I use a custom branch in leanpkg.toml again? I tried changing the commit and it doesn't seem to be working

Bryan Gin-ge Chen (Jun 05 2019 at 03:31):

Ah, I think I got it. Apparently comments aren't supported in leanpkg.toml.

Scott Morrison (Jun 05 2019 at 03:43):

I think I have decided my branch is too messy to actually give to people to use tomorrow

Scott Morrison (Jun 05 2019 at 03:43):

but I will be back to ask about this after tomorrow :-)

Wojciech Nawrocki (Jun 18 2019 at 14:16):

I came across this today: https://jscoq.github.io/

Bryan Gin-ge Chen (Jun 18 2019 at 14:42):

I saw this a few weeks ago too. I don't know enough (any) Coq to play around with it, but one feature it has which the lean-web-editor is missing is a "package manager" which loads Coq packages in the background as needed. I've been messing around with getting the lean-web-editor to be able to load different ZIP bundles on-the-fly, but it seems it would be much harder to get it to download only the necessary .olean files.

Simon Hudon (Jun 23 2019 at 02:41):

@Bryan Gin-ge Chen, I see you have Lean 3.5 running at https://bryangingechen.github.io/lean/lean-web-editor/. Can we get it hosted on leanprover-community?

Bryan Gin-ge Chen (Jun 23 2019 at 02:43):

Sure, it should just work if you mirror the files in this repo.

Bryan Gin-ge Chen (Jun 23 2019 at 02:47):

I'm about to push a new version with some minor changes and update mathlib too.

Simon Hudon (Jun 23 2019 at 02:47):

Cool, thanks! Would you mind creating a PR and link to it from https://github.com/leanprover-community/leanprover-community.github.io?

Bryan Gin-ge Chen (Jun 23 2019 at 02:59):

Sure, but what do you think the best approach is? I've been force-pushing a lot in my github.io repo in an attempt to avoid having lots and lots of versions of the library.zip file in the git history.

Bryan Gin-ge Chen (Jun 24 2019 at 01:51):

@Simon Hudon PR here. Thanks to @Scott Morrison for hosting a bunch of files on tqft.net!

Bryan Gin-ge Chen (Jun 26 2019 at 22:08):

The new version of the lean-web-editor is now hosted on the community github site! Not much has changed but it's a more official-looking link: https://leanprover-community.github.io/lean-web-editor

Note that if you're using the uBlock extension to block ads, you will need to add the following custom filter in order for the editor to work properly: @@||*$xmlhttprequest,domain=leanprover-community.github.io due to the rule discussed here.

Patrick Massot (Jul 01 2019 at 12:30):

Does anyone managed to use the Load .lean from URL: input from https://leanprover-community.github.io/lean-web-editor/? My browser keeps complaining about Cross-origin request security things

Patrick Massot (Jul 01 2019 at 12:40):

It does work if I copy the web-editor to my webpage. @Bryan Gin-ge Chen Is there a way to update the translations file, and maybe also to change the leader key? Even better, could we have the Tab key to trigger translations as in the VScode plugin? Is there any way to have custom imports without modifying library.zip?

Mario Carneiro (Jul 01 2019 at 12:52):

do you have any particular URLs as an example? I tried a few things and it seems to work

Mario Carneiro (Jul 01 2019 at 12:52):

also what browser are you using?

Patrick Massot (Jul 01 2019 at 12:52):

Firefox

Patrick Massot (Jul 01 2019 at 12:54):

Could you try https://www.math.u-psud.fr/~pmassot/enseignement/math114/tds/td1/td1.lean for instance?

Patrick Massot (Jul 01 2019 at 12:54):

It works in https://www.math.u-psud.fr/~pmassot/lean-web/#url=https%3A%2F%2Fwww.math.u-psud.fr%2F~pmassot%2Fenseignement%2Fmath114%2Ftds%2Ftd1%2Ftd1.lean but not on the official website

Mario Carneiro (Jul 01 2019 at 12:56):

ah yeah I get the same error:

Cross-Origin Request Blocked: The Same Origin Policy disallows reading the remote resource at https://www.math.u-psud.fr/~pmassot/enseignement/math114/tds/td1/td1.lean. (Reason: CORS header ‘Access-Control-Allow-Origin’ missing). [Learn more]

TypeError: NetworkError when attempting to fetch resource.

Mario Carneiro (Jul 01 2019 at 12:57):

still, there is a fix suggested in the error itself. Is it possible to serve this header?

Patrick Massot (Jul 01 2019 at 12:57):

serve from where?

Mario Carneiro (Jul 01 2019 at 12:59):

oh, that's actually a good question. I'm not sure if github needs to serve it or u-psud.fr

Patrick Massot (Jul 01 2019 at 13:00):

what kind of url did you try when you wrote it worked?

Mario Carneiro (Jul 01 2019 at 13:00):

GitHub raw lean files

Mario Carneiro (Jul 01 2019 at 13:00):

It's possible that GH-pages is actually on the same origin for that

Patrick Massot (Jul 01 2019 at 13:00):

Oh but that probably counts as "same origin"

Patrick Massot (Jul 01 2019 at 13:00):

yes

Mario Carneiro (Jul 01 2019 at 13:01):

In any case I'm not particularly surprised that this has happened. Browser security policies mostly don't allow unrelated sites to talk to each other like this

Patrick Massot (Jul 01 2019 at 13:02):

Then I think the Lean web editor should print something instead of hoping the user will open the dev console and check for errors...

Patrick Massot (Jul 01 2019 at 13:02):

Anyway I think I'll use a self hosted Lean web-editor since I need extra supporting Lean files

Patrick Massot (Jul 01 2019 at 13:02):

The translations and leader key questions are actually more important then

Bryan Gin-ge Chen (Jul 01 2019 at 13:03):

Re: CORS errors, to fix them directly, you'd have to talk to the server admin of www.math.u-psud.fr and get them to add Access-Control-Allow-Origin: * to the http response. One easy workaround is to use a CORS proxy, one that I just got to work was to use cors-anywhere, i.e. paste the URL:https://cors-anywhere.herokuapp.com/https://www.math.u-psud.fr/~pmassot/enseignement/math114/tds/td1/td1.lean into the web-editor's url form.

Patrick Massot (Jul 01 2019 at 13:03):

That's an interesting security feature...

Bryan Gin-ge Chen (Jul 01 2019 at 13:10):

I should be able to update the translations without too much trouble (what I may do is just fetch the most recent translations file from the vscode-lean github). The tab key thing will be a bit tougher, as it'll require me to figure out how to add new keybinds to the monaco editor.

Patrick Massot (Jul 01 2019 at 13:11):

Is there any access to this project for us? Do we have a community version somewhere? Or is it only the official repo and your private stuff? Is there any build documentation? I don't know much javascript but maybe other people could help

Bryan Gin-ge Chen (Jul 01 2019 at 13:12):

My fork isn't private, and I'd gladly accept contributions: https://github.com/bryangingechen/lean-web-editor

I did try to add to the documentation in the README, do let me know if you need any additional instructions

Bryan Gin-ge Chen (Jul 01 2019 at 13:13):

There should be a working link to that repo in the popup that appears if you click the purple ? button in the "header" of the web editor.

Patrick Massot (Jul 01 2019 at 13:16):

Thanks! I was looking at the wrong repo (https://github.com/bryangingechen/bryangingechen.github.io/tree/master/lean/lean-web-editor)

Patrick Massot (Jul 02 2019 at 13:24):

@Bryan Gin-ge Chen I tried following the instructions at https://github.com/bryangingechen/lean-web-editor and https://github.com/bryangingechen/lean-client-js but failed completely. I think I managed to get a recent node+npmthat doesn't complain. But then running npm run demo inside lean-client-js fails with various messages depending on where I try to put the content of https://github.com/leanprover-community/lean-nightly/releases/download/nightly-2019-06-24/lean-3.5.0-nightly-2019-06-24-browser.zip

Patrick Massot (Jul 02 2019 at 13:28):

I manage to run the web editor simply by cloning https://github.com/bryangingechen/leanprover-community.github.io/tree/master/lean-web-editor and opening the index page. Now I only want to add one library in addition to mathlib. Is there anything I can do which would not involve the crazy npm stack? Naively I would try to compile my lib using the community Lean 3.5 and hope to follow https://github.com/bryangingechen/lean-web-editor#creating-a-customized-libraryzip. Is that hopeless?

Patrick Massot (Jul 02 2019 at 13:46):

I give up until Bryan comes back. There is too much guesswork involved.

Patrick Massot (Jul 02 2019 at 13:47):

I can't even manage to use the community fork of Lean with mathlib

Patrick Massot (Jul 02 2019 at 13:48):

I get wonderful errors like "WARNING: Lean version mismatch: installed version is nightly-2019-06-24, but package requires leanprover-community-lean-nightly"

Rob Lewis (Jul 02 2019 at 14:12):

Hmm. The version at leanprover-community.github.io is failing now with the error The script at 'https://leanprover-community.github.io/lean-web-editor/lean_js_wasm.js' failed to load.

Patrick Massot (Jul 02 2019 at 14:13):

I didn't touch anything there!

Rob Lewis (Jul 02 2019 at 14:14):

Oh, I wasn't blaming you, just another note for Bryan when he gets back!

Bryan Gin-ge Chen (Jul 02 2019 at 14:36):

Oops! I'll fix the community lean web editor shortly. I forgot to change the URLs to point to Scott's site.

Edit: Fixed now!

Bryan Gin-ge Chen (Jul 02 2019 at 14:39):

I manage to run the web editor simply by cloning https://github.com/bryangingechen/leanprover-community.github.io/tree/master/lean-web-editor and opening the index page. Now I only want to add one library in addition to mathlib. Is there anything I can do which would not involve the crazy npm stack? Naively I would try to compile my lib using the community Lean 3.5 and hope to follow https://github.com/bryangingechen/lean-web-editor#creating-a-customized-libraryzip. Is that hopeless?

Sorry about the npm trouble. This second approach should indeed be possible. Let me try to figure out what's going on here.

Bryan Gin-ge Chen (Jul 02 2019 at 14:40):

I get wonderful errors like "WARNING: Lean version mismatch: installed version is nightly-2019-06-24, but package requires leanprover-community-lean-nightly"

This warning in particular is harmless; could you share the rest of the output of mk_library.py?

Bryan Gin-ge Chen (Jul 02 2019 at 14:40):

@Patrick Massot

Patrick Massot (Jul 02 2019 at 14:55):

Unfortunately I had to go back home where internet is currently broken (except on my phone). Could you try to document the full procedure to get a Lean web using a custom library built on top of mathlib?

Bryan Gin-ge Chen (Jul 02 2019 at 15:17):

So the first few steps are as in the instructions on my lean-web-editor README you linked. Afterwards, if you copied the contents of the lean-web-editor directory from the bryangingechen.github.io repo somewhere, you'll overwrite its library.zip, library.info.json, and library.olean_map.json with the files generated by mk_library.py.

Something seems to be unclear / wrong in the instructions I wrote in the README. It sounds like something is going wrong in step 4 when you're running mk_library.py but I need more output to figure out what is happening.

Patrick Massot (Jul 02 2019 at 15:25):

Unclear (to me) sentences include: "If you plan to use the prebuilt JS/WASM versions of Lean," and "lean_version needs to point to the same version of Lean as the Emscripten build of Lean you plan to use. "

Patrick Massot (Jul 02 2019 at 15:26):

I have no idea which version I'm using when I clone the community github.io site

Bryan Gin-ge Chen (Jul 02 2019 at 15:30):

The first sentence should perhaps say "If you plan to use the prebuilt JS/WASM versions of Lean downloaded from the leanprover-community/lean-nightly site, i.e. if you are not compiling Lean with emscripten yourself".

Patrick Massot (Jul 02 2019 at 15:33):

Ok, let's say I want to use such a download. What version of mathlib should I use then? More to the point: where are the corresponding mathlib binaries?

Bryan Gin-ge Chen (Jul 02 2019 at 15:33):

The second sentence needs to be rewritten completely. I realized that my instructions will give rise to the confusing warning you pointed out above. However, for current purposes, you can ignore it safely.

Also, I would suggest not cloning the community github.io repo, but rather the files in the bryangingechen.github.io repo instead because the version of the web editor app in the community repo grabs the dependencies from Scott's page rather than from the local folder.

Bryan Gin-ge Chen (Jul 02 2019 at 15:34):

You will have to recompile mathlib yourself since the olean files provided by e.g. update-mathlib are compiled with Lean 3.4.2, but the web-editor uses some version of Lean 3.5.0c

Bryan Gin-ge Chen (Jul 02 2019 at 15:34):

But the mk_library.py script will take care of compiling mathlib for you if you have edited leanpkg.toml as in the instructions (ignoring the harmless warning mentioned above).

Bryan Gin-ge Chen (Jul 02 2019 at 15:35):

You can put any commit of mathlib that you need in combined_lib/leanpkg.toml.

Patrick Massot (Jul 02 2019 at 15:46):

Ok, we really need Lean 3.5.0 versions of precompiled mathlib then. Compiling mathlib should happen only when working on mathlib

Patrick Massot (Jul 02 2019 at 15:47):

Thanks for all those explanations. I'll try again as soon as I'll get back to an internet enabled computer.

Mario Carneiro (Jul 02 2019 at 15:47):

The whole point behind the 3.5.0 release is to be compatible with 3.4.2

Mario Carneiro (Jul 02 2019 at 15:48):

3.5.1 is the backward-incompatible release

Bryan Gin-ge Chen (Jul 02 2019 at 15:48):

I agree about having precompiled mathlib. I meant to look into this with @Simon Hudon but forgot.

No problem! Your questions should help me improve the process.

Mario Carneiro (Jul 02 2019 at 15:48):

I think the warning should just be ignorable

Mario Carneiro (Jul 02 2019 at 15:49):

The olean files get the exact version number baked into them (down to the commit) so it's pretty likely for those to mismatch but that doesn't guarantee incompatibility unless lean has some silly requirement on top of everything else

Bryan Gin-ge Chen (Jul 02 2019 at 15:50):

It's true that it's compatible, but unfortunately Lean still checks the version info in the olean file under the hood and refuses to accept it if it differs. If I remember correctly there is a compile option to have Lean ignore that but it didn't seem like a good idea to turn it on even for the Emscripten build.

Mario Carneiro (Jul 02 2019 at 15:50):

I think we should just turn that check off then

Mario Carneiro (Jul 02 2019 at 15:53):

Given how we are trafficking in olean files a lot more than they were originally intended for, it's better to just try to load them and hope for the best. I don't think we are likely to change the serialization format in community lean any time soon

Mario Carneiro (Jul 02 2019 at 15:54):

It would be much better if the olean serialization had its own versioning system, because the vast majority of commits don't touch it

Bryan Gin-ge Chen (Jul 02 2019 at 16:00):

Right, that makes sense. It's even better for Emscripten Lean since the library/init files are bundled with library.zip. If someone wants to PR this, here's the relevant line.

Patrick Massot (Jul 03 2019 at 12:36):

@Bryan Gin-ge Chen I managed to run lean-web-editor with a custom library build on top of mathlib. Thank you very much for your help! Here are my notes/issue list:

I cloned mathlib, changed its leanpkg.toml so that it contains lean_version = "leanprover-community-lean-nightly"
I compiled mathlib, ignoring the lean version mismatch warning
In my custom lib leanpkg.toml, I used the same lean_version line as above, and in the [dependencies] section, I used mathlib = { path = "/home/pmassot/lean/mathlib_3.5" } featuring the path to my version of mathlib compiled using community Lean.
I cloned https://github.com/bryangingechen/lean-web-editor and edited combined_lib/leanpkg.toml to contain
[package] name = "combined_lib" version = "3.5.0" lean_version = "leanprover-community-lean-nightly" [dependencies] mathlib = {path = "/home/pmassot/lean/mathlib_3.5/"} lib114 = {path = "/home/pmassot/lean/lib114/"}
where lib114 is my custom lib built on top of mathlib.
Then I first to run mk_library.py. On the first try it complained the directory dist did not exist. So I created it. Then it complained my custom lib had no GitHub url. So I edited mk_library.py to use empty lib_info[lib_name] when the regex looking for GitHub failed. Then the script succeeded.
Then I cloned https://github.com/bryangingechen/bryangingechen.github.io, copied the content of lean/lean-web-editor to my website, and copied the three files created by mk_library.py into that directory in place of https://github.com/bryangingechen/bryangingechen.github.io/blob/master/lean/lean-web-editor/libcore.olean_map.json and its two friends.

That's all! It could clear use some ironing, but it works. TODO list:

solving the olean versionning check issue in Lean community
providing mathlib nightly compiled by community Lean 3.5.0, with a corresponding leanpkg.toml
disentangling combined_lib from the lean-web-editor repository, so that we don't need to edit the git repository to use the tool.
fix the non-existent dist folder and GitHub url check bugs in mk_library.py
make a user friendly script that download the precompiled website from https://github.com/bryangingechen/bryangingechen.github.io and move the output of mk_library.py
Document all that!
Thanks for all your work and help!

Patrick Massot (Jul 03 2019 at 13:51):

Next, I'll need to investigate @Mohammad Pedramfar's effort to integrate this with format_lean. I also have one more question: will I get a noticeable speed gain if I use a trimmed down mathlib? Or is it ignoring unneeded files in mathlib anyway?

Bryan Gin-ge Chen (Jul 03 2019 at 13:59):

Glad you got things working! And your writeup looks really helpful! I didn't even realize you could use local paths in leanpkg.toml until now...

There will be a speedup for the initial start of the web editor with a trimmed down mathlib. The dominant effect is due to shortening download times (though after the first run, the ZIP file is cached). A smaller ZIP file might also make a difference when the Emscripten loader sets up the file system, but this should be a much smaller effect. Once the web editor is initialized though, I think unused .olean files won't change the speed at which Lean processes files.

Bryan Gin-ge Chen (Jul 03 2019 at 14:00):

What's the best way of "minifying" a Lean package right now? It would be useful to integrate that functionality into mk_library.py.

Patrick Massot (Jul 03 2019 at 14:00):

What do you mean by minifying?

Bryan Gin-ge Chen (Jul 03 2019 at 14:01):

Removing all lean / olean files which are not imported by those in the src directory.

Patrick Massot (Jul 03 2019 at 14:02):

Oh, that would be nice. I guess you need one of our Rust gurus to ask Mario's olean reader

Bryan Gin-ge Chen (Jul 03 2019 at 14:03):

Perhaps I should say "tree shaking" instead of "minifying".

Mohammad Pedramfar (Jul 03 2019 at 21:35):

Next, I'll need to investigate Mohammad Pedramfar's effort to integrate this with format_lean. I also have one more question: will I get a noticeable speed gain if I use a trimmed down mathlib? Or is it ignoring unneeded files in mathlib anyway?

I started working on it a few days ago. I'll let you know when I get it to work.

Mohammad Pedramfar (Jul 03 2019 at 21:41):

Removing all lean / olean files which are not imported by those in the src directory.

Try adding a line path = "src" into the leanpkg.toml before running mk_library.

Bryan Gin-ge Chen (Jul 03 2019 at 22:20):

Oh, that works. Though you'll have to delete all the other olean files first and then wait for lean to build everything from scratch.

Mohammad Pedramfar (Jul 03 2019 at 22:22):

Yeah, it takes a little time

Bryan Gin-ge Chen (Jul 03 2019 at 23:21):

fix the non-existent dist folder and GitHub url check bugs in mk_library.py

I made an attempt to fix these bugs in the last few commits to my fork of the lean-web-editor, but it's not well-tested yet. I don't have the bandwidth to follow up on the other items at the moment, though.

Patrick Massot (Jul 04 2019 at 13:59):

Oh, that works. Though you'll have to delete all the other olean files first and then wait for lean to build everything from scratch.

What does "that" refers to in this sentence?

Bryan Gin-ge Chen (Jul 04 2019 at 14:01):

Adding the line path = "src" in leanpkg.toml and then putting some Lean files of interest in that directory before running mk_library.

Patrick Massot (Jul 04 2019 at 14:02):

which leanpkg.toml? The one in combined_lib?

Bryan Gin-ge Chen (Jul 04 2019 at 14:02):

Yes.

Bryan Gin-ge Chen (Jul 04 2019 at 14:03):

It relies on the fact that leanpkg build only builds the dependencies of the files in src.

Patrick Massot (Jul 04 2019 at 14:03):

Oooh

Patrick Massot (Jul 04 2019 at 14:03):

I need to try that

Patrick Massot (Jul 04 2019 at 14:05):

But I'm confused. Is mk_library.py running leanpkg build? Or do you mean I should have mathlib in the dependencies of combined_lib as a git repo and run leanpkg build there and then mk_library_build?

Bryan Gin-ge Chen (Jul 04 2019 at 14:06):

mk_library.py runs leanpkg build

Bryan Gin-ge Chen (Jul 04 2019 at 14:07):

And then it blindly copies all .olean files that it can find by looking in the directories provided by lean -p into the ZIP file; that's why I said you have to delete the other olean files.

Patrick Massot (Jul 08 2019 at 16:36):

I can confirm I successfully built a 5.7Mo library instead of 18Mo by removing every olean from mathlib and my small undergraduate lib, and then run mk_library.py -i ~/lean/lib114/ -o dist114/library.zip where lib114 import not much from mathlib

Johan Commelin (Jul 08 2019 at 16:38):

Otoh, this tree-shaking means that users can't import things from mathlib that they suddenly would like to use...

Patrick Massot (Jul 08 2019 at 16:39):

@Bryan Gin-ge Chen I can't open an issue in your fork, so let me continue using this thread. In the README, last item you wrote "Run ./mk_library.py (requires Python 3.5 or greater)" is wrong. Your script requires python 3.7. I discovered that when running it on an old Ubuntu.

Patrick Massot (Jul 08 2019 at 16:40):

From https://docs.python.org/3.7/library/subprocess.html#subprocess.run:

Changed in version 3.7: Added the capture_output parameter.

Patrick Massot (Jul 08 2019 at 16:41):

On Ubuntu 18.04 (the latest LTS), python3 default to 3.6 but there is an official python 3.7. I only needed to use python3.7 mk_library.py

Patrick Massot (Jul 08 2019 at 16:42):

Johan: yes indeed. But in the context of my teaching students don't want to import surprising things from mathlib. Remember we're not talking about Kevin's elite students. None of my 50 students created a Zulip account for instance. That's how curious they are

Patrick Massot (Jul 08 2019 at 16:43):

None of them asked whether there was any lemma they could add to Lean's library (I'm not even talking about knowing the name mathlib)

Bryan Gin-ge Chen (Jul 08 2019 at 17:07):

@Patrick Massot Thanks! I still have yet to make the other changes you suggested...

Patrick Massot (Jul 09 2019 at 12:03):

One more suggestion about the Lean web editor: when clicking the Save button, inspiration for the file name could be taken from the name of the file that was last loaded (either from disk or url).

Patrick Massot (Jul 09 2019 at 12:04):

Maybe also turn "no goal" into "goal accomplished" as in VScode, for consistency

Patrick Massot (Jul 09 2019 at 12:04):

Otherwise the main thing is really getting Tab to autocomplete. Currently it seems only space works, which is really unconvenient

Bryan Gin-ge Chen (Jul 09 2019 at 13:10):

Thanks for the suggestions! The issue with Tab vs Space is indeed at the top of the list but I still haven't figured out a good approach to address it...

Patrick Massot (Jul 09 2019 at 15:53):

One more suggestion that came to me while documenting my use of this tool: in the top status bar, you could replace "Lean is running..." by "Lean is loading..." that is less ambiguous

Kevin Buzzard (Jul 09 2019 at 15:53):

I agree that "Lean is running..." is confusing.

Bryan Gin-ge Chen (Jul 09 2019 at 15:55):

So you would want "Lean is loading..." while it initializes but "Lean is running" afterwards, when it is actually processing the editor contents? That sounds reasonable.

Patrick Massot (Jul 09 2019 at 15:56):

"Lean is ready!" is also fine

Bryan Gin-ge Chen (Jul 09 2019 at 16:05):

Oh, I think I misunderstood the request at first. Would you be happy if the status bar showed either "Lean is ready!" or "Lean is busy..." ?

Patrick Massot (Jul 09 2019 at 16:31):

Yes

Wojciech Nawrocki (Jul 15 2019 at 20:13):

Low priority, but I just tried it on my phone (android 9, chrome and Firefox) and the editor is unusable (backspace doesnt work). Possibly an issue in whatever text editor widget is used

Marc Huisinga (Jul 15 2019 at 20:17):

i doubt that monaco will work properly on mobile any time soon, and it probably doesn't make much sense to move away from it.
it's a pretty damn good web editor and also the backend for vscode.
there's a github issue (https://github.com/Microsoft/monaco-editor/issues/246), but it doesn't look like there's any progress being made.

Bryan Gin-ge Chen (Jul 15 2019 at 20:59):

It's too bad that it doesn't work on Android. I tested it a while back on an iPad and it seemed OK (if rather slow). I tested it just now on my iPhone and while backspace is OK, Safari zooms in way too far when I try to type, making it pretty much unusable.

Re: monaco, I haven't updated the monaco version in my fork so it's probably out of date. Hopefully there aren't any big issues with it...

Marc Huisinga (Jul 15 2019 at 21:06):

the one we used for the wavelength ide has been frozen since early 2018 and it still seems to work fine

Marc Huisinga (Jul 15 2019 at 21:07):

while working through TPIL with the web editor i made a list with weird behavior, but that list seems to be gone now ...

Marc Huisinga (Jul 15 2019 at 21:13):

while opening it right now, just some quick weird things:
- there's no bracket matching overlay for the bracket at the position of the text cursor like in vs-code. i think you can enable it in the settings and configure which brackets to use (might be worth configuring \< \> and such).
- closing brackets are also seemingly not inserted automatically
- when using it while working through TPIL, i think i also had some issue with undo/redo, but i can't reproduce it right now

Bryan Gin-ge Chen (Jul 23 2019 at 05:31):

It took me a while to get to this, but you can now use tab to perform translations to unicode in the community lean-web-editor! @Patrick Massot

I cleaned up some stuff in the meantime, in particular, it should now be much easier to build the web app from scratch with npm, etc. now that I've published my fork of lean-client-js-browser to npm. @Mohammad Pedramfar

Kevin Kappelmann (Jul 25 2019 at 11:49):

It took me a while to get to this, but you can now use tab to perform translations to unicode in the community lean-web-editor! Patrick Massot

I cleaned up some stuff in the meantime, in particular, it should now be much easier to build the web app from scratch with npm, etc. now that I've published my fork of lean-client-js-browser to npm. Mohammad Pedramfar

Is it just me or is the community lean-web-editor not working at the moment?

Johan Commelin (Jul 25 2019 at 11:50):

Works for me

Kevin Kappelmann (Jul 25 2019 at 11:55):

uff, u-block origin was blocking a request to https://tqft.net/ . thanks

Keeley Hoek (Jul 26 2019 at 02:37):

Scott has actually decided to branch out and start an ad delivery network

Last updated: Dec 20 2023 at 11:08 UTC