Re: [isabelle] Juxtaposed cartouche error in session run; okay in PIDE



On 1/9/2016 9:00 AM, Makarius wrote:
Have you tried Isabelle2016-RC0 already?

It provides many new things concerning document markup and markdown. Very few LaTeX macros are remaining. Since you are using creative add-ons to Isabelle document preparation, there is also a chance that something stops working.

Now is still a chance to work it out. Later in the release process, further changes will be less likely.

Makarius,

This email is to finish things up before I send in another email, about the big problems with RC1.

My game has changed, so I installed. I don't do proof with Isabelle anymore, so my need for help will be near zero.

I only do programming with Isabelle. The right foundation has to be laid, and programming is part of the foundation; there's not enough time to do both.

The first part is to you. The rest is just me talking.

I jumped to conclusions about `\<^emph>`, but the associated symbol for the command is good. Not having true italics is no big loss, but not having a true bold font would be a really big loss.

The extra bullet symbols are good.

I got everything converted that's important.

You switched the way Windows paths work, but I found those problems when you put out a test release last year. Here's how I now have to set USER_HOME to be able to change my home folder:

set USER_HOME=/cygdrive/e/D_1/w rk/g_d/gezz

I had some ML in between {*...*}, which allowed me to not having matching cartouches. Using 'isabelle build' wouldn't allow that. Now I have a dummy right cartouche like this:

val split1 = IsE.split_symS_delim_to_snd "\<open>" setup1; val _ = "\<close>"

I tell you that to let you know that all the programming commands I've implemented are all dependent on the cartouche delimiters.

*BAD PROBLEMS*

I'll send in a different email about the bad problems. There's been some bad process runaway, a blue screen of death, and bad hanging for the 64-bit Windows version.

*FRONT END MATH*

I've been driven by a simple number theory problem, where the proof was based on manipulating base ten digits.

The long story is too long, but here's a good book:

Computer Arithmetic and Verilog HDL, by Cavanagh

https://www.crcpress.com/Computer-Arithmetic-and-Verilog-HDL-Fundamentals/Cavanagh/9781439811245

That was supposed to give me the model for computer arithmetic in Isabelle/HOL, for number systems.

In my mind, I just break up a decimal number as a sum of digits, multiplied by the appropriate power. In Isabelle/HOL, it's not simple at all, because all the basic groundwork isn't there. It seems true types for at least bases 3, 5, 7, and 10 should be there.

Now, take a standard function, "f:A --> B", where A and B are elements of the power set of the natural numbers. How do you easily state A and B as your domain and codomain in HOL?

You don't, not easily. It could be reasonably easy, but right now it's not. Part of the problem is just a "syntax feature problem". It's not a logic problem.

Nothing in all this is a problem with the software. The software is powerful enough, if people are flexible and will fill in all the gaps.

Regards,
GB






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