leanprover
Online tutorial's links do not support Cmd-click, do not preserve browser history, and more
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.
I'll take this occasion to express how excited I am about Lean. The tutorial is especially user-friendly.
You're welcome. Normally I'd try to contribute pull requests, but finals are looming in Canada so I can't start anything. Good luck.
@lilred, sure. When you have a chance, please contribute to this repo :-) Good luck with your finals!
There's a related issue which I'm not sure how to consistently reproduce. Sometimes, when using the drop-down list to go to one chapter to the next, I end up on, say, section 4.3 instead of the top of the Chapter 4 page. I'm going to open an issue once I figure out how to repro.