[isabelle-dev] Incomplete .hgignore?
Hi, Building the repository version (7476665f3e0f) with isabelle build -a generates a number of files that Mercurial doesn't know about (see below). I could simply add them to .hgignore, but perhaps someone who knows why these files are generated would be more qualified to do so? Best regards, Tjark $ 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 ? doc-src/Functions/Thy/document/session.tex ? doc-src/IsarImplementation/Thy/document/session.tex ? doc-src/IsarRef/Thy/document/Base.tex ? doc-src/IsarRef/Thy/document/Old_Recdef.tex ? doc-src/IsarRef/Thy/document/Wfrec.tex ? doc-src/IsarRef/Thy/document/session.tex ? doc-src/LaTeXsugar/Sugar/document/session.tex ? doc-src/Main/Docs/document/session.tex ? doc-src/ProgProve/Thys/document/MyList.tex ? doc-src/ProgProve/Thys/document/session.tex ? doc-src/System/Thy/document/session.tex ? doc-src/TutorialI/document/Basic.tex ? doc-src/TutorialI/document/Binomial.tex ? doc-src/TutorialI/document/Blast.tex ? doc-src/TutorialI/document/Examples.tex ? doc-src/TutorialI/document/Force.tex ? doc-src/TutorialI/document/Forward.tex ? doc-src/TutorialI/document/Functions.tex ? doc-src/TutorialI/document/Primes.tex ? doc-src/TutorialI/document/Recur.tex ? doc-src/TutorialI/document/Relations.tex ? doc-src/TutorialI/document/Setup.tex ? doc-src/TutorialI/document/Tacticals.tex ? doc-src/TutorialI/document/session.tex ? doc-src/ZF/document/FOL_examples.tex ? doc-src/ZF/document/IFOL_examples.tex ? doc-src/ZF/document/If.tex ? doc-src/ZF/document/ZF_examples.tex ? doc-src/ZF/document/session.tex ? src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.prv ? src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/f.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/hash.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_l.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_r.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_l.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_r.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/round.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/s_l.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/s_r.prv ? 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 -- Ceterum censeo: Isabelle needs an issue tracker. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Incomplete .hgignore?
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
Re: [isabelle-dev] Incomplete .hgignore?
On Tue, 2012-08-14 at 17:09 +0200, Makarius wrote: Building the repository version (7476665f3e0f) with isabelle build -a generates a number of files that Mercurial doesn't know about (see below). 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.) If these files are intentionally generated in isabelle/.../ and not meant to be under version control, I am not sure I see the abuse in adding them to .hgignore. On the other hand, if they are a mess and an issue, perhaps that could be addressed. Anyway, what do you do to keep the output of hg status uncluttered? Best regards, Tjark -- Ceterum censeo: Isabelle needs an issue tracker. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Incomplete .hgignore?
On Tue, 14 Aug 2012, Tjark Weber wrote: Anyway, what do you do to keep the output of hg status uncluttered? Nothing, there is just a lot of garbage accumulating. (This does not mean regular Isabelle sessions should write into the source space under normal circumstances.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Incomplete .hgignore?
On 14.08.2012 20:12, Tjark Weber wrote: If these files are intentionally generated in isabelle/.../ and not meant to be under version control, I am not sure I see the abuse in adding them to .hgignore. On the other hand, if they are a mess and an issue, perhaps that could be addressed. Anyway, what do you do to keep the output of hg status uncluttered? If the .hgignore in the repository stays at it is, you can add your own private ignore file; see hgignore(5). -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
