[isabelle-dev] Incomplete .hgignore?

[Makarius]

On Tue, 14 Aug 2012, Tjark Weber wrote:

> Building the repository version (7476665f3e0f) with "isabelle build -a"
> generates a number of files that Mercurial doesn't know about (see
> below).

> $ bin/isabelle build -a
> [...]
> $ hg status
> ? doc-src/Classes/Thy/document/Code_Integer.tex
> ? doc-src/Classes/Thy/document/Code_Natural.tex
> ? doc-src/Classes/Thy/document/Setup.tex
> ? doc-src/Classes/Thy/document/session.tex
> ? doc-src/Codegen/Thy/document/Setup.tex
> ? doc-src/Codegen/Thy/document/session.tex
> ? doc-src/Codegen/Thy/examples/rat.ML
> ...
> ? src/HOL/SPARK/Examples/Sqrt/sqrt/isqrt.prv
> ? src/HOL/SPARK/Manual/complex_types_app/initialize.prv
> ? src/HOL/SPARK/Manual/loop_invariant/proc1.prv
> ? src/HOL/SPARK/Manual/loop_invariant/proc2.prv
> ? src/HOL/SPARK/Manual/simple_greatest_common_divisor/g_c_d.prv

That is normal for people who are used to build the doc-src stuff 
occasionally.  The difference is that it is now part of the regular build.

.hgignore should not be abused to hide that mess, otherwise the issue gets 
swepped under the carpet.  (AFP had some issues recently because of too 
liberal .hgignore.)


I am still in the process of reworking doc-src to make it more like a 
collection of normal sessions, not the odd collection of generated sources 
with some Makefiles operating on them in an odd way. Change c3ea910b3581 
from today is another step towards that.


> Ceterum censeo: Isabelle needs an issue tracker.

A good tracker needs at least two essential things:

   * good technology (most trackers lack that)
   * continuous maintenance, i.e. people actually taking care of it.

The majority of issue trackers in the wild are just a menagerie of "bugs" 
that are collected but not addressed.

This does not mean I am fundamentally opposed to a really convincing 
tracker, but I still don't see it emerging without engaging myself 
substantially in it.


(This particular case is not for a tracker at all, but for a mailing list 
like this one.)


 	Makarius