Online Lean editor

Stream: general

[Mohammad Pedramfar]

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 ?

[Bryan Gin-ge Chen]

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

[Mohammad Pedramfar]

Yeah, I did.

[Kevin Buzzard]

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

[Gabriel Ebner]

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?

[Mohammad Pedramfar]

Yeah, I used lean 3.4.1 for both

[Mohammad Pedramfar]

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

[Chris Hughes]

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

[Mohammad Pedramfar]

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.

[Mohammad Pedramfar]

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

[Mohammad Pedramfar]

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.