• change the color used for keywords. avoid red
• subatomic mode?

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:

• Main Page (Introduction)
• Link to Tutorial
• Link to Live Demo
• Source (github)
• Download / Installation
• People
• Publications & Presentations
• Blog

Tools:

• http://khan.github.io/KaTeX/
• http://getbootstrap.com/
• http://jekyllrb.com/

I think it is easier to explain by showing the resultant page:

The talks/RacketCon2022.pdf is missing. There is a dead link under Presentations to it.

@leodemoura reported the followings:

• The input method only worked for “\fun” and “\eq”. Everything else I tried did not work: “\Pi”, “\r”, “\tr”, “\sy”, “\x”, “\forall”.
  My conjecture is: if auto-completion is activated, then the input method does not work. For example, when I type “\f” the auto-completion is already suggesting “forall”, and it seems to block the input method.
• The auto-completion gets “confused” with hierarchical names. If I type “eq.sy”, it will show “eq.symm” as a possible candidate. However, if I select it, the text becomes “eq.eq.symm” instead of “eq.symm”.

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:

• There is an [online tutorial], which is presented alongside a version of Lean running in your browser.
• You can also read the [pdf version].

(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.

url in _config.yml is using http which causes the requests to main.css, main.js, etc to be blocked when accessed via https.

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.

Landing Page Update

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/.

Lean Technical Blog

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.

Communication mediums

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.

Roadmap

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.

• run loaded text automatically

• The site http://www.tryfsharp.org/ has nice ideas.
• http://rightjs.org/ui/resizable

Examples:

• https://github.com/leanprover/lean/blob/master/library/logic/examples/nuprl_examples.lean#L22-L29
• https://github.com/leanprover/lean/blob/master/library/logic/examples/nuprl_examples.lean#L22
• https://gist.github.com/soonhokong/d57051ec2a929c05833b#file-small_exercises-lean-L27-L30

TODOs:

• Highlight selected lines
• Scroll to the first highlighted line.

reference: http://superuser.com/questions/434630/customizing-how-html-is-generated-for-source-code-blogs-when-using-export-in-org

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.

Ubuntu

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

OSX

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:

1. Opera
2. Firefox
3. Chrome

• http://msdn.microsoft.com/en-us/library/jj680723.aspx
• http://isdk.dev.live.com/dev/isdk/ISDK.aspx?category=scenarioGroup_skyDrive&index=0

We can deal with this after POPL, just something I didn't want to forget.

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),

https://github.com/kloudless/file-explorer

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:
  • https://lean-lang.org/theorem_proving_in_lean4/
  • https://lean-lang.org/lean4/doc/
  • https://lean-lang.org/functional_programming_in_lean/
• /download:
  • https://lean-lang.org/lean4/doc/quickstart.html

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.