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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
