Theorem proving in Lean down?

Stream: general

[Terence Tao]

Is it just me, or is the link

https://lean-lang.org/theorem_proving_in_lean4/title_page.html

to "Theorem proving in Lean4" currently broken?

[Jason Rute]

https://lean-lang.org/functional_programming_in_lean/ is also down I think. @David Thrane Christiansen

[N Gelwan]

Two commits tonight

• https://github.com/leanprover/lean-lang.org/commit/ac5bfcfef79b9a395b8eadb24473eb213f4cd9eb
• https://github.com/leanprover/lean-lang.org/commit/2a473d9ea6b19e412e47fd4ee0751907316c1cdd

Perhaps "un-domain self-links"? Not sure how github.io works

[Patrick Massot]

@Sebastian Ullrich :up:

[N Gelwan]

Here's a quick pull request in case that was the problem: https://github.com/leanprover/lean-lang.org/pull/110

[Jiahua Chen]

In the meanwhile, I've been able to access the GitHub pages deployments directly at the leanprover.github.io links: like https://leanprover.github.io/theorem_proving_in_lean4/introduction.html if anyone is looking for working versions (same holds for Functional Programming in Lean and other docs)

[N Gelwan]

Nice

[Sebastian Ullrich]

Thanks for the reports, they are back now. It was a configuration mistake.