Skip to content

Commit d7e4633

Browse files
authored
Update README.md
1 parent f2f3530 commit d7e4633

File tree

1 file changed

+11
-2
lines changed

1 file changed

+11
-2
lines changed

README.md

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,15 +4,24 @@
44

55
# Lean 4 Web
66

7-
This is a web version of Lean 4. The official lean playground is hosted at [live.lean-lang.org](https://live.lean-lang.org), while [lean.math.hhu.de](https://lean.math.hhu.de) hosts a development server testing newer features.
7+
This is a web version of Lean 4. There is a playground hosted at [live.lean-lang.org](https://live.lean-lang.org) and one at [lean.math.hhu.de](https://lean.math.hhu.de).
88

99
In contrast to the [Lean 3 web editor](https://github.com/leanprover-community/lean-web-editor), in this web editor, the Lean server is
1010
running on a web server, and not in the browser.
1111

12+
## Scope of lean4web
13+
14+
The main scope of `lean4web` is to provide an easy way to run [MWEs](https://leanprover-community.github.io/mwe.html) from [Zulip](https://leanprover.zulipchat.com) with the latest [Mathlib](https://github.com/leanprover-community/mathlib4) installed.
15+
16+
While `lean4web` looks very similar to VSCode with the [Lean4 extension](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4) installed - and it reuses much of that code - there is currently no official support by the [Lean FRO](https://lean-fro.org) and therefore `lean4web` does not claim to be feature complete.
17+
1218
## Contribution
1319

1420
If you experience any problems, or have feature requests, please open an issue here!
15-
PRs are welcome as well.
21+
22+
PRs fixing issues are very welcome!
23+
24+
For new features, it's best to write an issue first to discuss them: For example, some functionality might be better implemented in [lean4monaco](https://github.com/hhu-adam/lean4monaco) which provides the key features and a discussion might be helpful to figure this out.
1625

1726
## Documentation
1827

0 commit comments

Comments
 (0)