[isabelle-dev] NEWS: Isabelle server

Makarius makarius at sketis.net
Mon Mar 26 13:26:34 CEST 2018


On 26/03/18 09:33, Christian Sternagel wrote:
> 
> I don't see a significant difference in output between my original
> 
>   isabelle build_doc system

> *** Failed to build document in
> "/tmp/isabelle-griff/document_output1585848392449927242/system"
> 
> and the suggested
> 
>   isabelle build -c -b System -o document=pdf -o document_output=output
>
> *** Failed to build document in
> "/home/griff/repos/tools/isabelle/src/Doc/System/output/system"
> 
> I am still unclear on why "isabelle document" fails in both cases.

The difference is the output directory. In the latter situation, you can
go there and inspect root.log or run pdflatex root manually.


	Makarius




More information about the isabelle-dev mailing list