importing files from github in Lean 4 Web?

Stream: Is there code for X?

[Isabelle Dubois]

Is it possible to import files (or even folders) from a github deposit (or an html address) into Lean 4 Web? (with a command)

[Floris van Doorn]

It's not, unless you set up your own instance of the server.

[Aaron Liu]

There's the "Load File from Disk", "Load File from URL", and "Load File from Zulip" options on the top right corner, if that's what you want.

[Aaron Liu]

You can only have one file though.

[Christian K]

I forked the lean4 web server a while ago and created a file picker that could be used to open files in a github repo (but this was quite hacky and it is not online anymore).

[Isabelle Dubois]

Floris van Doorn said:

It's not, unless you set up your own instance of the server.

Ok, thanks.

[Isabelle Dubois]

Aaron Liu said:

There's the "Load File from Disk", "Load File from URL", and "Load File from Zulip" options on the top right corner, if that's what you want.

I wasn't precise enough: it's not what I wanted. I knew this option, but i wanted to be able to import many files, and if possible with a kind of "import" command.

[Isabelle Dubois]

Christian K said:

I forked the lean4 web server a while ago and created a file picker that could be used to open files in a github repo (but this was quite hacky and it is not online anymore).

Interesting indeed. Thanks for the answer!