In chapter 4, the following proposition is provided as exercise:

  example : (∃x : A, r) ↔ r := sorry

But, because there are no hypothesis assuming A is non-empty, I think this exercise cannot be shown.

For example, http://leanprover.net/tutorial/08_Building_Theories_and_Proofs.html has a link to "Section 1.4" which should be "Section 8.4".

I wish this is because of using old version of lean (we're using apt-get version in travis, and it's built 23 hours ago now).

ERROR executing 09_Using_Tactics.org.10.lean, for in_code_block block starting at 175, produced output:
09_Using_Tactics.org.10.lean:3:0: warning: imported file uses 'sorry'
09_Using_Tactics.org.10.lean:8:20: error: (small) natural number expected

https://travis-ci.org/leanprover/tutorial/jobs/49797191

The auto-reload feature in firefox only works for local files.
This is problematic since we need to use

python -m SimpleHTTPServer

to correctly visualize the pages.
I don't bother pressing refresh to see the effect of my changes, but we should probably remove the auto-reload feature from the README.md file.

Reference:

• HTML Export: https://github.com/yyr/org-mode/blob/master/contrib/lisp/ox-bibtex.el
• PDF Export: http://tex.stackexchange.com/questions/114864/how-to-get-bibtex-to-work-with-org-mode-latex-export

@avigad wrote in an email:

If you go to page 90 of the tutorial,

  https://leanprover.github.io/tutorial/tutorial.pdf

you will see a reference to "Section Automatically Generated Constructions". 

I am pretty sure that in the past this was rendered as "Section 6.8".

For example, in Sections 4.2 and 6.2.

