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

On 14-04-22 10:33, Makarius wrote:
The "right language" depends a lot on what you want to do with it, but that should be common folklore anyway. As a Windows user you might be interested in F# which seems to have taken over most of the potential market share of OCaml in recent years. OCaml was once a big thing, but now it is just another scripting language performance-wise, since it is still not multicore capable.


It takes a lot of analyzing to figure out what's the right route to take, since time is of the essence, but at this point, my current frame of mind is that all my programming needs are relative to Isabelle/ML. If I hadn't been following the occasional discussions about ML vs. OCaml, such as between you and Mark Adams, I might be complaining about how imperfect ML is, but consistency is everything in logic, so not a complaint enters my mind about Isabelle/ML.

I don't do much programming, so I can't get good at ML if I don't do it, or something close to it. I'm not committed to Windows for this, and only decent performance is required for most scripting, so unless I go through another iteration to change my mind, or things just don't work, OCaml will support my use of ML more than anything else.

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.

I don't see the point. The Cygwin-Setup.bat is there to add whatever might be interesting in addition to the default packages that are necessary to run Isabelle and its standard tools. The Cygwin installation dialog is not ultra user-friendly, but any requests for improvements should be directed to the Cygwin guys and gals, especially Corinna Vinschen.

The point is to make things ridiculously easy for other people to do what I'm doing, so it increases the chance they'll want to do it too. But I don't expect you to care about "ridiculous easy" in every way.

I don't throw out these ideas expecting to get results any time soon. I put them out as early attempts to plants seeds. If something were to come out of this in two years, that would be more than what I expect.

The Cygwin dialog is not that bad. Once I get to the main dialog, I type in "ruby" or "ocaml", and it narrows down the selection. Five screen shots could give someone a good idea of what to do.

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.

I did look at it, but not very systematically.  Here are a few notes:

Here, we've entered into the realm of the professional versus the realm of an amateur. I took what you gave me, and I have to make it work for me within a reasonable amount of time. You would have to work out the details for a better way to do things, and you don't have time to do that.

I explain a little about your first point, and my experience with it.

I took the "cd" commands that you gave me, that use the master directory. I used them at the top of File1.thy to set the folder. I would move to File2.thy, which also used the "cd" command to set the folder for it's use. When I would move back to File1.thy, I would be working in the folder that File2.thy set. To get back to File1.thy's folder, I would have to go back to the top of File1.thy, and make an edit to force it to execute the "cd" again.

From that, my conclusion was that the only thing I can depend on for paths is hard-coded paths that are set using the cross-platform $HOME_USER or $ISABELLE_HOME_USER. It ends up being semi-portable. Everyone that starts Isabelle has a .isabelle folder.

Your 6th point is also related to my choice to use hard-coded paths, and that I'm hard coding them to a structure in a THY. All of that is my solution to trying to deal with my "awareness" of statelessness and mutability.

All I can do is take what you give me and use them as templates. Every template can only be extended so far, and then I have to have some understanding to extend them further.

At some point, it becomes a hack, where I start using whatever I can think of.

It is generally difficult to produce unique indentifiers that are actually unique in a sufficiently large scope. Within a running Isabelle/ML process you can use "serial ()" or "serial_string ()" for that, but it is also not 100% fool-proof if such ids persist over unrelated Isabelle sessions.

You didn't tell me this, but as far as I can tell, too different outer syntax commands that are using ML act as unrelated Isabelle sessions. What I've learned is that the only place I can depend on sequential order of execution is inside a particular outer syntax command.

I'd be happy for you to work out the details, but that's not going to happen. If you wouldn't have made me aware of statelessness and mutability/immutability, the unpredictability that happens would probably be a total mystery to me. If I can get a decent hack going, and not waste my time, that will be good enough. It's all just supposed to be a tool in support of proving theorems, with a little bit of computation.


- Load all files relatively to the implicit master directory of the
  enclosing theory.  This avoids absolute file-system references, and
  keeps your application "portable", i.e. you don't have to ask people to
  put things into a specific place.

- Watch out for global side-effects of Isar command declarations
  ('keywords') and their subsequent definitions in ML part of a theory.
  This implicit statefulness of the command table is TTY / Proof General
  legacy and easily leads to mistakes in the Prover IDE.

- Instead of fragile echo within the shell and its complicated rules for
  quoting, better use a temp file and stdin redirection (via "<").  See
  also the Isabelle/ML operation Isabelle_System.create_tmp_path or
  better the higher-order wrapper Isabelle_System.with_tmp_file.

- The type 'a Unsynchronized.ref in Isabelle/ML is just an alias of
  regular 'a ref, to empasize its unsynchronized nature, and to make it
  easier to get old ML code right with the help of static analysis: fewer
  ref operations are pervasive by default, so it is easier to locate its
  remaining uses.  The easiest way to give that up that discipline is ML
  "open Unsynchronized", but you should not do this in production code.

- A mutable HashArray is a very old-fashioned (and in general inefficient)
  data structure. Mutability belongs into the bucket with the label
  "premature optimization is the root of all evil".  On today's parallel
hardware it is often less efficient by default, and actually plain wrong without special precautions. See @{file "~~/src/Pure/General/table.ML"}
  for an efficient immutable data structure that can be used by default
almost everywhere, without requiring extra thinking about correctness or

  If you want to make a global cache of certain items, the canonical way
  is via some immutable table that is stored within a Synchronized.var.
Moving mutability away from the data structures to some topmost position
  is the first step to get things right (correct and efficient).

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.

Much could be said about random numbers, e.g. see what Scott Adams says. We have our own old jokes and running gags about the various random generators that are floating around in the Isabelle sources.

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