I'm an outsider, and prefer no feedback, which is either being rude, or stating a necessary formality.
I've long been scrolling to the end of theories to make sure they check error free, but lately, several times, I see no errors, turn my computer off, and then the next day errors show up when I start things up. That's a scary thought; proving what you didn't prove.
There are some related user-list emails about this, on doing an official run of a sessions to catch that sort of thing. I got the verbose flag from this one by L.Hupel:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-October/msg00106.htmlIt also talks about a part of the problem I've experienced. A metis proof is good, and applied with a 'by' command, but then I make changes, and then some metis proof doesn't kick out. It just churns away forever, but I don't know about it. The 'by' statement still results in the theorem being used after that.
For some reason either errors aren't showing up in the sidebar, or "purple proof action" isn't showing up there. It could be because I changed "Editor Reparse Limit" from 10000 to 100000. Regardless, I need that so that errors clear on big commented out sections in the THY.
I've gone official now, by finally starting to run the sessions with 'isabelle build', which is nothing extraordinary. What's special is that I both edit the 'ROOT' file, and run 'isabelle build -v -D .', in the THY.
That can be done with my custom 'I.bash' and 'I.prog' commands, which are not to be talked about here, only admired.
The first attached screen shot shows my experiments with 'quick_and_dirty' mode, running the session with the option friendly 'I.bash', which runs a script without writing it to a file. There are others, or were, like I.perl, I.pypy, and I.polyml. I still need to set up I.nodejs.
When I tried again, things went bad with running 'isabelle' in the PIDE. Things were spawning other things too much.
The 2nd screenshot shows my switch to the very useful 'I.prog', where I'm just using it to write a file, and run bash. It can be used with any compiled language or scripting language, for which bash files and makes files have been set up, or with any build tool, like Ruby rake.
Again, not something to be talked about, only speculatively admired. Is it wannabe-ware? Or is the real thing? Options. It has 'em. Help? Use the 'h' switch, in your mind.
Description: PNG image
Description: PNG image