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

On Tue, 22 Apr 2014, Gottfried Barrow wrote:

I went through lots of iterations looking for the right language.

The "right language" depends a lot on what you want to do with it, but that should be common folklore anyway.

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

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.

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.

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.

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:

- 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.

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.


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