Zulip Chat Archive

Stream: general

Topic: Online Lean editor


view this post on Zulip Mohammad Pedramfar (Apr 12 2019 at 15:19):

I'm playing around with the online lean editor. I tried to replace the "library.zip" with this file. olean_files.7z (I compressed it since zulip wouldn't allow me to upload a large file). After replacing the "library.zip", I can import the files in mathlib. But when I try to import "xenalib.M1P1", it says "file '/library/xenalib/M1P1.lean' not found". The auto complete realises that this file exists when I'm trying to write the import, but it can't import it. I can't figure out what is going on. Is there something I'm missing ?

view this post on Zulip Bryan Gin-ge Chen (Apr 12 2019 at 15:24):

Did you follow the instructions here (namely, first changing the leanpkg.toml and then running mk_library.py)?

view this post on Zulip Mohammad Pedramfar (Apr 12 2019 at 16:19):

Yeah, I did.

view this post on Zulip Kevin Buzzard (Apr 12 2019 at 18:20):

I remember trying to get all this working a year or so ago and having real trouble. @Gabriel Ebner I've seen Mohammad's web editor in action -- he can import mathlib files but not files from my repo even though they are offered as an autocompletion option. It looks just like what happens in VS Code if you have an olean file but no corresponding lean file, but in this setup mathlib seems to work with only the olean files

view this post on Zulip Gabriel Ebner (Apr 12 2019 at 19:09):

I don't see any obvious problems in library.zip. Did you use the same Lean version to compile the olean files that the web editor uses?

view this post on Zulip Mohammad Pedramfar (Apr 12 2019 at 19:25):

Yeah, I used lean 3.4.1 for both

view this post on Zulip Mohammad Pedramfar (Apr 12 2019 at 19:27):

I remember trying to get all this working a year or so ago and having real trouble. Gabriel Ebner I've seen Mohammad's web editor in action -- he can import mathlib files but not files from my repo even though they are offered as an autocompletion option. It looks just like what happens in VS Code if you have an olean file but no corresponding lean file, but in this setup mathlib seems to work with only the olean files

This idea worked ! If I take olean files from mathlib and lean files for the rest, then everything works ! The problem is that it's slow. There should be a way to make it open the olean files

view this post on Zulip Chris Hughes (Apr 12 2019 at 19:29):

3.4.1 is old. Does the xenalib work with old Lean?

view this post on Zulip Mohammad Pedramfar (Apr 12 2019 at 19:32):

It's not a new version of xenalib, it only has a few files in it. And it runs with lean 3.4.1 in vs code.

view this post on Zulip Mohammad Pedramfar (Apr 12 2019 at 19:33):

And if I replace olean xenalib files with lean files, the online editor works as well. It's slow, but it works.

view this post on Zulip Mohammad Pedramfar (Apr 12 2019 at 19:44):

Oh ! my bad ! It does work. Some python code from somewhere was compiling it using 3.4.2. I compiled it again with 3.4.1 and it worked.


Last updated: May 16 2021 at 05:21 UTC