[isabelle-dev] Bad documentation directory

Makarius makarius at sketis.net
Mon Feb 12 14:01:27 CET 2018

On 12/02/18 10:52, Lars Hupel wrote:
> When I clone a fresh copy of Isabelle, or run "hg clean --all", then
> "isabelle build" fails with the following error message:
> *** Bad documentation directory:
> "/home/lars/work/isabelle/src/Tools/jEdit/dist/doc"
> That directory is not present by default and appears to be only created
> by "isabelle jedit". A workaround is to always run "isabelle jedit -bf"
> before running "isabelle build".

That is a consequence of the formal treatment of documentation names here:

changeset:   67462:bddfa23a4ea9
user:        wenzelm
date:        Fri Jan 19 14:55:46 2018 +0100
files:       src/Pure/ML/ml_process.scala src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala src/Pure/PIDE/resources.ML
src/Pure/Thy/document_antiquotations.ML src/Pure/Thy/sessions.scala
src/Pure/Tools/build.ML src/Pure/Tools/build.scala src/Pure/Tools/doc.scala
formal treatment of documentation names;

I've made it again more permissive here:

changeset:   67604:02cf352cbc4c
tag:         tip
user:        wenzelm
date:        Mon Feb 12 13:27:30 2018 +0100
files:       src/Pure/Tools/doc.scala
permissive Doc.dirs: some entries may be absent due to distribution
bootstrap, e.g. $JEDIT_HOME/dist/doc;

That is for merely convenience when experimenting with a few sessions
from a cloned repository. A formal test does require "isabelle jedit -b"
before "isabelle build -a". (That is implicit in the order given in
README_REPOSITORY and explicit in the build_history tool.)


More information about the isabelle-dev mailing list