update local building instructions in README.md

[dimpase]

It will fix #283

[dimpase]

for the record, with the latest branch d60b223, the workaround is still needed, without it it's still an error:

%  cd book        
% lake exe fp-lean
info: verso: cloning https://github.com/leanprover/verso.git
info: verso: checking out revision '637d1288c590366c177c465916177817d33fa485'
info: illuminate: cloning https://github.com/leanprover/illuminate
info: illuminate: checking out revision '56958b3901ca108830de34fbce6cecd4b5757c1f'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'b1c4a69a7e247ab7df20460212001673d74f08c0'
info: MD4Lean: cloning https://github.com/acmepjz/md4lean
info: MD4Lean: checking out revision '31907cc18f48a95384f99cee5582c00fb39e0f67'
info: subverso: cloning https://github.com/leanprover/subverso
info: subverso: checking out revision '4db22f2caed235317d21945d1b51fba0fdb69e89'
� [94/612] Running exampleBinaries
error: no such file or directory (error code: 2)
  file: /Users/dima/software/lean/fp-lean/book/../examples/.lake/build/bin
Some required targets logged failures:
- exampleBinaries
error: build failed

[dimpase]

the produced html is a bit buggy, however. With Linux/firefox, links aren't followed directly, one gets pages showing directories with index.html files in them; so navigation needs an extra click.

Also, on macOS it's even worse - there these index.html files don't open at all (perhaps there are some browser settings which should be modified - I don't know, I am not an macOS desktop user)

[dimpase]

As well, the resulting document just doesn't work offline, probably due to hardcoded URLs to certain js stuff, such as
e.g.

   <script src="https://cdn.jsdelivr.net/npm/marked@11.1.1/marked.min.js" integrity="sha384-zbcZAIxlvJtNE3Dp5nxLXdXtXyxwOdnILY1TDPVmKFhl4r4nSUG1r8bcFXGVa4Te" crossorigin="anonymous"></script>

[david-christiansen]

With the latest master version, the instructions in the README do the right thing with a fresh checkout on my machine. Better to fix it than to add more docs, I figured. Thanks for engaging on this!

WRT the HTML: Verso's output is not intended for use with file:// URLs. It requires a local web server. The one CDN dependency (marked) should be reasonably optional (it's used for some Markdown rendering inside of hovers). Can you try it out that way?

[dimpase]

lake exe fp-lean isn't enough for me on a clean checkout. The 1st run stops as follows:

% lake exe fp-lean
info: verso: cloning https://github.com/leanprover/verso.git
info: verso: checking out revision '655d4f6e89bbf4c3c946e54625dcbe1539ea1107'
info: illuminate: cloning https://github.com/leanprover/illuminate
info: illuminate: checking out revision '56958b3901ca108830de34fbce6cecd4b5757c1f'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'b1c4a69a7e247ab7df20460212001673d74f08c0'
info: MD4Lean: cloning https://github.com/acmepjz/md4lean
info: MD4Lean: checking out revision '31907cc18f48a95384f99cee5582c00fb39e0f67'
info: subverso: cloning https://github.com/leanprover/subverso
info: subverso: checking out revision '859ab80c32c5851151919a7d757d7c0c0b6e39d2'
ℹ [232/237] Built book/buildExamples
info: Building examples in ../examples
%

That is, some dependencies aren't still set up quite right.
The process seems to converge after 3 iterations:

% lake exe fp-lean
ℹ [232/252] Built book/buildExamples
info: Building examples in ../examples
% lake exe fp-lean
ℹ [232/303] Replayed book/buildExamples
info: Building examples in ../examples
% lake exe fp-lean
ℹ [233/614] Replayed book/buildExamples
info: Building examples in ../examples
% lake exe fp-lean
ℹ [233/614] Replayed book/buildExamples
info: Building examples in ../examples
% lake exe fp-lean
ℹ [233/614] Replayed book/buildExamples
info: Building examples in ../examples
%

[dimpase]

w.r.t. HTML, if there are still JS references to stuff on a CDN, then it won't work with a local HTTP server, anyway?