[isabelle-dev] Isabelle build only works in certain directories

[Makarius]

On 02/07/18 12:59, Max Haslbeck wrote:
> 
> When I’m in one of the "wrong" directories the build process spend most
> of its time in the function Mercurial.check_files [1]. The problem seems
> to be that the paths in hg.known_files() are relative to the current
> working directory. So "hg.root + Path.explode(name)" returns an
> incorrect path. The filtering of files in the next lines then doesn’t
> work and it reruns check() for every file.
> 
> The build process works in the directory "~/tmp/tmp" because the paths
> in hg.known_files() start with "../../" and by luck "hg.root +
> Path.explode(name)" returns a correct path.
> 
> The version of my mercurial installation is 4.6.1.
> 
> [1]
> <https://isabelle.in.tum.de/repos/isabelle/file/1b9462304e1d/src/Pure/General/mercurial.scala#l156>

Thanks for going to the bottom of it. Mercurial.known_files is merely a
command-line invocation as follows:

"${HG:-hg}" --config defaults.status\= --repository
/home/makarius/isabelle/repos --noninteractive status --modified --added
--clean --no-status


I did not see the reported problem: the file names are always relative
to the repository root, independently of the current working directory.
I have tried it Mercurial 4.6.1 on macOS 10.13.5, and Mercurial 3.7.3 on
Ubuntu 16.04.

So there must be something else in your setup. If we can figure this out
within the coming days or weeks, I can still do something about it for
the Isabelle2018 release.


	Makarius