Some interesting views here by Paulson on SML vs. (O)Caml, would be interesting to hear insiders comment...
for a functional language, let’s just say it’s odd that OCaml doesn’t have a streamlined syntax for (drum roll) declaring a function using pattern-matching
The main praise I remember of Caml in the 1990s was “it enjoys institutional support” (certainly true) and “it works with UNIX makefiles”
When I was porting HOL Light libraries, I occasionally had to replay a proof. I would have to launch OCaml, first thing in the morning. I could load the sources of HOL Light in under a minute. But the full analysis library would not finish loading until after lunch. This is a world-beating system?
they say that OCaml is finally catching up [to threads in Poly/ML], 15 years later, thanks to having 100 times as much funding.
The first point is fair, though it is mostly a matter of taste; I for one do not care about such programming style. The second point is a bit distorted; the part about makefiles means that Caml code could be compiled to object files that could then be passed to the system linker; this was certainly seen as an improvement at the time. The third point conflates John's design decisions (e.g., using the bytecode repl) with the performance of OCaml; this is the most unfair of his points, in my opinion. The fourth point is the fairest one.
Does OCaml have 100 times more users than polyml?
(just one way to cut the crap)
I guess we can use this to approximate relative users (Jan 2022): https://redmonk.com/sogrady/files/2022/03/lang-rank-0122-wm.png
SML is well behind Coq at this point on GitHub, OCaml is just trailing Haskell and Perl
and it's a bit of a disappointment in the SML world that threads are not portable across compilers. But as an SML user, the lack of a widely used package manager is the worst pain point (this is the current best approximation)
I don't think we should feed the troll
fine by me, but I didn't even understand the point about Makefiles until Guillaume's comment.
it's called separate compilation for the civilized ones
(and I think some SML implementations do have it)
it is really a trolling post
Where is the trolling in the post? I can't pinpoint any specific part IMO that would count as a troll. There are some personal opinions, that's different.
some writers like to separate opinions from facts more explicitly :-)
Paolo Giarrusso said:
some writers like to separate opinions from facts more explicitly :-)
what concrete phrase you have a problem with?
I feel the tone is pretty biased beyond my literary criticism ability, but "This is a world-beating system?" is an example that I would object, say, in a paper peer review (just as a case where opinions _must_ be explicitly annotated)
Yup, Lawrence is quite biased that's obvious. But this is why I like to understand if he says something wrong or troll vs his own opinion.
The latter can't be addressed, the former yes
Does trolling implies saying something wrong?
In this case "this is a world beating system" I have to agree with him
if that's the user experience for HOL , that's terrible
tho it would be nice to ask for a clarification there
to see he means HOL, not OCaml
OCaml has its own problems
when I migrated from Haskell I was far from impressed, and Haskell is not the 5th wonder of the world
it also has very good things of course
I can't define "troll" well enough to debate it, but he doesn't seem to believe in OCaml enough to be precise about what's going on. Of course, real problems exist :sweat_smile:
@Emilio Jesús Gallego Arias I think you are the only one who thinks he's talking about HOL here.
here's why he blames OCaml for it:
With no way to save an image, you had to rebuild HOL Light from sources at every launch (even today). Even Edinburgh LCF was a stand-alone executable.
somehow the option of doing <anything else than saving an image> isn't even worth mentioning — I mean, does Isabelle save images?
SML can save a heap image for the state of any program, to my knowledge, so Isabelle uses them, see for example here: https://sketis.net/2017/isabelle-docker-image
I don't know why HOL Light doesn't use native compilation in OCaml, I can't think of an obvious reason why one couldn't native-compile modules piecewise and then get a REPL on top that, but I've never seriously used HOL Light or the OCaml REPL
I was mostly wondering why they can't compile sources to binaries and load the binaries, instead of reproving theorems
Maybe because of when HOL Light was created?
from HOL Light README on GitHub:
There are now two alternatives: launch the OCaml toplevel and directly load the HOL Light source files into it, or create a standalone image with all the HOL Light sources pre-loaded. The latter is more convenient, but requires a separate checkpointing program, which may not be available for some platforms.
yes, apparently, they're happy to link to _checkpointing tools_, which worries me a bit (maybe for no good reason)
... I guess abstract types would force serialization into an LCF kernel, and somehow they're not willing to trust that, while trusting the checkpointing tool?
this is apparently the checkpointing tool of preference these days: https://dmtcp.sourceforge.io/
my understanding is that for most purposes, HOL Light could be called "John Harrison's HOL". If John doesn't need a feature (like convenient incremental compilation of theories) it doesn't get added
http://www.catb.org/jargon/html/T/troll.html
1. v.,n. [From the Usenet group alt.folklore.urban] To utter a posting on Usenet designed to attract predictable responses or flames; or, the post itself.
... Some people claim that the troll (sense 1) is properly a narrower category than flame bait, that a troll is categorized by containing some assertion that is wrong but not overtly controversial. See also Troll-O-Meter.
Well, I stand by my analysis of the post.
About separate compilation.
Take Coq: it has separate compilation. Loading two .vo is not super clear, e.g. their loading order is relevant (e.g. the last notation takes precedence). If you reason in term of heaps, then the order is fixed, either you user that heap or not. You can't merge heaps. That is much easier.
I while ago I tried many snapshot systems, in the end I've used virtualbox. I let you imagine why.
... because userspace checkpointing is fast, easy and correct? :smiling_devil:
The last one, in particular ;-)
in fairness, that's probably possible for a process doing just plain file I/O instead of opening sockets :sweat_smile:
Théo Zimmermann said:
Emilio Jesús Gallego Arias I think you are the only one who thinks he's talking about HOL here.
If not HOL what is he talking about? Clearly you can design a system in OCaml that doesn't require that time to load.
We recently invited Makarius to talk about the Isabelle build system and indeed heap images are pretty essential to what they do
Anyways I don't see anything wrong or trollish in the post, other than indeed it addresses a very emotional and complex topic and of course he gives strong opinions but I wouldn't expect less of a professor of his level.
And for me, as part of this community, I'd rather avoid qualifying colleagues with adjectives such as "troll". As scientists we are free to disagree with other, but name-calling better not be based on vague interpretations that are far from consensual.
Emilio Jesús Gallego Arias said:
If not HOL what is he talking about? Clearly you can design a system in OCaml that doesn't require that time to load.
he's blaming this HOL Light problem entirely on OCaml lacking images https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneous/topic/Standard.20ML.20vs.20.28O.29Caml/near/302910577.
In 1990 that was a very valid concern
I don't see a problem with the phrasing "With no way to save an image, you had to rebuild HOL Light from sources at every launch (even today). Even Edinburgh LCF was a stand-alone executable." That was 100% accurate
given the way these systems work
it is a very valid concern, if you wanna do a HOL-style prover you better use PolyML these days
Isabelle relies on this (and threading) extensively
it is intrinsic to their design
Indeed saving of state is a huge pain point in OCaml
What we have in Coq with Marshall is just horrible and has many serious problems and limitations
and prevents from doing very interesting stuff
even in Coq today
we don't support saving a proof session
sorry that's horrible
Was there a ML dialect with images in 1990? If not then the point is moot.
Emilio Jesús Gallego Arias said:
we don't support saving a proof session
we had a Write State command, it got removed for some reason (cf 447965a9d4b409850e94a3289097ed28de8772fd)
since nobody complained it seems there were no users
Compiling files looked like a more principled way of speeding startup at that time I remember. It still looks like that to me today but I am not aware of how it works in other provers. Last time I discussed with Makarius he was happy with replaying the whole Isabelle standard lib with polyML in a few seconds (provided you had 3-4 cores/processors).
Larry Paulson was using HOL Light just a few years ago to port things from the HOL Light stdlib to Isabelle. So he's not complaining about lack of heap images / checkpoint support in the 90s/2000s, he's complaining about it in modern OCaml.
but my take would be that heap image support in Poly/ML has likely been maintained precisely because "big clients" (HOL4, Isabelle, ...) use it and require it. HOL Light could do without it, since it's even more niche than HOL4 and Isabelle, so therefore we get pointers in README to general Linux checkpointing tools.
@Emilio Jesús Gallego Arias what would be the benefits of such feature in ocaml? I am curious.
I mean for coq.
one possibly-relevant data point: the colossus of the HOL4 world, CakeML, stopped using Poly/ML heap images as part of their regular builds a couple of years ago, and now uses an "incremental file-based build" similar to in Coq projects (Holmake
in place of coq_makefile)
Last updated: Jun 05 2023 at 09:01 UTC