Re: [isabelle] Annoying message about "unknown files"



On 05/03/18 16:41, Lars Hupel wrote:
> 
> ### Unknown files (not part of a Mercurial repository):
> ###   /home/lars/work/reify/isabelle-cakeml/thy/generated/CakeML/Ast.thy
> ### ... many more lines ...
> 
> While this is technically correct – they're indeed not part of a
> Mercurial repository –, it is also annoying, because they are part of a
> Git repository.

I have now changed it here:

changeset:   67782:7e223a05e6d8
tag:         tip
user:        wenzelm
date:        Thu Mar 08 11:46:37 2018 +0100
files:       src/Pure/General/mercurial.scala src/Pure/Tools/build.scala
description:
clarified notion of unknown files: ignore files outside of a Mercurial
repository;


> If I'm reading
> the sources correctly, it is triggered by whether or not Isabelle itself
> is under Mercurial control:
> 
>   check_unknown_files = Mercurial.is_repository(Path.explode("~~"))
> 
> That doesn't seem particularly useful to me. (The warning may be useful
> to people who run stable Isabelle, for example.)

The main purpose is to guard against accidental pushes on Isabelle or
AFP, without having added new files. This fits to the standard model of
Isabelle testing: "isabelle build -a" and careful inspection of "hg
diff" before "hg push". The scheme still works for other projects (like
IsaFoR or IsaFoL) as long as it is for the Isabelle repository.

That check is inactive for official releases, because finding the
repository root of a file means to traverse the whole directory tree to
the top. That might be expensive in the case where none such root exists
-- the check needs to be done for thousands of files. Moreover, towards
the top of the file-system it could become dangerous to trip on certain
special mount points, e.g. on Windows this can cause long / infinite delays.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.