max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(doc/bin/README): remove options that no longer exist

Browse source
This commit is contained in:
Gabriel Ebner 2017-06-12 15:42:40 +02:00
parent fa8d690559
commit 0e864e5e9f
1 changed files with 0 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
doc/bin/README.md
View file

@ -23,28 +23,3 @@ and provides many examples. The tutorial is available in two different forms:
- Interactive HTML: http://leanprover.github.io/tutorial/index.html
- PDF: http://leanprover.github.io/tutorial/tutorial.pdf
Command line options
--------------------
Here are some useful commands for users that do not want to use Emacs,
or prefer command line tools.
- `-T` do not type check imported .olean files
% bin/lean -T examples/ex.lean
The option can save you a significant amount of time if you are importing
many files. Lean still checks the check-sum of the imported files.
So, it still can detect trivial tempering of the .olean files.
- `-c [file.clean]` create/use a cache file. This option can increase the
compilation time of large files when we are invoking Lean many times
with small incremental changes.
% bin/lean -c ex.clean examples/ex.lean
- `--deps` display files imported by a given Lean file. This option
is useful if you want to build your own custom Makefile.
% bin/lean --deps examples/ex.lean