leanprover / leanprover.github.io Goto Github PK
View Code? Open in Web Editor NEWwww
Home Page: https://lean-lang.org/
www
Home Page: https://lean-lang.org/
Tutorial claims that you can type \to or \nat and have them replaced by the appropriate symbol, but this functionality doesn't seem to be working (in Chrome on ubuntu)
Items:
Tools:
The talks/RacketCon2022.pdf
is missing. There is a dead link under Presentations to it.
@leodemoura reported the followings:
It seems the web font used in the "live" website is not being supported correctly by IE.
It seems we need to use some workarounds for IE
http://stackoverflow.com/questions/15045425/getting-web-fonts-to-work-in-ie10
http://stackoverflow.com/questions/19561414/google-fonts-not-working-in-internet-explorer-ie-11
http://www.thewindowsclub.com/web-fonts-appear-blurry-internet-explorer
It seems to me that the instructions on the download page should tell users that they have to set up emacs, and it should provide guidance for doing that.
I can think of a few options.
(1) We can link to the instructions here:
https://github.com/leanprover/lean/blob/master/src/emacs/README.md
(2) We can make a copy of that file in leanprover.github.io.
(3) We can cut and paste parts of that file into the download instructions on leanprover.github.io.
(4) The download instructions on leanprover.github.io can tell users where to find the README file on their computer, once Lean has been installed.
If you tell me which option you think is best, I will be happy to make these changes. If it is (4), please tell me what directory contains the lean folder after the installations on the various systems.
Also, even though there is a github ribbon in the corner, it wouldn't hurt to mention the github repository as a download option.
https://lean-lang.org/people/
contains a link to
https://lean-fro.org/people/
which should be
https://lean-fro.org/team/
[I don't think the repo for lean-lang.org
is public, so I cannot submit a PR]
Some of the backslash shortcuts aren't producing their expected output in the online editor.
According to the table in Chapter 3.3 of the tutorial:
\iff
and \lr
should produce ↔\not
and \neg
should produce ¬In the first case, \lr
works as expected (as does \<->
and \leftrightarrow
), but \iff
produces ⇔ instead, which results in an unexpected token
error. The cause here seems to be input-method.js#L689.
The second case is weirder: \neg
works correctly (as does \lnot
), but \not
produces U+0338, a sort of "combining slash" character. Looking at input-method.js#L701 though, nothing really seems amiss. 😕
I reviewed the Lean web pages, and I would like to suggest come changes.
(1) The "about" button should come first. When people come to a strange new page, it is reasonable to want to know what is there.
(2) On the "about" page it would be helpful to tell people about the collaborative nature of Lean. I would suggest adding a second paragraph:
"The Lean project was launched by Leonardo de Moura at Microsoft Research in 2013. It is a collaborative open source project, hosted on [github]. Contributions to the code base and library are welcome."
(3) "Publications" can be merged with "Documentation", at the bottom.
Later, we can add information about mailing lists and stackoverflow.
(4) Under Documentation, it would be helpful to let people know what to expect when they click the tutorial buttons. I would make a separate section "Tutorial", with the following entries:
(5) It is disconcerting that users just clicking around get taken to a totally different page with a slow load process when they click "Try Lean". It would be friendlier if the button took them to a page that says something like this:
You can experiment with an [online version of Lean] that runs in your browser.
Actually, I don't know if we need a separate button for this. Instead, we could delete the "Try Lean" and add this line to "About":
You can experiment with an [online version of Lean] that runs in your browser, or use an [online tutorial].
We can all add this same line to the bottom of the Download page.
Thoughts? I would be happy to implement these changes.
I noticed the problem with two characters \and and \forall.
For example, try to input
theorem tst : ∀a b: Prop, a ∧ b → a ∧ b:=
The cursor position is so off that it is not even funny.
I wanted to kick off a discussion about updating the website.
I was talking to Leo about this at work last week but I would like to make a couple concerted changes to our web presence.
First I think we should improve our exposure online in general, we have built impressive, state-of-the-art infrastructure but haven't done much to publicize this to others. There are many under-documented features that even current users are unaware of.
Update the landing page of the website to bring it more inline with
other programming languages.
* We should provide clear examples of how to use Lean for proving, programming, etc
* Demonstrate what programs written in Lean look like, and sign post to downloads,
documentation, and primary chat platforms. See examples such as
https://www.python.org/, https://www.ruby-lang.org/en/, https://www.haskell.org/,
and https://www.rust-lang.org/en-US/.
Start a Lean technical blog which we update at semi-regular intervals. The posts need
not be long, ideally we could try for brief posts that act as sign posts for new features, or
developments. For example we could write one for new algebra decision procedures,
the new IO subsystem, the state of the native compiler, how to implement something like
super or the z3 tactic, how interactive parsers work, the new structure command, and so
on. I think even if we just spent a small amount of time synthesizing all of our current chats,
issues, and personal thoughts it would be awesome, also see Roadmap.
At a high level I want to revisit and clarify where communication happens.
I think the current private Slack is a great for internal development chatter, and priorities.
We should discuss updating or clarifying external communication mediums, right now
all kinds of communication (bug reports, language design, help, Q&A) occur via email, Slack, Google Groups, and issues.
Having clearer distinctions about where each type of communication happens, will help us as we continue to acquire new users.
For example if we want to try Gitter out we should make a concerted effort to channel Lean users there. This allows us to form policies around new user problems, such as false bug reports, which we can easily close and direct users to the correct forum. Another example is possibly using Discourse over Google Groups.
We also have quite a few expert users who are not on Slack, and I think it would be good to create a single public (and easily joinable) place for new users to seek help, where both the development team and expert users will be.
My final proposal is a Roadmap for the project as a whole. Currently there are multiple large changes happening each week to Lean, and we should provide a way for users and the development team to sync on the status of various initiatives. This is also a boon to users, new and old, right now we just tell people that a feature is "coming" at some point in the future, but we spend a lot of time and energy communicating the priorities, and that "yes, that feature is planned".
We could just compile a link of RFCs and supporting issues for example, or do something more complicated. I think part of this is ensuring that we publish release notes on each release.
Thoughts would be much appreciated.
When I try to process Jakob's file on the web, I get the following error message:
-- Processing file ...
Cannot enlarge memory arrays. Either (1) compile with -s TOTAL_MEMORY=X with X higher than the current value 16777216, (2) compile with ALLOW_MEMORY_GROWTH which adjusts the size at runtime but prevents some optimizations, or (3) set Module.TOTAL_MEMORY before the program runs.
-- Saved to 'Dropbox/Apps/Lean.JS/input.lean'.
Here is his file
import hott.path
open path function
-- Equivalences
-- ------------
definition Sect {A B : Type} (s : A → B) (r : B → A) := Πx : A, r (s x) ≈ x
-- -- TODO: need better means of declaring structures
-- -- TODO: note that Coq allows projections to be declared to be coercions on the fly
-- Structure IsEquiv
inductive IsEquiv [class] {A B : Type} (f : A → B) :=
IsEquiv_mk : Π
(inv : B → A)
(retr : Sect inv f)
(sect : Sect f inv)
(adj : Πx, retr (f x) ≈ ap f (sect x)),
IsEquiv f
namespace IsEquiv
definition inv {A B : Type} {f : A → B} (H : IsEquiv f) : B → A :=
IsEquiv.rec (λinv retr sect adj, inv) H
-- TODO: note: does not type check without giving the type
definition retr {A B : Type} {f : A → B} (H : IsEquiv f) : Sect (inv H) f :=
IsEquiv.rec (λinv retr sect adj, retr) H
definition sect {A B : Type} {f : A → B} (H : IsEquiv f) : Sect f (inv H) :=
IsEquiv.rec (λinv retr sect adj, sect) H
definition adj {A B : Type} {f : A → B} (H : IsEquiv f) :
Πx, retr H (f x) ≈ ap f (sect H x) :=
IsEquiv.rec (λinv retr sect adj, adj) H
end IsEquiv
-- Structure Equiv
inductive Equiv (A B : Type) : Type :=
Equiv_mk : Π
(equiv_fun : A → B)
(equiv_isequiv : IsEquiv equiv_fun),
Equiv A B
namespace Equiv
definition equiv_fun [coercion] {A B : Type} (e : Equiv A B) : A → B :=
Equiv.rec (λequiv_fun equiv_isequiv, equiv_fun) e
definition equiv_isequiv [coercion] {A B : Type} (e : Equiv A B) : IsEquiv (equiv_fun e) :=
Equiv.rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
infix `≃`:25 := Equiv
notation e `⁻¹` := IsEquiv.inv e
end Equiv
-- Some instances and closure properties of equivalences
namespace IsEquiv
variables {A B C : Type} {f : A → B} {g : B → C} {f' : A → B}
-- The identity function is an equivalence.
definition idIsEquiv [instance] : (@IsEquiv A A id) := IsEquiv_mk id (λa, idp) (λa, idp) (λa, idp)
-- The composition of two equivalences is, again, an equivalence.
definition comp_closed [instance] (Hf : IsEquiv f) (Hg : IsEquiv g) : (IsEquiv (g ∘ f)) :=
IsEquiv_mk ((inv Hf) ∘ (inv Hg))
(λc, ap g (retr Hf ((inv Hg) c)) @ retr Hg c)
(λa, ap (inv Hf) (sect Hg (f a)) @ sect Hf a)
(λa, (whiskerL _ (adj Hg (f a))) @
(ap_pp g _ _)^ @
ap02 g (concat_A1p (retr Hf) (sect Hg (f a))^ @
(ap_compose (inv Hf) f _ @@ adj Hf a) @
(ap_pp f _ _)^
) @
(ap_compose f g _)^
)
-- Any function equal to an equivalence is an equivlance as well.
definition path_closed (Hf : IsEquiv f) (Heq : f ≈ f') : (IsEquiv f') :=
path.induction_on Heq Hf
-- Any function pointwise equal to an equivalence is an equivalence as well.
definition sim_closed (Hf : IsEquiv f) (Heq : f ∼ f') : (IsEquiv f') :=
let sect' := (λ b, (Heq (inv Hf b))^ @ retr Hf b) in
let retr' := (λ a, (ap (inv Hf) (Heq a))^ @ sect Hf a) in
let adj' := (λ (a : A),
let ff'a := Heq a in
let invf := inv Hf in
let secta := sect Hf a in
let retrfa := retr Hf (f a) in
let retrf'a := retr Hf (f' a) in
have eq1 : ap f secta @ ff'a ≈ ap f (ap invf ff'a) @ retr Hf (f' a),
from calc ap f secta @ ff'a
≈ retrfa @ ff'a : (ap _ (adj Hf _ ))^
... ≈ ap (λb, f (invf b)) ff'a @ retrf'a : (!concat_A1p)^
... ≈ ap f (ap invf ff'a) @ retr Hf (f' a) : {ap_compose invf f ff'a},
have eq2 : retrf'a ≈ Heq (invf (f' a)) @ ((ap f' (ap invf ff'a))^ @ ap f' secta),
from calc retrf'a
≈ (ap f (ap invf ff'a))^ @ (ap f secta @ ff'a) :(moveL_Vp _ _ _ (eq1^))
... ≈ ap f (ap invf ff'a)^ @ (ap f secta @ Heq a) : {ap_V invf ff'a}
... ≈ ap f (ap invf ff'a)^ @ (Heq (invf (f a)) @ ap f' secta) : {!concat_Ap}
... ≈ ap f (ap invf ff'a)^ @ Heq (invf (f a)) @ ap f' secta : {!concat_pp_p^}
... ≈ ap f ((ap invf ff'a)^) @ Heq (invf (f a)) @ ap f' secta : {!ap_V^}
... ≈ Heq (invf (f' a)) @ ap f' ((ap invf ff'a)^) @ ap f' secta : {!concat_Ap}
... ≈ Heq (invf (f' a)) @ (ap f' (ap invf ff'a))^ @ ap f' secta : {!ap_V}
... ≈ Heq (invf (f' a)) @ ((ap f' (ap invf ff'a))^ @ ap f' secta) : !concat_pp_p,
have eq3 : (Heq (invf (f' a)))^ @ retr Hf (f' a) ≈ ap f' ((ap invf ff'a)^ @ secta),
from calc (Heq (invf (f' a)))^ @ retr Hf (f' a)
≈ (ap f' (ap invf ff'a))^ @ ap f' secta : moveR_Vp _ _ _ eq2
... ≈ (ap f' ((ap invf ff'a)^)) @ ap f' secta : {!ap_V^}
... ≈ ap f' ((ap invf ff'a)^ @ secta) : (!ap_pp)^,
eq3) in
IsEquiv_mk (inv Hf) sect' retr' adj'
--TODO: Maybe wait until rewrite rules are available.
theorem inv_closed (Hf : IsEquiv f) : (IsEquiv (inv Hf)) :=
IsEquiv_mk sorry sorry sorry sorry
end IsEquiv
namespace Equiv
variables {A B C : Type} (eqf : A ≃ B)
theorem id : A ≃ A := Equiv_mk id IsEquiv.idIsEquiv
theorem compose (eqg: B ≃ C) : A ≃ C :=
Equiv_mk ((equiv_fun eqg) ∘ (equiv_fun eqf))
(IsEquiv.comp_closed (equiv_isequiv eqf) (equiv_isequiv eqg))
check IsEquiv.path_closed
theorem path_closed (f' : A → B) (Heq : equiv_fun eqf ≈ f') : A ≃ B :=
Equiv_mk f' (IsEquiv.path_closed (equiv_isequiv eqf) Heq)
theorem inv_closed : B ≃ A :=
Equiv_mk (IsEquiv.inv (equiv_isequiv eqf)) (IsEquiv.inv_closed (equiv_isequiv eqf))
end Equiv
Yesterday I had a problem with the unicode fonts, and I fixed it following the instructions in the Emacs mode README file. (I installed emacs-unicode-fonts.) But to do this I had to (1) remember that Soonho once told us about this, and (2) look for the README. Users with the same problem may be more frustrated.
Two possible solutions:
(1) On leanprover.github.io, add a more prominent link to the Emacs README file, under "Download". For example, at the bottom of the page, we can write:
Once Lean is installed, you can start the Emacs with Lean mode using the command leanemacs
. For information on how to configure Emacs yourself and install unicode-friendly fonts, see [here].
(2) On the Documentation page, we can start a FAQ. This could go in a "troubleshooting" section. We could do this, for example, by changing the header "Forum" to "Additional Information", with entries:
o You are welcome to join the [Lean user forum] on Google Groups.
o There is also a list of [Frequently Asked Questions].
@leodemoura @soonhokong ? I will be happy to make either or both of these changes. (I am not sure how to set up a new page for the FAQ, but I can probably figure it out.)
How to contribute a Chinese translation for homepage? By the way, we are translating Functional Programming in Lean and Theorem Proving in Lean. Should I merge it into the official repo?
On the "Documentation" page, the last two lines are in a slightly larger font on my browser. On the "People" page, the items are slightly smaller than the list headers.
Examples:
TODOs:
Hi.
The file "Are We Fast Yet" from LT2024 is a malformed PDF 607 byte in length.
In the past, we could use shortcuts such as \to
, \nat
and \fun
in the Lean web version.
It doesn't seem to work anymore. I tried in different browsers on Windows and Linux.
It doesn't work in any of them.
@soonhokong Do you have any idea why it doesn't work anymore?
@avigad Does it work for you?
Thanks.
For the first time, you need to run:
sudo apt-get install python-software-properties # to use add-apt-repository
sudo add-apt-repository ppa:leanprover/lean
sudo apt-get update
sudo apt-get install lean
To get the latest version, please run:
sudo apt-get update
sudo apt-get install --only-upgrade lean # to make sure
it only upgrade lean. In general, you can do "apt-get upgrade"
Note: This PPA1 has an outdated version (2014.11.20). We need to set
up a server running ppa-updater2
For the first time, you need to run (I assume that you're using homebrew):
brew tap leanprover/lean # tap our repository
https://github.com/leanprover/homebrew-lean
brew install lean
To get the latest version, please run:
brew update
brew upgrade lean
Note: I've set up two machines running OSX-10.9 and OSX-10.10 to
provide precompiled binaries of Lean for both version of OSX. The
latest binary is available at
https://github.com/leanprover/homebrew-lean/tree/gh-pages
On Windows 7 (I will try Windows 8 later), the cursor position is completely off on the "Try Lean" page.
See the position of the cursor in the following snapshot:
Now suppose we type "12345". Here is the result
The problem happens when I use Chrome or Firefox.
The weird thing is that the tutorial page is fine. The ACE editor seems to use a different font in the tutorial page. See the following snapshop:
The problem does not happen on Linux + Chrome.
Possibly having a reminder in the installation instructions to add /*/lean4/build/release/stage1/bin to your path in your .bashrc could be helpful.
The new version of the tutorial includes type information on mouse hover. This is a great feature, but there is a bug, which manifests itself when one resizes the horizontal pane bar:
The issue is that the mouse hover information isn't available in the new position of the proof term, instead, it is available at a shifted location, at the original position of the term before pane resize.
The issue is present on all 3 browsers I've tested:
Under the "Editor Support" section, it's pointing to https://github.com/leanprover/lean4/tree/master/lean4-mode, which gives 404. I think the new link is now https://github.com/leanprover/lean4-mode
In the documentation page, subsection Lean 2
, I think first paragraph The previous version of Lean ...
should change to This previous version of Lean ...
to be clearer.
Somebody skimming over the page (like me) could think The
refers to Lean in the previous section, and Lean 2
is an upcoming version (without realizing that Lean 3
is current),
The most recent redeployment of the lean-lang.org
site (pages build and deployment #62) seems to have broken all site links to GitHub Pages deployments by other leanprover
organization projects.
These include (organized by the lean-lang.org
site page they are present on):
/documentation
:
/download
:
As of this morning (prior the most recent deployment), the above links were working as expected on the lean-lang.org
site.
It looks like these all used to be absolute links to the https://leanprover.github.io/
domain, but were rewritten within the past month to be relative paths for lean-lang.org
. Each of these URL paths are still up and functional relative to the https://leanprover.github.io/
domain.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.