Email Gateway (Aug 19 2022 at 14:09): Email Gateway (Aug 19 2022 at 14:09):From: Makarius <makarius@sketis.net>
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# http://fsharp.org/ 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
efficiency.
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
http://dilbert.com/strips/comic/2001-10-25/ 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.
Makarius
Email Gateway (Aug 19 2022 at 14:11):From: Makarius <makarius@sketis.net>
My hint was more basic that this. Your ML_file references where all
absolute, but by just removing a prefix it becaume relative to the master
directory of the enclosing theory, and thus became "portable".
Makarius
Email Gateway (Aug 19 2022 at 14:12):From: Makarius <makarius@sketis.net>
It is about HOL-Zero and Ocaml as unsafe programming language etc.
A very entangled variant of several related and unrelated threads around
this can be seen here on the HOL mailing list:
Title of the thread: "Re: rigorous axiomatic geometry proof in HOL Light".
Makarius
Email Gateway (Aug 19 2022 at 14:12):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Incidentally, the gmane interface to the mailing list, at for example
http://article.gmane.org/gmane.comp.mathematics.hol/1605/
is much nicer than the antiquated UI available through sourceforge.
Michael
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 19 2024 at 20:15 UTC