Karl Palmskog (Oct 06 2022 at 19:19): Karl Palmskog (Oct 06 2022 at 19:19):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.
Guillaume Melquiond (Oct 06 2022 at 19:57):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.
Enrico Tassi (Oct 06 2022 at 20:27):Does OCaml have 100 times more users than polyml?
Enrico Tassi (Oct 06 2022 at 20:28):(just one way to cut the crap)
Karl Palmskog (Oct 06 2022 at 20:30):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
Karl Palmskog (Oct 06 2022 at 20:34):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)
Enrico Tassi (Oct 06 2022 at 20:36):I don't think we should feed the troll
Karl Palmskog (Oct 06 2022 at 20:37):fine by me, but I didn't even understand the point about Makefiles until Guillaume's comment.
Enrico Tassi (Oct 06 2022 at 20:39):it's called separate compilation for the civilized ones
Enrico Tassi (Oct 06 2022 at 20:42):(and I think some SML implementations do have it)
Enrico Tassi (Oct 06 2022 at 20:43):it is really a trolling post
Emilio Jesús Gallego Arias (Oct 07 2022 at 15:36):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.
Paolo Giarrusso (Oct 07 2022 at 17:50):some writers like to separate opinions from facts more explicitly :-)
Emilio Jesús Gallego Arias (Oct 07 2022 at 18:01):Paolo Giarrusso said:
some writers like to separate opinions from facts more explicitly :-)
what concrete phrase you have a problem with?
Paolo Giarrusso (Oct 07 2022 at 18:06):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)
Emilio Jesús Gallego Arias (Oct 07 2022 at 18:07):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.
Emilio Jesús Gallego Arias (Oct 07 2022 at 18:07):The latter can't be addressed, the former yes
Théo Zimmermann (Oct 07 2022 at 18:07):Does trolling implies saying something wrong?
Emilio Jesús Gallego Arias (Oct 07 2022 at 18:08):In this case "this is a world beating system" I have to agree with him
Emilio Jesús Gallego Arias (Oct 07 2022 at 18:08):if that's the user experience for HOL , that's terrible
Emilio Jesús Gallego Arias (Oct 07 2022 at 18:08):tho it would be nice to ask for a clarification there
Emilio Jesús Gallego Arias (Oct 07 2022 at 18:08):to see he means HOL, not OCaml
Emilio Jesús Gallego Arias (Oct 07 2022 at 18:08):OCaml has its own problems
Emilio Jesús Gallego Arias (Oct 07 2022 at 18:09):when I migrated from Haskell I was far from impressed, and Haskell is not the 5th wonder of the world
Emilio Jesús Gallego Arias (Oct 07 2022 at 18:09):it also has very good things of course
Paolo Giarrusso (Oct 07 2022 at 18:12):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:
Théo Zimmermann (Oct 07 2022 at 18:16):@Emilio Jesús Gallego Arias I think you are the only one who thinks he's talking about HOL here.
Paolo Giarrusso (Oct 07 2022 at 18:20):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.
Paolo Giarrusso (Oct 07 2022 at 18:21):somehow the option of doing <anything else than saving an image> isn't even worth mentioning — I mean, does Isabelle save images?
Karl Palmskog (Oct 07 2022 at 18:25):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
Karl Palmskog (Oct 07 2022 at 18:27):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
Paolo Giarrusso (Oct 07 2022 at 18:28):I was mostly wondering why they can't compile sources to binaries and load the binaries, instead of reproving theorems
Théo Zimmermann (Oct 07 2022 at 18:28):Maybe because of when HOL Light was created?
Karl Palmskog (Oct 07 2022 at 18:31):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.
Paolo Giarrusso (Oct 07 2022 at 18:31):yes, apparently, they're happy to link to _checkpointing tools_, which worries me a bit (maybe for no good reason)
Paolo Giarrusso (Oct 07 2022 at 18:32):... 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?
Karl Palmskog (Oct 07 2022 at 18:34):this is apparently the checkpointing tool of preference these days: https://dmtcp.sourceforge.io/
Karl Palmskog (Oct 07 2022 at 18:39):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
Enrico Tassi (Oct 07 2022 at 19:09):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.
Enrico Tassi (Oct 07 2022 at 19:11):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.
Enrico Tassi (Oct 07 2022 at 19:12):I while ago I tried many snapshot systems, in the end I've used virtualbox. I let you imagine why.
Paolo Giarrusso (Oct 07 2022 at 19:17):... because userspace checkpointing is fast, easy and correct? :smiling_devil:
Enrico Tassi (Oct 07 2022 at 19:17):The last one, in particular ;-)
Paolo Giarrusso (Oct 07 2022 at 19:20):in fairness, that's probably possible for a process doing just plain file I/O instead of opening sockets :sweat_smile:
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:41):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.
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:43):We recently invited Makarius to talk about the Isabelle build system and indeed heap images are pretty essential to what they do
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:45):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.
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:49):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.
Paolo Giarrusso (Oct 08 2022 at 13:55):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.
Emilio Jesús Gallego Arias (Oct 08 2022 at 14:10):In 1990 that was a very valid concern
Emilio Jesús Gallego Arias (Oct 08 2022 at 14:11):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
Emilio Jesús Gallego Arias (Oct 08 2022 at 14:11):given the way these systems work
Emilio Jesús Gallego Arias (Oct 08 2022 at 14:11):it is a very valid concern, if you wanna do a HOL-style prover you better use PolyML these days
Emilio Jesús Gallego Arias (Oct 08 2022 at 14:12):Isabelle relies on this (and threading) extensively
Emilio Jesús Gallego Arias (Oct 08 2022 at 14:12):it is intrinsic to their design
Emilio Jesús Gallego Arias (Oct 08 2022 at 14:13):Indeed saving of state is a huge pain point in OCaml
Emilio Jesús Gallego Arias (Oct 08 2022 at 14:13):What we have in Coq with Marshall is just horrible and has many serious problems and limitations
Emilio Jesús Gallego Arias (Oct 08 2022 at 14:14):and prevents from doing very interesting stuff
Emilio Jesús Gallego Arias (Oct 08 2022 at 14:14):even in Coq today
Emilio Jesús Gallego Arias (Oct 08 2022 at 14:14):we don't support saving a proof session
Emilio Jesús Gallego Arias (Oct 08 2022 at 14:14):sorry that's horrible
Pierre Courtieu (Oct 08 2022 at 14:23):Was there a ML dialect with images in 1990? If not then the point is moot.
Gaëtan Gilbert (Oct 08 2022 at 14:37):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
Pierre Courtieu (Oct 08 2022 at 14:47):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).
Karl Palmskog (Oct 08 2022 at 14:58):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.
Karl Palmskog (Oct 08 2022 at 15:04):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.
Pierre Courtieu (Oct 08 2022 at 18:13):@Emilio Jesús Gallego Arias what would be the benefits of such feature in ocaml? I am curious.
Pierre Courtieu (Oct 08 2022 at 18:13):I mean for coq.
Karl Palmskog (Oct 08 2022 at 20:46):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