lean browser with large buffer

Stream: general

[Thorsten Altenkirch]

I am using lean (actually still lean 3, sorry) for teaching and discovered that one can just cut and paste the lean editor buffer as a link and the content will show up (stored in the URL). However, since the maximal length of URL arguments is limited it seems this works only for small buffers. Hence my question: is there a way to load a file from a different url into the buffer?

[Alex J. Best]

Yes there is an option at the top "Load .lean from URL" (or from disk) if you are on https://leanprover-community.github.io/lean-web-editor/

[Thorsten Altenkirch]

Thank you, that should work the students only would have to press Load buffer but now I notice that I cannot load from the exercise files on moodle. I can open them with the browser but can't load them into lean. :unamused:

[Eric Wieser]

Does the browser console have anything to say?

[Eric Wieser]

I would guess that this is either a CORS security "feature" of moodle, or that there's some content-type problem