Lean tutorial fails on "set_option profiler.freq 10"

catskillsresearch commented 3 years ago

Prerequisites

[ X] Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
  - Specifically, check out the wishlist, open RFCs, or feature requests.
- Reduced the issue to a self-contained, reproducible test case.

Description

Lean tutorial https://leanprover.github.io/introduction_to_lean/ fails on "set_option profiler.freq 10"

Steps to Reproduce

Press "set_option profiler.freq 10" gives error

Expected behavior: No error Actual behavior:

2:11:error: unknown option 'profiler.freq', type 'help options.' for list of available options
Done(0.001sec)

Reproduces how often: [100%

Versions

https://leanprover.github.io/introduction_to_lean/

Additional Information

Reproduced in browsers on two separate machines

PatrickMassot commented 3 years ago

Unfortunately you managed to find an extremely outdated document. See https://leanprover-community.github.io/ for up to date information about the current version of Lean. This GitHub repository is about the next version of Lean which is not yet ready for users (see the README).

catskillsresearch commented 3 years ago

The newer docs point me to this and it just says sorry all the way through. The extremely outdated doc at least works most of the time

http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=1&level=1

It's OK I'll figure it out but my intuition is to go through this oldest stuff first.

leanprover / lean4