[isabelle] Please make OCaml and Ruby part of the Cygwin distribution



Hi,

I went through lots of iterations looking for the right language. Dissatisfaction is a good thing, if it leads to a better solution.

Part of first passing over OCaml was that it doesn't come installed with Cygwin, where Perl and Python do.

I finally figured out that others don't have to have languages installed. My theories won't be full of warnings, for what I distribute, since program code won't mostly be enabled. Programming needs aren't the same as proving needs.

But, though It's very easy for me to install OCaml and Ruby on Cygwin, with Cygwin-Setup.bat, it might not be easy for someone who has never done it before.

If OCaml and Ruby came as part of Cygwin, in the contrib folder, then things would be closer to working by magic, if someone was trying to do what I'm doing. At least it would be for Cygwin. I don't worry about Linux.

I attach a zip file. I don't expect anyone to look at it, but I attach it to show, as part of the request, that my request has something behind it.

What I'm trying to do has gone from "an interesting experiment" to being "work to finish it off", but I make my request now because people need time to think, a release is coming up, and I might need another month to work this out.

Part of the work is related to dealing with the statelessness of the PIDE. It's not that complex to implement, but my current is idea is to use a hash table along with a random number generator to get a name. There's a number of them available, but I guess I'll use the one from Larry Paulson's book that I acquired recently from the SML/NJ import. The SML/NJ Library manual has some things to say about it.

Getting some basic regular expressions was also important. The way it's working with these interpreters is that I use echo to pipe a string to them, though I don't know if that will ever cause a problem. I use up the single quote character, but it was easy to use the regular expressions to deal with that, once I figured out the solution. Also, it would be a real pain to get arguments from a string without regular expressions.

I attach a couple of screen shots. Learning OCaml will be a lot like learning Standard ML, except when its different, at which times it will be learning what's special about OCaml, along with using what I've already learned, which will be a lot like what's the same about SML, if you get my drift.

As to where Ruby is in all of this, it's just there.

What's in the zip file works for me. If you want to look at it, you put the folder in your .isabelle folder, and open up Iz0/examples/Script_Commands.thy.

Regards,
GB



Attachment: 140422a__gc44_IzS__Examples__Script_Commands.zip
Description: Zip archive

Attachment: 140422a__some_OCaml.png
Description: PNG image

Attachment: 140422a__taking_arguments.png
Description: PNG image



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