Email Gateway (Aug 22 2022 at 16:53): Email Gateway (Aug 22 2022 at 16:53):From: Lars Hupel <hupel@in.tum.de>
Makarius,
you've introduced a warning for "isabelle build" that tells me when
files are not part of a Mercurial repository, like so:
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.
Would it at least be possible to opt out of this warning? 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.)
Lars
Email Gateway (Aug 22 2022 at 16:55):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 30 2024 at 04:19 UTC