feature request: import package

leanprover-community / lean4web

The Lean 4 web editor

https://live.lean-lang.org/

Apache License 2.0

52 stars 14 forks source link

feature request: import package #22

Closed Seasawher closed 2 months ago

Seasawher commented 2 months ago

Current situation

Packages other than mathlib cannot be used.
To add more packages that can be used with lean4 web, changes need to be made to the lean4 web code

I want a feature such that...

Import packages in-place on the lean4 web based on GitHub repository URLs.

joneugster commented 2 months ago

It is possible for the admin of a server to provide featured packages (for example here we provide the "Duper Demo" lean package). And one can switch in the settings between the finite amount of admin-chosen projects.

However, with the current setup ("everything runs server-side"), I don't think it's feasible to allow users to essentially upload to the server and have them built on the server.

However, what would be the advantage over gitpod?

Seasawher commented 2 months ago

Certainly GitPod and Codespace seem sufficient. Thanks.

Seasawher commented 2 months ago

I raise this issue because it is possible to create interactive books by linking the lean4 web editor to mdbook.

see https://github.com/Seasawher/lean-book

However, it may seem strange to demand that much from a lean4 web editor.