Email Gateway (Aug 22 2022 at 11:37): Email Gateway (Aug 22 2022 at 11:37):From: Gottfried Barrow <igbi@gmx.com>
This is either shameless advertisement, or useful disclosure to raise
some awareness.
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.html
It 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.
Regards,
GB
151027_IDE_bash_isa_build.png
151027_IDE_build_ext_cons.png
Last updated: Apr 26 2024 at 20:16 UTC