What is a closed form of $\int_0^1\ln(-\ln x)\ \text{li}\ x\ dx$ Let $\operatorname{li} x$ denote the logarithmic integral:
$$\operatorname{li} x=\int_0^x\frac{dt}{\ln t}.$$
Is it possible to find a closed form of the following integral?
$$\int_0^1\ln(-\ln x) \operatorname{li} x\ dx$$
I tried integration by parts, but only ended up with more complicated expressions.
 A: This integral can be expressed in a closed form:
$$\int_0^1\ln(-\ln x)\operatorname{li}x\ dx=\frac{\pi^2}{12}+\frac{(\ln2)^2}2+\gamma\,\ln2,\tag1$$
where $\gamma$ is the Euler-Mascheroni constant.

Proof:
Let
$$\mathcal{I}(a)=\int_0^1(-\ln x)^a\operatorname{li}x\ dx,\tag2$$
then, taking a derivative with respect to $a$, we get
$$\mathcal{I}'(0)=\int_0^1\ln(-\ln x)\operatorname{li}x\ dx.\tag3$$
Mathematica can express the integral $(2)$ in a closed form for explicitly given non-negative integer values of $a$, but not in a general form with a parameter. We could use those values to get a conjectured general formula, and indeed one could get the result $(1)$ this way. Numerical integration shows that
$$\Bigg|\frac{\pi^2}{12}+\frac{(\ln2)^2}2+\gamma\,\ln2-\int_0^1\ln(-\ln x)\operatorname{li}x\ dx\Bigg|<10^{-1000}\tag4,$$
so the result looks plausible.
But here we will follow a different approach to get a rigorous proof (modulo possible bugs in Mathematica tuned exactly to hide that tiny difference). Take the formula $(12)$ from the MathWorld article:
$$\operatorname{li}x=\operatorname{Ei}(\ln x),\tag5$$
where $\operatorname{Ei}z$ is the exponential integral, and plug it into $(2)$. In this form the integral can be evaluated in Mathematica, that gives us
$$\mathcal{I}(a)=-\frac{_2F_1(a+1,a+1;a+2;-1)\ \Gamma(a+1)}{a+1},\tag6$$
and, taking a derivative with respect to $a$,
$$\mathcal{I}'(0)=(1+\gamma)\ln2-\left[\frac{d}{da}{_2F_1}(a+1,a+1;a+2;-1)\right]_{a=0}.\tag7$$
To find the derivative of the hypergeometric function we need to replace it with its definition (formula $(8)$ in this MathWorld article):
$$_2F_1(a+1,a+1;a+2;-1)=\sum_{n=0}^\infty\frac{(a+1)\ \Gamma(a+n+1)}{(a+n+1)\ \Gamma(a+1)\ n!}(-1)^n.\tag8$$
So,
$$\left[\frac{d}{da}{_2F_1}(a+1,a+1;a+2;-1)\right]_{a=0}=\sum_{n=0}^\infty\frac{(n+1)(\gamma+\psi(n+1))+n}{(n+1)^2}(-1)^n,\tag9$$
where $\psi(n+1)=\frac{\Gamma'(n+1)}{\Gamma(n+1)}=-\gamma+\sum_{m=1}^n\frac1m\,$ is the digamma function. Evaluating this sum with Mathematica we get
$$\left[\frac{d}{da}{_2F_1}(a+1,a+1;a+2;-1)\right]_{a=0}=\ln2-\frac{(\ln2)^2}2-\frac{\pi^2}{12}\tag{10}.$$
Plugging this back in $(7)$ and $(3)$ we get the final result $(1)$.
A: Solution by Khalef Ruhemi
From the definition 
$$\operatorname{li}(x)=\int_0^x\frac{\ dt}{\ln t}=-\int_0^x\int_0^\infty t^y\ dt\ dy=-\int_0^\infty\frac{x^{y+1}}{1+y}\ dy=-\int_0^\infty\frac{e^{-(1+y)\ln(1/x)}}{1+y}\ dy$$
where we used $$\frac{1}{\ln t}=-\int_0^\infty t^y\ dy, \quad t\in(0,1)$$
It follows that 
\begin{align}
I&=-\int_0^1\left(\ln\left(\ln(1/x)\right)\int_0^\infty\frac{e^{-(1+y)\ln(1/x)}}{1+y}\ dy\right)\ dx,\quad \ln(1/x)=t\\
&=-\int_0^\infty\left(\frac1{1+y}\int_0^\infty e^{-(2+y)t}\ln t \ dt\right)\ dy\\
&=\int_0^\infty\frac1{1+y}\left(\frac{\gamma}{2+y}+\frac{\ln(2+y)}{2+y}\right)\ dy,\quad \frac1{1+y}=x\tag{*}\\
&=\gamma\int_0^1\frac{\ dx}{1+x}+\int_0^1\frac{\ln(1+x)-\ln x}{1+x}\ dx\\
&=\gamma\ln2+\frac12\ln^22+\frac12\zeta(2)
\end{align}

Regarding step $(*)$, we know that $$\int_0^\infty t^p e^{-(y+2)t}\ dt=\Gamma(p+1)(2+y)^{-p-1}$$
Differentiate both sides with respect to $p$ to get 
$$\int_0^\infty t^p e^{-(y+2)t}\ln t\ dt=\Gamma'(p+1)(2+y)^{-p-1}-\Gamma(p+1)(2+y)^{-p-1}\ln(2+y)$$
Set $p=0$ we get
$$\int_0^\infty e^{-(2+y)t}\ln t\ dt=-\frac{\gamma}{2+y}-\frac{\ln(2+y)}{2+y}$$