(Another issue is that we should be more consistent about using "nat" or "IN". At some point, I'll change them to the blackboard bold N.)

It's implemented, but it doesn't work well when the document is long.

latest version of google closure-compiler: http://dl.google.com/closure-compiler/compiler-latest.zip

usage:

java -jar compiler.jar --js hello.js --js_output_file hello-compiled.js

@awodey reported via @avigad.

I believe that this is due to 3453d60. I'll fix it soon.

@avigad requested this feature:

"an environment for exercises that would have some distinctive typesetting (on the web page, and in the book)"

+#BEGIN_EXERCISE

+#END_EXERCISE

For example, subscript n is rendered correctly only if a system has GNU Unifont (or other fonts which have a glyph for subscript n). Please see the following screenshot:

One possible solution is to provide a webfont for GNU Unifont.

Related issue: #32

use http://yui.github.io/yuicompressor/

BTW, they are fine in the HTML version.

Both characters are used in Section 10.2

I tried this method with the first two links in Section 5.6, Notations, Overloads, and Coercions:

http://orgmode.org/manual/Links-in-HTML-export.html#Links-in-HTML-export
http://stackoverflow.com/questions/14217908/org-mode-export-to-html-links-open-in-new-tabs

It doesn't seem to work.

There is an example of a cross-chapter link in Section 8.1.

The following solution doesn't seem to work:

http://stackoverflow.com/questions/4577709/emacs-org-mode-org-to-html-conversion-linking-to-section-in-a-different-page

sometimes the whole tutorial page is scrolled up slightly so that users can only see the bottom half of the top menu bar.

https://github.com/leanprover/tutorial/blob/03bfe1cb4733906a1ee15658213fd8295aecdf01/02_Dependent_Type_Theory.org#simple-type-theory

"the type of g is nat → (nat → nat). Thus we can view g as a function that takes natural numbers and returns a natural number."

should be something like "...and returns another function that takes a natural number and returns a natural number."

Ed suggested this in his comments.

e.g. the first example in Section 1.4.

From Bas Spitters: "A tiny suggestion on the web interface. Not all the symbols are completely self-explanatory. Perhaps you can add a description on mouse over."

On my PDF reader (Okular), "properties" says that the PDF tutorial is 6 by 9 inches. And when I print out a page, it is typeset in the upper right corner with about three inch margins on the left and bottom, and the topmost and rightmost part of the page are cut off.

I'm listing several bugs here, but they all have the same root cause and fix, related to how internal links are handled.

Bug 1: from https://leanprover.github.io/tutorial/index.html, I click the drop-down list and select "02 Dependent Type Theory". The URL address does not meaningfully change; if I send the address to someone and they open it, it brings them to chapter 1.

Expected behaviour: if I am on the chapter 2 page, the URL should be a permalink to chapter 2.

Bug 2: if I go further down this page, there is a link to the chapter on type classes. Cmd-click (OS X) creates a new tab with the chapter in question, but the current page also moves to the type classes chapter.

Expected behaviour: Cmd-click should have the same effect as right-click -> open in new tab.

Note: this is probably reproducible on Windows with Ctrl-click.

Bug 3: after opening one internal link, all other internal links appear purple, as if visited.

Expected behaviour: only links to chapters which I've actually visited should appear purple.

Related issue: #32

Example: https://travis-ci.org/leanprover/tutorial/jobs/48388232

From https://leanprover.github.io/tutorial/index.html, clicking the Dropbox button sends me to a page with the following text:

Error (400)
It seems the app you were using submitted a bad request. If you would like to report this error to the app's developer, include the information below.

More details for developers

Invalid redirect_uri: "https://leanprover.github.io/tutorial/index.html". It must exactly match one of the redirect URIs you've pre-configured for your app (including the path)

https://github.com/ded/script.js

need to use 'freemono-lean' in <pre>

Dear @avigad,

My friend @pondering sent me an email reporting an issue in the code example in chapter 2 (2.7 Implicit Arguments).

#+BEGIN_SRC lean
namespace hide
constant list : Type → Type

namespace list
  constant cons : ΠA : Type, A → list A → list A
  constant nil : ΠA : Type, list A
  constant append : ΠA : Type, list A → list A → list A
end list

-- BEGIN
open list

constant  A : Type
constant  a : A
constants l1 l2 : list A

check cons A a (nil A)
check append A (cons A a (nil A)) l1
check append A (append A (cons A a (nil A)) l1) l2
-- END
end hide
#+END_SRC

The last three checks generate errors. Could you take a look at and fix it?

@leodemoura, I remember that you mentioned a way to automatically check all the code in .org files. Could you elaborate it more? I'll integrate it in .travis.yml file so that we will get email notifications for any errors in the tutorial.

#29 (comment)
#29 (comment)
#29 (comment)

The size of lean.js is 6MB and we need to find a way to cache it. Certainly, there is a way to do this:

• https://developers.google.com/speed/docs/insights/LeverageBrowserCaching
• http://www.feedthebot.com/pagespeed/leverage-browser-caching.html
• http://stackoverflow.com/questions/6311694/browser-caching-javascript-and-css-files

However, github pages do not allow us to use .htaccess file to enable browser cache. One alternative is to host lean.js on a server where we have a full-control (i.e. CMU server, MSR server, digital ocean..).

Better solution is to use CDNJS (or any alternative). I just open http://cdnjs.cloudflare.com/ajax/libs/6px/1.0.1/6px.min.js to test it. Then, I checked its cache status via chrome://view-http-cache:

HTTP/1.1 200 OK
Date: Sun, 02 Nov 2014 22:59:37 GMT
Content-Type: application/javascript
Last-Modified: Mon, 08 Sep 2014 07:45:18 GMT
Expires: Fri, 23 Oct 2015 22:59:37 GMT
Cache-Control: public, max-age=30672000
Access-Control-Allow-Origin: *
CF-Cache-Status: MISS
Vary: Accept-Encoding
Server: cloudflare-nginx
CF-RAY: 1833f18de189077f-EWR
Content-Encoding: gzip

The line Expires: Fri, 23 Oct 2015 22:59:37 GMT means that the cached content can be used for a year. Of course, we need to make sure that it picks up the modified contents when we push new lean.js to the CDNJS.

2.3 Function Abstraction and Evaluation

Conversely, if we have p : nat × nat, then we have pr1 p : nat and pr2 : nat.

The last bit:

pr2 : nat

Should be

pr2 p : nat

2.5 Local definitions [0]

The expression let a := t1 in t2 is definitionally equal to the result of replacing every occurrence of a in t1 by t2.

The last bit:

a in t1 by t2

Should be

a in t2 by t1

2.5 Local definitions [1]

Notice that the meaning of the expression let a := t1 in t2 is very similar to the meaning of (λa, t1) t2, but the two are not the same. In the first expression, you should think of every instance of a in t2 as a syntactic abbreviation for t1. In the second expression, a is a variable, and the expression λa, t1 has to make sense independent of the value of a. The let construct is a stronger means of abbreviation, and there are expressions of the form let a := t1 in t2 that cannot be expressed as (λa, t1) t2.

Shouldn't all the occurrences of (λa, t1) t2 actually be (λa, t2) t1 - as we are saying that a should represent an abbreviation for t1 within t2. Which is how let a := t1 in t2 reads.

6.2 Constructors with Arguments

Describes example definitions for pr1 and pr2:

definition pr1 {A B : Type} (p : A × B) : A :=
prod.rec_on p (λa b, a)

definition pr2 {A B : Type} (p : A × B) : A :=
prod.rec_on p (λa b, a)

The definition for pr2 is just a copy of pr1. I believe the example is supposed to be:

definition pr1 {A B : Type} (p : A × B) : A :=
prod.rec_on p (λa b, a)

definition pr2 {A B : Type} (p : A × B) : B :=
prod.rec_on p (λa b, b)

6.4 Defining the Natural Numbers

Consider, for example, the addition function add m n on the natural numbers. Fixing m, we can define addition by recursion on n. In the base case, we set add m zero to n. In the successor step, assuming the value add m n is already determined, we define add m (succ n) to be succ (add m n).

Where it says:

set add m zero to n

Should be:

set add m zero to m

7.5 Inaccessible Terms

In the following example can be find in [1].

I think this is supposed to say something like:

The following example can be found in [1].

@avigad, there is a test failure.

https://travis-ci.org/leanprover/tutorial/jobs/48726614

Code:

section
  variable {A : Type}
  variable x : A
  definition id := x
end

check id
check id a  // <-- fail
check id b  // <-- fail

Message:

ERROR executing 02_Dependent_Type_Theory.org.37.lean, for in_code_block block starting at 1049, produced output:
02_Dependent_Type_Theory.org.37.lean:2:0: warning: imported file uses 'sorry'
id : ?A → ?A
02_Dependent_Type_Theory.org.37.lean:9:9: error: unknown identifier 'a'
02_Dependent_Type_Theory.org.37.lean:10:9: error: unknown identifier 'b'
make: *** [test] Error 1

Prof. Klaus Sutner mentioned about this in the class. Actually current binding of executing code, C-x, is bad because it should do cut. I'm thinking about shift-enter or something with enter.

Dear @leodemoura and @avigad ,

As you may notice, we have a test failure in chapter 5 of the tutorial. Here is the log:

-- testing 05_Interacting_with_Lean.org
code fragment #1 worked
code fragment #2 worked
code fragment #3 worked
code fragment #4 worked
code fragment #5 worked
code fragment #6 worked
code fragment #7 worked
code fragment #8 worked
code fragment #9 worked
code fragment #10 worked
code fragment #11 worked
code fragment #12 worked
ERROR executing 05_Interacting_with_Lean.org.13.lean, for in_code_block block starting at 515, produced output:
05_Interacting_with_Lean.org.13.lean:3:0: warning: imported file uses 'sorry'
05_Interacting_with_Lean.org.13.lean:6:10: error: invalid notation declaration, symbol expected
05_Interacting_with_Lean.org.13.lean:6:15: error: invalid local/reserve notation, 'infix', 'infixl', 'infixr', 'prefix', 'postfix' or 'notation' expected
05_Interacting_with_Lean.org.13.lean:7:7: error: invalid notation declaration, ':=' expected
05_Interacting_with_Lean.org.13.lean:7:12: error: invalid local/reserve notation, 'infix', 'infixl', 'infixr', 'prefix', 'postfix' or 'notation' expected

You can also find this failure at travis-ci: https://travis-ci.org/leanprover/tutorial/jobs/48438890#L3664-L3683

Note that we're using lean-0.2.0.20150126211556.git2a5658ebe28ad3f7b3be13fdac6213a1a4cf000d~12.04 which is the latest version (leanprover/lean3@2a5658e) as I write this issue.

You should define what it is. It is somewhat exotic (for beginners).

Tom Ball reported the following issue:

The default size of fonts makes the ‘e’ look very odd in Chrome.

n Tom

@soonhokong I think he has a point, it looks weird. I believe the problem happens because we are using 'bold'. I think replacing the font is not feasible, since it took some effort to find one that works in most browsers. What do you think? For me, removing 'bold' is good enough :)