Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized



On 10/29/2012 8:21 PM, Christian Sternagel wrote:
On 10/30/2012 03:51 AM, Gottfried Barrow wrote:
...I at least try to end up having made an educational contribution.
I tried to achieve something very similar in my PhD-thesis (the content is not really textbook-like, but the presentation was intended for people that do not know Isabelle/HOL). Just ignoring the content you could have a look whether this way of presentation could be used in your case.

http://www.jaist.ac.jp/~c-sterna/publications/PhD-thesis.pdf

Okay, this ends up being a perfect example to tie into things I said, or could have said, and the essence of your complaint about noise and clutter.

You give me a document that you spent a lot of time on to make it a professional grade document, and you offer to give me the TEX source (or THY with a lot of LaTeX in it).

I open the PDF, and I think something that I don't plan on saying at the time, like, "Well, TEX files and TEX content are a dime a dozen on the web, and I've already made many of my LaTeX design decisions. Your blue text boxes look good, but I ruled out using colored boxes some time ago, though seeing how you do it might get me to think about it again."

You tell me to ignore the content, but then when I get to your Chapter 2, I say, "Alright, another one of these PhD theses which provides a short tutorial on Isabelle. I need to read this Chapter 2."

In fact, your PhD thesis has been setting on my hard drive with documents from 13 other people, most of who I found on the TUM web site, and all of whose articles I ripped off of their sites. Those along with most if not all documents off of Wenzel's, Nipkow's, and Paulson's web pages.

As it turns out, I'm not interested in your source, I'm interested in your content. I gave you a THY, and you weren't interested in my involved system, you just wanted to see the pertinent content, which was obscured.

I think this describes most of us. We want to know what a person has to say, or what their code says. We're not normally interested in people's low-level methods of creating source code.

And now that my attention is brought to your tree in the forest, I see that on page 13 and 19, you say that implicit quantification is happening at the meta-logic level. Without the examples you gave me, it wouldn't have the same meaning that it does now.

However, it was a huge overhead over the actual formalization to present it this way ;). (And I found it necessary to explain at least a bit about Isabelle in the beginning.)

This brings up how we work with THY and TEX files. We read the PDF for the discussion of concepts, and we read the THY (if we have to, or to edit it) for the non-text{*...*} code.

I'm trying to get away from this two-document editing process. It's a pain. Edit, then compile to be able to read it and make sure it compiles. Do that again forever, hitting the compile button multiple times on many loops because of a LaTeX error.

REMARK: The continuous prover mode of jEdit makes errors immediate, which helps to get away from a "compile to make sure it compiles" type process of editing code. Thanks Makarius.

You talked about me reinventing the wheel. This huge overhead you talk about is something I want to do once, and then benefit from easily and repeatedly.

First, I do a lot of work to set up a THY document style that can be processed by a script, and I write a bunch of jEdit macros for text entry.

After that, I'm in "cheap imitation WYSIWYG word processor mode". I compile to PDF, not to see if it compiles (unless I had to resort to LaTeX), and not to read what I wrote, but to create a professional looking document to give to other people. The script also creates a bare-bones THY to give to other people like you who don't want any verbosity, or help from me to know what the code means. And the code that's in the bare-bones THY? It's also in a verbatim environment in the TEX file that gets compiled. (Any of this is subject to change.)

If you (or anyone else) are interested I can send you the sources later.

TEX sources? A dime a dozen. Pertinent, good instructional content on Isabelle that's generated from LaTeX, like your Chapter 2? A very, very small percentage of the content that is generated from the millions of lines of LaTeX in the world.

Thanks for bringing attention to your thesis.

Regards,
GB








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.