Re: [isabelle-dev] document_output vs. old document_dump/document_dump_mode
On 28/08/2012, at 8:06 PM, Makarius wrote: > Are there remaining uses (or users) of the old document_dump / > document_dump_mode options? This corresponds to former options -D and -C of > isabelle usedir. > > The meaning of these features has become quite difficult to define, so it > looks like they are better discontinued. > > If there are remaining cases of difficult IsaMakefile/usedir configurations > that still use them, they can be discussed here to see if anything is still > missing in the new build tool to replace them. I use -D/document_dump extensively for producing papers. The Isabelle Latex output pretty much always requires post processing for anything that has higher type setting requirements. My standard setup these days is not to use root.tex for papers, but only to generate .tex from .thy, then post-process, then include manually in a master .tex file. It looks like document_dump with default "all" for document_dump_mode produces what I need, though (even "tex" would be sufficient). Tobias and I had a setup where we also needed isabelle.sty, but we could subsume that with document_output. A small annoyance with document_output was that the output doesn't seem to get produced for document=false (i.e. seems to force a latex run) and that it insists on creating a "document" subdirectory in the target directory that I give it. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] document_output vs. old document_dump/document_dump_mode
Are there remaining uses (or users) of the old document_dump / document_dump_mode options? This corresponds to former options -D and -C of isabelle usedir. The meaning of these features has become quite difficult to define, so it looks like they are better discontinued. If there are remaining cases of difficult IsaMakefile/usedir configurations that still use them, they can be discussed here to see if anything is still missing in the new build tool to replace them. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle manuals as regular session documents
This is an update on this ancient issue, which is not NEWS since it is not relevant to users, only for people hooked on the repository. It should nonetheless simplify many lives. This refers to Isabelle/037d32448e29, which also contains a short update on README_REPOSITORY. * The doc sessions now conform better to the current Isabelle document preparation system (from > 10 years ago) with some recent updates on the build process. * The sources are in src/Doc together with all other session sources. This is not nostalgy for the old name "Doc" from many years ago, but helps to grep/hypersearch over session sources exhaustively. * The Admin tool "isabelle build_doc" helps to populate the doc/ directory on the spot, such that "isabelle doc" finds the results. This is again one less reason for the old-style development snapshot produced by isatest. (Is anybody still working with that?) Authors of non-outdated manuals should take a brief look if things still look the way they should be. Latex is a bit weak in formally checking its input -- \include does not even stop on missing files. Note that option document_output greatly helps to organized document output, but this particular option should not be hard-wired in public sessions, since it will spill output in some directory where it might not be wanted by others. The old doc-src directory can now be purged manually in local clones, but this requires some care. I've wiped out one of uncommitted my draft files today already. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS
* HOL/Codatatype: New (co)datatype package with support for mixed, nested recursion and interesting non-free datatypes. * HOL/Ordinals_and_Cardinals: Theories of ordinals and cardinals (supersedes the AFP entry of the same name). Kudos to Andrei and Dmitriy! Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle/jEdit: Feature Requests for Ctrl-Click
Just to add that I'm very grateful for this support which enables Poly/ML to continue and get better with each release since I don't have a university or a big company behind me. If anyone has a feature that requires work on Poly/ML and a bit of money I'm happy to discuss it. David On 27/08/2012 20:27, Lawrence Paulson wrote: Various projects of mine, going back many years, have supported Poly/ML at the rate of £1000 per year. (That's just under €1300.) This is a much better use of grant money than to give it to already wealthy publishers for the sake of so-called Gold open access. Larry On 27 Aug 2012, at 16:18, Tobias Nipkow wrote: Just for the record: I have spent over 20k EUR to this over the past 1 1/2 years but that will have to be it from the TUM side. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle/jEdit: Feature Requests for Ctrl-Click
On Tue, 28 Aug 2012, Christian Sternagel wrote: Sometimes it is just hard to know whether some snag was not detected yet or is already in the pipeline... so I report anything ;). After so many years, Isabelle pilelines have become looong, so it is very likely that whatever you name is in there already. Nonetheless, you should report whatever you observe and find relevant. There might be new things coming from that that are *not* yet in any pipeline system from the Ural, and it always helps to figure out priorities what needs to be pulled or pushed forward a bit more quickly than 5-10 years. Maybe it would be a good idea to collect "feature-requests" in the wiki? We are back to the tracker issue, which has already become a running gag on this mailing list. A wiki is very bad technology to track feature reports or bug requests. There are dedicated trackers for that, but most of them are also quite bad. More recently some non-bad trackers have emerged, so it might be worth revisiting the question with a clear mind at some point. Apart from that, technology alone never solves a problem. It needs to be supported by people behind it, and this is exactly where most tracker-based project that I've ever seen are lacking. E.g. when I put something on one of the many jEdit trackers on Sourceforge (another bad technology), it takes a very long time to get any feedback on it, even just that it has been seen by someone. Other projects like Cygwin define themselves as explicitly tracker-free. When I posted something on their mailing list -- an actual "issue" -- I've got feedback almost as quickly as normally on isabelle-dev. (The official place of collection is currently the mailing list, but it is not that easy to extract this kind of information.) I mean, in order to have a place to point like: "first look there and only if you do not find your 'feature' there, write to the mailing list". The mailing list archive also helps. It has the advantage that it provides an historical context to some issue and its discussion, unlike a wiki that is always known to be outdated without explicit clues. (This is also a reason why it is so important to quote changeset ids when pointing to anything in the repository.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle/jEdit: Feature Requests for Ctrl-Click
On Tue, 28 Aug 2012, Tjark Weber wrote: On Mon, 2012-08-27 at 13:35 +0200, Makarius wrote: 1) In "theory T imports A", I'd like to be able to Ctrl-click on A to open the corresponding theory file. See some changesets leading up to Isabelle/10b89c127153 how I've spent Sunday afternoon. Nice. I suspect it would be considerably more work to support C-click in already loaded theories (e.g., HOL/Main)? That is a conceptually different problem: loaded images are "dead" wrt. document markup. It will take several more rounds of refinement until the heap image concept is unified with the online document markup. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] mira disk usage
Hi, since a few weeks, mira's shared results (/mnt/tmp/isatest/shared_results on anything but macbroy2) started taking a lot more disk space then before; I got a quota warning today (500GiB); the last one was exactly three weeks ago). Most space seems to spend with Isabelle_makeall and AFP runs, amounting to 4-5GiB each. Has someone an idea what changed? If yes: do we want to revert to store less stuff again or should we implement some kind of automatic cleanup? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
